Nuprl - Proof: member reverse

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

T:Type, x:T, L:T List. (x rev(L)) (x L)

By: InductionOnList THEN Reduce 0 THEN RWW Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2) 0 THEN RWW Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) 0

Generated subgoals:

1 1. T: Type
2. x: T
3. L: T List
4. u: T
5. v: T List
6. (x rev(v)) (x v)
7. (x rev(v)) (x v)
8. (x rev(v)) x = u (x nil)
x = u (x v) 1 step

2 1. T: Type
2. x: T
3. L: T List
4. u: T
5. v: T List
6. (x rev(v)) (x v)
7. (x rev(v)) (x v)
8. x = u (x v)
(x rev(v)) x = u (x nil) 1 step

About:

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

1	1. `T:` `Type` 2. `x:` `T` 3. `L:` `T List` 4. `u:` `T` 5. `v:` `T List` 6. `(x rev(v)) (x v)` 7. `(x rev(v)) (x v)` 8. `(x rev(v)) x = u (x nil)` `x = u (x v)`	1 step

2	1. `T:` `Type` 2. `x:` `T` 3. `L:` `T List` 4. `u:` `T` 5. `v:` `T List` 6. `(x rev(v)) (x v)` 7. `(x rev(v)) (x v)` 8. `x = u (x v)` `(x rev(v)) x = u (x nil)`	1 step