GM08a
Premises:
; Graph of Exercise 2.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) ; P represents a colored or marked vertex in the graph (P a) (P b) (not (P c)) (not (P d)) ; 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:
; There is a vertex that is colored and whose successor is colored (exists ?X (and (P ?X) (forall ?Y (=> (R ?X ?Y) (P ?Y)))))