Step | Hyp | Ref | Expression |
1 |
|
eqtr |
a : l ++ r = (\\ x, \\ z, \ y, x : y) @ (a, l, lrec r (\\ x, \\ z, \ y, x : y) l) ->
(\\ x, \\ z, \ y, x : y) @ (a, l, lrec r (\\ x, \\ z, \ y, x : y) l) = a : (l ++ r) ->
a : l ++ r = a : (l ++ r) |
2 |
|
lrecS |
lrec r (\\ x, \\ z, \ y, x : y) (a : l) = (\\ x, \\ z, \ y, x : y) @ (a, l, lrec r (\\ x, \\ z, \ y, x : y) l) |
3 |
2 |
conv append |
a : l ++ r = (\\ x, \\ z, \ y, x : y) @ (a, l, lrec r (\\ x, \\ z, \ y, x : y) l) |
4 |
1, 3 |
ax_mp |
(\\ x, \\ z, \ y, x : y) @ (a, l, lrec r (\\ x, \\ z, \ y, x : y) l) = a : (l ++ r) -> a : l ++ r = a : (l ++ r) |
5 |
|
anll |
x = a /\ z = l /\ y = l ++ r -> x = a |
6 |
|
anr |
x = a /\ z = l /\ y = l ++ r -> y = l ++ r |
7 |
5, 6 |
conseqd |
x = a /\ z = l /\ y = l ++ r -> x : y = a : (l ++ r) |
8 |
7 |
applamed |
x = a /\ z = l -> (\ y, x : y) @ (l ++ r) = a : (l ++ r) |
9 |
8 |
appslamed |
x = a -> (\\ z, \ y, x : y) @ (l, l ++ r) = a : (l ++ r) |
10 |
9 |
appslame |
(\\ x, \\ z, \ y, x : y) @ (a, l, l ++ r) = a : (l ++ r) |
11 |
10 |
conv append |
(\\ x, \\ z, \ y, x : y) @ (a, l, lrec r (\\ x, \\ z, \ y, x : y) l) = a : (l ++ r) |
12 |
4, 11 |
ax_mp |
a : l ++ r = a : (l ++ r) |