Nuprl - Proof: sublist append iff 1

(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)

B:T List. [u / v] [u1 / (v1 @ B)] (A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B)

By: RWO Thm* x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 0

Generated subgoals:

1 10. B: T List
11. u = u1 & v v1 @ B [u / v] v1 @ B
A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B 6 steps

2 10. B: T List
11. A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B
u = u1 & v v1 @ B [u / v] v1 @ B 8 steps

About:

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

1	10. `B:` `T List` 11. `u = u1 & v v1 @ B [u / v] v1 @ B` `A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B`	6 steps

2	10. `B:` `T List` 11. `A',B':T List. [u / v] = (A' @ B') & A' [u1 / v1] & B' B` `u = u1 & v v1 @ B [u / v] v1 @ B`	8 steps