Nuprl - Proof: mapoutl is append 1

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

1. A: Type
2. B: Type
3. L: (A+B) List
4. l1: A List
5. l2: A List
6. mapoutl(L) = (l1 @ l2)

L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = l1 & mapoutl(L2) = l2

By: MoveToConcl 3 THEN ListInd -2 THEN Reduce 0

Generated subgoals:

1 3. l1: A List
4. l2: A List
L:(A+B) List. mapoutl(L) = l2 (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = nil & mapoutl(L2) = l2) 1 step

2 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) 5 steps

About:

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

1	3. `l1:` `A List` 4. `l2:` `A List` `L:(A+B) List. mapoutl(L) = l2 (L1,L2:(A+B) List. L = (L1 @ L2) & mapoutl(L1) = nil & mapoutl(L2) = l2)`	1 step

2	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)`	5 steps