Nuprl - Proof: mapoutl is singleton

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

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

By: Auto THEN ExRepD

Generated subgoals:

1 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 5 steps

2 1. A: Type
2. B: Type
3. L: (A+B) List
4. a: A
5. L1: (A+B) List
6. L2: (A+B) List
7. L = (L1 @ [inl(a)] @ L2)
8. mapoutl(L1) = nil
9. mapoutl(L2) = nil
mapoutl(L) = [a] 1 step

About:

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

1	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`	5 steps

2	1. `A:` `Type` 2. `B:` `Type` 3. `L:` `(A+B) List` 4. `a:` `A` 5. `L1:` `(A+B) List` 6. `L2:` `(A+B) List` 7. `L = (L1 @ [inl(a)] @ L2)` 8. `mapoutl(L1) = nil` 9. `mapoutl(L2) = nil` `mapoutl(L) = [a]`	1 step