Nuprl - Proof: mapoutl is append 1 2

(9steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1. A: Type
2. B: Type
3. l1: A List
4. l2: A List
5. u: A
6. v: A List
7. L:(A+B) List. mapoutl(L) = (v @ l2) (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = v & mapoutl(L2) = l2)

L:(A+B) List. mapoutl(L) = [u / (v @ l2)] (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)

By: InductionOnList THEN Reduce 0

Generated subgoals:

1 8. L: (A+B) List
nil = [u / (v @ l2)] (L1,L2:(A+B) List. nil = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2) 1 step

2 8. L: (A+B) List
9. u1: A+B
10. v1: (A+B) List
11. mapoutl(v1) = [u / (v @ l2)] (L1,L2:(A+B) List. v1 = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)
mapoutl([u1 / v1]) = [u / (v @ l2)] (L1,L2:(A+B) List. [u1 / v1] = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2) 3 steps

About:

(9steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1	8. `L:` `(A+B) List` `nil = [u / (v @ l2)] (L1,L2:(A+B) List. nil = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)`	1 step

2	8. `L:` `(A+B) List` 9. `u1:` `A+B` 10. `v1:` `(A+B) List` 11. `mapoutl(v1) = [u / (v @ l2)] (L1,L2:(A+B) List. v1 = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)` `mapoutl([u1 / v1]) = [u / (v @ l2)] (L1,L2:(A+B) List. [u1 / v1] = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2)`	3 steps