Step | Hyp | Ref | Expression |
1 |
|
eqtr |
recnaux z S (suc n) = (\ p, suc (fst p), S @ p) @ rec (0, z) (\ p, suc (fst p), S @ p) n ->
(\ p, suc (fst p), S @ p) @ rec (0, z) (\ p, suc (fst p), S @ p) n = suc (fst (recnaux z S n)), S @ recnaux z S n ->
recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n |
2 |
|
recS |
rec (0, z) (\ p, suc (fst p), S @ p) (suc n) = (\ p, suc (fst p), S @ p) @ rec (0, z) (\ p, suc (fst p), S @ p) n |
3 |
2 |
conv recnaux |
recnaux z S (suc n) = (\ p, suc (fst p), S @ p) @ rec (0, z) (\ p, suc (fst p), S @ p) n |
4 |
1, 3 |
ax_mp |
(\ p, suc (fst p), S @ p) @ rec (0, z) (\ p, suc (fst p), S @ p) n = suc (fst (recnaux z S n)), S @ recnaux z S n ->
recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n |
5 |
|
fsteq |
p = recnaux z S n -> fst p = fst (recnaux z S n) |
6 |
5 |
suceqd |
p = recnaux z S n -> suc (fst p) = suc (fst (recnaux z S n)) |
7 |
|
appeq2 |
p = recnaux z S n -> S @ p = S @ recnaux z S n |
8 |
6, 7 |
preqd |
p = recnaux z S n -> suc (fst p), S @ p = suc (fst (recnaux z S n)), S @ recnaux z S n |
9 |
8 |
applame |
(\ p, suc (fst p), S @ p) @ recnaux z S n = suc (fst (recnaux z S n)), S @ recnaux z S n |
10 |
9 |
conv recnaux |
(\ p, suc (fst p), S @ p) @ rec (0, z) (\ p, suc (fst p), S @ p) n = suc (fst (recnaux z S n)), S @ recnaux z S n |
11 |
4, 10 |
ax_mp |
recnaux z S (suc n) = suc (fst (recnaux z S n)), S @ recnaux z S n |