(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:

11. 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:
ifthenelseintnatural_numbersubtractequalsqequalimpliesall

(10steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc