Nuprl - Proof: equal appends eq 1

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

1. T: Type
2. x1: T List
3. z: T List
4. x2: T List
5. x3: T List
6. ||x1|| = ||z||
7. (x1 @ x2) = (z @ x3)
8. z': T List
9. z = (x1 @ z')
10. x2 = (z' @ x3)

x1 = z & x2 = x3

By: Analyze -3

Generated subgoals:

1 8. z = (x1 @ nil)
9. x2 = (nil @ x3)
x1 = z & x2 = x3 2 steps

2 8. u: T
9. v: T List
10. z = (x1 @ [u / v])
11. x2 = ([u / v] @ x3)
x1 = z & x2 = x3 1 step

About:

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

1	8. `z = (x1 @ nil)` 9. `x2 = (nil @ x3)` `x1 = z & x2 = x3`	2 steps

2	8. `u:` `T` 9. `v:` `T List` 10. `z = (x1 @ [u / v])` 11. `x2 = ([u / v] @ x3)` `x1 = z & x2 = x3`	1 step