(10steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc
At:
f91-val
i:
. f91(i) ~ if 101 <
i
i-10 else 91 fi
By:
(InductionOn (d = if 101 <
i
0 else 101-i fi) CompNatInd) THENA SplitOnConclITE
Generated subgoal:
1
1.
d:
2.
d1:
. d1 < d
(
i:
. if 101 <
i
0 else 101-i fi = d1
(f91(i) ~ if 101 <
i
i-10 else 91 fi))
i:
. if 101 <
i
0 else 101-i fi = d
(f91(i) ~ if 101 <
i
i-10 else 91 fi)
9
steps
About:
(10steps total)
PrintForm
Definitions
graph
1
1
Sections
Graphs
Doc