Step | Hyp | Ref | Expression |
1 |
|
eqtr |
rlrec z S (l |> a) = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) ->
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = S @ (l, a, rlrec z S l) ->
rlrec z S (l |> a) = S @ (l, a, rlrec z S l) |
2 |
|
lreceq3 |
rev (l |> a) = a : rev l -> lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (rev (l |> a)) = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) |
3 |
2 |
conv rlrec |
rev (l |> a) = a : rev l -> rlrec z S (l |> a) = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) |
4 |
|
revsnoc |
rev (l |> a) = a : rev l |
5 |
3, 4 |
ax_mp |
rlrec z S (l |> a) = lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) |
6 |
1, 5 |
ax_mp |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = S @ (l, a, rlrec z S l) -> rlrec z S (l |> a) = S @ (l, a, rlrec z S l) |
7 |
|
eqtr |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) @ (a, rev l, rlrec z S l) ->
(\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) @ (a, rev l, rlrec z S l) = S @ (l, a, rlrec z S l) ->
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = S @ (l, a, rlrec z S l) |
8 |
|
lrecS |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) =
(\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) @ (a, rev l, lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (rev l)) |
9 |
8 |
conv rlrec |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) @ (a, rev l, rlrec z S l) |
10 |
7, 9 |
ax_mp |
(\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) @ (a, rev l, rlrec z S l) = S @ (l, a, rlrec z S l) ->
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = S @ (l, a, rlrec z S l) |
11 |
|
revrev |
rev (rev l) = l |
12 |
|
anlr |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> a2 = rev l |
13 |
12 |
reveqd |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> rev a2 = rev (rev l) |
14 |
11, 13 |
syl6eq |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> rev a2 = l |
15 |
|
anll |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> a1 = a |
16 |
|
anr |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> a3 = rlrec z S l |
17 |
15, 16 |
preqd |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> a1, a3 = a, rlrec z S l |
18 |
14, 17 |
preqd |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> rev a2, a1, a3 = l, a, rlrec z S l |
19 |
18 |
appeq2d |
a1 = a /\ a2 = rev l /\ a3 = rlrec z S l -> S @ (rev a2, a1, a3) = S @ (l, a, rlrec z S l) |
20 |
19 |
applamed |
a1 = a /\ a2 = rev l -> (\ a3, S @ (rev a2, a1, a3)) @ rlrec z S l = S @ (l, a, rlrec z S l) |
21 |
20 |
appslamed |
a1 = a -> (\\ a2, \ a3, S @ (rev a2, a1, a3)) @ (rev l, rlrec z S l) = S @ (l, a, rlrec z S l) |
22 |
21 |
appslame |
(\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) @ (a, rev l, rlrec z S l) = S @ (l, a, rlrec z S l) |
23 |
10, 22 |
ax_mp |
lrec z (\\ a1, \\ a2, \ a3, S @ (rev a2, a1, a3)) (a : rev l) = S @ (l, a, rlrec z S l) |
24 |
6, 23 |
ax_mp |
rlrec z S (l |> a) = S @ (l, a, rlrec z S l) |