Nuprl - Proof: sublist append iff 1 2 2

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

1. T: Type
2. C: T List
3. u: T
4. v: T List
5. A,B:T List. v A @ B (A',B':T List. v = (A' @ B') & A' A & B' B)
6. A: T List
7. u1: T
8. v1: T List
9. B:T List. [u / v] v1 @ B (A',B':T List. [u / v] = (A' @ B') & A' v1 & B' B)
10. B: T List
11. u2: T
12. v2: T List
13. B': T List
14. [u / v] = [u2 / (v2 @ B')]
15. [u2 / v2] [u1 / v1]
16. B' B

u = u1 & v v1 @ B [u / v] v1 @ B

By: RWO Thm* x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 -2 THEN Analyze -2

Generated subgoals:

1 15. u2 = u1 & v2 v1
16. B' B
u = u1 & v v1 @ B [u / v] v1 @ B 4 steps

2 15. [u2 / v2] v1
16. B' B
u = u1 & v v1 @ B [u / v] v1 @ B 1 step

About:

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

1	15. `u2 = u1 & v2 v1` 16. `B' B` `u = u1 & v v1 @ B [u / v] v1 @ B`	4 steps

2	15. `[u2 / v2] v1` 16. `B' B` `u = u1 & v v1 @ B [u / v] v1 @ B`	1 step