Nuprl - Proof: equal appends case1 2 2

(8steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1. T: Type
2. x1: T List
3. u: T
4. v: T List
5. z,x2,x3:T List. ||v||||z|| (v @ x2) = (z @ x3) (z':T List. z = (v @ z') & x2 = (z' @ x3))
6. z: T List
7. u1: T
8. v1: T List
9. x2,x3:T List. ||v||+1||v1|| [u / (v @ x2)] = (v1 @ x3) (z':T List. v1 = [u / (v @ z')] & x2 = (z' @ x3))

x2,x3:T List. ||v||+1||v1||+1 [u / (v @ x2)] = [u1 / (v1 @ x3)] (z':T List. [u1 / v1] = [u / (v @ z')] & x2 = (z' @ x3))

By: Auto THEN InstHyp [v1;x2;x3] 5

Generated subgoals:

1 10. x2: T List
11. x3: T List
12. ||v||+1||v1||+1
13. [u / (v @ x2)] = [u1 / (v1 @ x3)]
(v @ x2) = (v1 @ x3) 1 step

2 10. x2: T List
11. x3: T List
12. ||v||+1||v1||+1
13. [u / (v @ x2)] = [u1 / (v1 @ x3)]
14. z':T List. v1 = (v @ z') & x2 = (z' @ x3)
z':T List. [u1 / v1] = [u / (v @ z')] & x2 = (z' @ x3) 2 steps

About:

(8steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1	10. `x2:` `T List` 11. `x3:` `T List` 12. `\|\|v\|\|+1\|\|v1\|\|+1` 13. `[u / (v @ x2)] = [u1 / (v1 @ x3)]` `(v @ x2) = (v1 @ x3)`	1 step

2	10. `x2:` `T List` 11. `x3:` `T List` 12. `\|\|v\|\|+1\|\|v1\|\|+1` 13. `[u / (v @ x2)] = [u1 / (v1 @ x3)]` 14. `z':T List. v1 = (v @ z') & x2 = (z' @ x3)` `z':T List. [u1 / v1] = [u / (v @ z')] & x2 = (z' @ x3)`	2 steps