GM06dGnd
Premises:
; Graph of Exercise 1.1 ; R represents directed arcs in the graph ; (R q r) denotes an arc directed from 'q' to 'r' ; The vertex out-order is not greater than 1 ; (successors are unique to their predecessor) (forall (?X ?Y ?Z) (=> (and (R ?X ?Y) (R ?X ?Z)) (= ?Y ?Z))) ; The vertex in-order is not greater than 1 ; (predecessors are unique to their successor) (forall (?X ?Y ?Z) (=> (and (R ?Y ?X) (R ?Z ?X)) (= ?Y ?Z))) ; R is anti-reflexive (forall ?X (not (R ?X ?X))) ; Arcs in the graph ; The graph is a cyclic connection of four vertices: ; 'a', 'b', 'c' and 'd' (R a b) (R b c) (R c d) (R d a) ; Each vertex name denotes a distinct vertex in the graph (not (= a b)) (not (= a c)) (not (= a d)) (not (= b c)) (not (= b d)) (not (= c d))
Conclusion:
(and (or (R a b) (R b a) (exists ?Z (and (R a ?Z) (R ?Z b))) (exists ?Z (and (R b ?Z) (R ?Z a)))) (or (R a c) (R c a) (exists ?Z (and (R a ?Z) (R ?Z c))) (exists ?Z (and (R c ?Z) (R ?Z a)))) (or (R a d) (R d a) (exists ?Z (and (R a ?Z) (R ?Z d))) (exists ?Z (and (R d ?Z) (R ?Z a)))) (or (R b c) (R c b) (exists ?Z (and (R b ?Z) (R ?Z c))) (exists ?Z (and (R v ?Z) (R ?Z b)))) (or (R b d) (R d b) (exists ?Z (and (R b ?Z) (R ?Z d))) (exists ?Z (and (R d ?Z) (R ?Z b)))) (or (R c d) (R d c) (exists ?Z (and (R c ?Z) (R ?Z d))) (exists ?Z (and (R d ?Z) (R ?Z c)))))