Nuprl - Proof: l before append iff 1

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

1. T: Type
2. A: T List
3. B: T List
4. x: T
5. y: T
6. A',B':T List. [x; y] = (A' @ B') & A' A & B' B

[x; y] A [x; y] B (x A) & (y B)

By: ExRepD THEN Analyze -5 THEN All Reduce

Generated subgoals:

1 6. B': T List
7. [x; y] = B'
8. nil A
9. B' B
[x; y] A [x; y] B (x A) & (y B) 1 step

2 6. u: T
7. v: T List
8. B': T List
9. [x; y] = [u / (v @ B')]
10. [u / v] A
11. B' B
[x; y] A [x; y] B (x A) & (y B) 4 steps

About:

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

1	6. `B':` `T List` 7. `[x; y] = B'` 8. `nil A` 9. `B' B` `[x; y] A [x; y] B (x A) & (y B)`	1 step

2	6. `u:` `T` 7. `v:` `T List` 8. `B':` `T List` 9. `[x; y] = [u / (v @ B')]` 10. `[u / v] A` 11. `B' B` `[x; y] A [x; y] B (x A) & (y B)`	4 steps