Nuprl - Proof: mapoutl is append 1 2 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)
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)

By: Analyze -3 THEN Reduce 0

Generated subgoals:

1 9. x: A
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)
12. [x / mapoutl(v1)] = [u / (v @ l2)]
L1,L2:(A+B) List. [inl(x) / v1] = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2 1 step

2 9. y: 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)
12. mapoutl(v1) = [u / (v @ l2)]
L1,L2:(A+B) List. [inr(y) / v1] = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2 1 step

About:

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

1	9. `x:` `A` 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)` 12. `[x / mapoutl(v1)] = [u / (v @ l2)]` `L1,L2:(A+B) List. [inl(x) / v1] = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2`	1 step

2	9. `y:` `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)` 12. `mapoutl(v1) = [u / (v @ l2)]` `L1,L2:(A+B) List. [inr(y) / v1] = (L1 @ L2) & mapoutl(L1) = [u / v] & mapoutl(L2) = l2`	1 step