Nuprl - Proof: no repeats mapoutl

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

A,B:Type, s:(A+B) List. no_repeats(A+B;s) no_repeats(A;mapoutl(s))

By: InductionOnList THEN Unfold `mapoutl` 0 THEN Unfold `mapfilter` 0 THEN Reduce 0 THEN Try (SplitOnConclITE THEN (Reduce 0) THEN (Fold `mapfilter` 0) THEN (Fold `mapoutl` 0)) THEN Try ((RWO Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l) 0) THEN ThinTrivial THEN (Try Trivial))

Generated subgoals:

1 1. A: Type
2. B: Type
3. s: (A+B) List
no_repeats(A+B;nil) no_repeats(A;nil) 1 step

2 1. A: Type
2. B: Type
3. s: (A+B) List
4. u: A+B
5. v: (A+B) List
6. isl(u)
7. no_repeats(A+B;v)
8. (u v)
9. no_repeats(A;mapoutl(v))
(outl(u) mapoutl(v)) 2 steps

About:

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

1	1. `A:` `Type` 2. `B:` `Type` 3. `s:` `(A+B) List` `no_repeats(A+B;nil) no_repeats(A;nil)`	1 step

2	1. `A:` `Type` 2. `B:` `Type` 3. `s:` `(A+B) List` 4. `u:` `A+B` 5. `v:` `(A+B) List` 6. `isl(u)` 7. `no_repeats(A+B;v)` 8. `(u v)` 9. `no_repeats(A;mapoutl(v))` `(outl(u) mapoutl(v))`	2 steps