Nuprl - Proof: l before-iff 2 1 2

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

1. T: Type
2. L: T List
3. u: T
4. v: T List
5. x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x] @ L2 @ [y] @ L3))
6. x: T
7. y: T
8. L1,L2,L3:T List. [u / v] = (L1 @ [x] @ L2 @ [y] @ L3)

x = u & (y v) x before y v

By: ExRepD THEN Analyze -4 THEN All Reduce THEN SplitCons -1

Generated subgoals:

1 5. x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x / (L2 @ [y / L3])]))
6. x: T
7. y: T
8. L2: T List
9. L3: T List
10. u = x
11. v = (L2 @ [y / L3])
x = u & (y v) x before y v 1 step

2 5. x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x / (L2 @ [y / L3])]))
6. x: T
7. y: T
8. u1: T
9. v1: T List
10. L2: T List
11. L3: T List
12. u = u1
13. v = (v1 @ [x / (L2 @ [y / L3])])
x = u & (y v) x before y v 2 steps

About:

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

1	5. `x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x / (L2 @ [y / L3])]))` 6. `x:` `T` 7. `y:` `T` 8. `L2:` `T List` 9. `L3:` `T List` 10. `u = x` 11. `v = (L2 @ [y / L3])` `x = u & (y v) x before y v`	1 step

2	5. `x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x / (L2 @ [y / L3])]))` 6. `x:` `T` 7. `y:` `T` 8. `u1:` `T` 9. `v1:` `T List` 10. `L2:` `T List` 11. `L3:` `T List` 12. `u = u1` 13. `v = (v1 @ [x / (L2 @ [y / L3])])` `x = u & (y v) x before y v`	2 steps