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

At: div-graph-iso 1
Graph(i: -- > in | n:) Graph(i,j:. c:. j = ic )
By:
BackThru Thm* fun-graph-rel-graph
THEN
Try (FwdThru Thm* a,b:, n:. na = nb a = b [-1])
THEN
Try Easy
Generated subgoal:

11. i:
2. j:
Dec(c:. j = ic )		4 steps

About:
decidableintmultiplyfunctionuniverseequalimpliesallexists

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