Step | Hyp | Ref | Expression |
1 |
|
eqtr |
rev (a : l) = (\\ a1, \\ a2, \ a3, a3 |> a1) @ (a, l, rev l) -> (\\ a1, \\ a2, \ a3, a3 |> a1) @ (a, l, rev l) = rev l |> a -> rev (a : l) = rev l |> a |
2 |
|
lrecS |
lrec 0 (\\ a1, \\ a2, \ a3, a3 |> a1) (a : l) = (\\ a1, \\ a2, \ a3, a3 |> a1) @ (a, l, lrec 0 (\\ a1, \\ a2, \ a3, a3 |> a1) l) |
3 |
2 |
conv rev |
rev (a : l) = (\\ a1, \\ a2, \ a3, a3 |> a1) @ (a, l, rev l) |
4 |
1, 3 |
ax_mp |
(\\ a1, \\ a2, \ a3, a3 |> a1) @ (a, l, rev l) = rev l |> a -> rev (a : l) = rev l |> a |
5 |
|
anr |
a1 = a /\ a2 = l /\ a3 = rev l -> a3 = rev l |
6 |
|
anll |
a1 = a /\ a2 = l /\ a3 = rev l -> a1 = a |
7 |
5, 6 |
snoceqd |
a1 = a /\ a2 = l /\ a3 = rev l -> a3 |> a1 = rev l |> a |
8 |
7 |
applamed |
a1 = a /\ a2 = l -> (\ a3, a3 |> a1) @ rev l = rev l |> a |
9 |
8 |
appslamed |
a1 = a -> (\\ a2, \ a3, a3 |> a1) @ (l, rev l) = rev l |> a |
10 |
9 |
appslame |
(\\ a1, \\ a2, \ a3, a3 |> a1) @ (a, l, rev l) = rev l |> a |
11 |
4, 10 |
ax_mp |
rev (a : l) = rev l |> a |