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