(7steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
At:
div-graph-iso
1
1
1.
i:
2.
j:
Dec(
c:
. j = i
c
)
By:
Assert Dec(i | j)
THEN
Unfold `divides` -1
THEN
RepeatFor 2 (ParallelOp -1)
THEN
Try Easy
Generated subgoals:
1
3.
c:
. j = i
c
c:
. j = i
c
2
steps
2
3.
(
c:
. j = i
c)
(
c:
. j = i
c
)
1
step
About:
(7steps total)
PrintForm
Definitions
Lemmas
graph
1
2
Sections
Graphs
Doc
c:
. j = i
c
c:
. j = ic 
(c:. j = ic) (c:. j = ic )
Dec(c:. j = ic )
c:. j = ic c:. j = ic (c:. j = ic) (c:. j = ic )
