Nuprl - Proof: append one one 1

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

1. T: Type
2. x: T List
3. z: T List
4. y: T List
5. w: T List
6. ||x|| = ||z|| ||y|| = ||w||
7. (x @ y) = (z @ w)
8. e: T List
9. x = (z @ e) & w = (e @ y) z = (x @ e) & y = (e @ w)

e = nil

By: Analyze -2

Generated subgoals:

1 8. x = (z @ nil) & w = (nil @ y) z = (x @ nil) & y = (nil @ w)
nil = nil T List 1 step

2 8. u: T
9. v: T List
10. x = (z @ [u / v]) & w = ([u / v] @ y) z = (x @ [u / v]) & y = ([u / v] @ w)
[u / v] = nil 1 step

About:

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

1	8. `x = (z @ nil) & w = (nil @ y) z = (x @ nil) & y = (nil @ w)` `nil = nil T List`	1 step

2	8. `u:` `T` 9. `v:` `T List` 10. `x = (z @ [u / v]) & w = ([u / v] @ y) z = (x @ [u / v]) & y = ([u / v] @ w)` `[u / v] = nil`	1 step