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

By: ThinTrivial THEN ExRepD THEN InstConcl [[inr(y) / L1];L2] THEN Reduce 0 THEN Analyze

Generated subgoals:

None

About:

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