Nuprl - Proof: mapoutl is singleton 1

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

1. A: Type
2. B: Type
3. L: (A+B) List
4. a: A
5. mapoutl(L) = [a]

L1,L2:(A+B) List. L = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil

By: ListInd -3 THEN Reduce 0

Generated subgoals:

1 nil = [a] (L1,L2:(A+B) List. nil = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil) 1 step

2 5. u: A+B
6. v: (A+B) List
7. mapoutl(v) = [a] (L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)
mapoutl([u / v]) = [a] (L1,L2:(A+B) List. [u / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil) 3 steps

About:

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

1	`nil = [a] (L1,L2:(A+B) List. nil = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil)`	1 step

2	5. `u:` `A+B` 6. `v:` `(A+B) List` 7. `mapoutl(v) = [a] (L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)` `mapoutl([u / v]) = [a] (L1,L2:(A+B) List. [u / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil)`	3 steps