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