Nuprl - Proof: f91-val 1 1 1 1

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

At: f91-val 1 1 1 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))
3. i:
4. i101
5. i100
6. 101-i = d
7. f91(i+11) ~ if 101 < i+11 i+11-10 else 91 fi
8. 101 < i+11

f91(i+11-10) ~ 91

By: InstHyp [d-1;i+1] 2

Generated subgoals:

1 if 101 < i+1 0 else 101-(i+1) fi = d-1 1 step

2 9. f91(i+1) ~ if 101 < i+1 i+1-10 else 91 fi
f91(i+11-10) ~ 91 3 steps

About:

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