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