Abella logo (small)

graphs.thm

Kind g type. Type node g -> prop. Type adj, path g -> g -> prop. % Introduce the structure of graphs as a collection of axioms (theorems with skips). Theorem refl : forall n, node n -> path n n. skip. Theorem trans : forall x y z, adj x y -> path y z -> path x z. skip. Type a,b,c,d,e,f g. Theorem nodes : node a /\ node b /\ node c /\ node d /\ node e /\ node f. skip. Theorem adjs : adj a b /\ adj a c /\ adj b c /\ adj b e /\ adj c e /\ adj d f. skip. Theorem example1 : path a e. apply nodes. apply adjs. apply refl to H5. apply trans to H10 H13. apply trans to H7 H14. search. Theorem example1_fchain : path a e. fchain 6 nodes adjs refl trans. search.