Step | Hyp | Ref | Expression |
1 |
|
eqtr |
rlrec z S 0 = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 -> lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 = z -> rlrec z S 0 = z |
2 |
|
lreceq3 |
rev 0 = 0 -> lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (rev 0) = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 |
3 |
2 |
conv rlrec |
rev 0 = 0 -> rlrec z S 0 = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 |
4 |
|
rev0 |
rev 0 = 0 |
5 |
3, 4 |
ax_mp |
rlrec z S 0 = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 |
6 |
1, 5 |
ax_mp |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 = z -> rlrec z S 0 = z |
7 |
|
lrec0 |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) 0 = z |
8 |
6, 7 |
ax_mp |
rlrec z S 0 = z |