(28steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: connect-iff 2 1
1. the_graph: Graph
2. x,y:Vertices(the_graph). Dec(x = y)
3. x: Vertices(the_graph)
4. y: Vertices(the_graph)
5. x = y
x-the_graph- > *y
By:
HypSubst -1 0
THEN
Connect
Generated subgoals:

None

About:
decidableequalall

(28steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc