Nuprl - Proof: equal appends case1 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))

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

By: InductionOnList THEN Reduce 0

Generated subgoals:

1 6. z: T List
x2,x3:T List. ||v||+10 [u / (v @ x2)] = x3 (z':T List. nil = [u / (v @ z')] & x2 = (z' @ x3)) 1 step

2 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)) 4 steps

About:

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

1	6. `z:` `T List` `x2,x3:T List. \|\|v\|\|+10 [u / (v @ x2)] = x3 (z':T List. nil = [u / (v @ z')] & x2 = (z' @ x3))`	1 step

2	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))`	4 steps