Nuprl - Proof: l member decomp

(13steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: l member decomp

T:Type, l:T List, x:T. (x

(

l1,l2:T List. l = (l1 @ [x] @ l2))

By:	((InductionOnList ((THEN ((RWW Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) 0) (THEN ((RWW Thm* x:T. (x nil) False 0)) THEN ExRepD

Generated subgoals:

1 1. T : Type
2. T List
3. x : T
4. l1 : T List
5. l2 : T List
6. nil = (l1 @ [x] @ l2)
  False
1 step

2 1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  (l1,l2:T List. v = (l1 @ [x] @ l2))
6. x : T
7. x = u  (x  v)
  l1,l2:T List. [u / v] = (l1 @ [x] @ l2)
5 steps

3 1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  (l1,l2:T List. v = (l1 @ [x] @ l2))
6. x : T
7. l1 : T List
8. l2 : T List
9. [u / v] = (l1 @ [x] @ l2)
  x = u  (x  v)
6 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(13steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc

1	1. T : Type 2. T List 3. x : T 4. l1 : T List 5. l2 : T List 6. nil = (l1 @ [x] @ l2) False	1 step
2	1. T : Type 2. T List 3. u : T 4. v : T List 5. x:T. (x v) (l1,l2:T List. v = (l1 @ [x] @ l2)) 6. x : T 7. x = u (x v) l1,l2:T List. [u / v] = (l1 @ [x] @ l2)	5 steps
3	1. T : Type 2. T List 3. u : T 4. v : T List 5. x:T. (x v) (l1,l2:T List. v = (l1 @ [x] @ l2)) 6. x : T 7. l1 : T List 8. l2 : T List 9. [u / v] = (l1 @ [x] @ l2) x = u (x v)	6 steps