Nuprl - Proof: equal appends case1 2 2 2 1

(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))
10. x2: T List
11. x3: T List
12. ||v||+1||v1||+1
13. [u / (v @ x2)] = [u1 / (v1 @ x3)]
14. z': T List
15. v1 = (v @ z')
16. x2 = (z' @ x3)

z'@0:T List. [u1 / v1] = [u / (v @ z'@0)] & (z' @ x3) = (z'@0 @ x3)

By: InstConcl [z'] THEN Analyze THEN Obvious

Generated subgoals:

None

About:

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