Proof of Nuprl Lemma : word-rel-diamond

Step * 1 1 of Lemma word-rel-diamond

1. [X] : Type
2. n : ℕ
3. x : (X + X) List
4. ∀x1:(X + X) List
     (||x1|| < ||x||
     ⇒ (∀y,z:(X + X) List.
           (word-rel(X;x1;y)
           ⇒ word-rel(X;x1;z)
           ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))))
5. y : (X + X) List
6. z : (X + X) List
7. x@0 : X + X
8. y@0 : X + X
9. a1 : (X + X) List
10. b1 : (X + X) List
11. x@0 = -y@0
12. x = (a1 @ [x@0; y@0] @ b1) ∈ ((X + X) List)
13. y = (a1 @ b1) ∈ ((X + X) List)
14. x1 : X + X
15. y1 : X + X
16. a : (X + X) List
17. b : (X + X) List
18. x1 = -y1
19. x = (a @ [x1; y1] @ b) ∈ ((X + X) List)
20. z = (a @ b) ∈ ((X + X) List)
21. (a1 @ [x@0; y@0] @ b1) = (a @ [x1; y1] @ b) ∈ ((X + X) List)

⊢ ((a1 @ b1) = (a @ b) ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;a1 @ b1;w) ∧ word-rel(X;a @ b;w)))

{ ((DVar `a1' THEN All Reduce) THEN DVar `a' THEN All Reduce THEN (RWO "cons_one_one" (-1) THENA Auto) THEN D -1) }

1
1. [X] : Type
2. n : ℕ
3. x : (X + X) List
4. ∀x1:(X + X) List
     (||x1|| < ||x||
     ⇒ (∀y,z:(X + X) List.
           (word-rel(X;x1;y)
           ⇒ word-rel(X;x1;z)
           ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))))
5. y : (X + X) List
6. z : (X + X) List
7. x@0 : X + X
8. y@0 : X + X
9. b1 : (X + X) List
10. x@0 = -y@0
11. x = [x@0; [y@0 / b1]] ∈ ((X + X) List)
12. y = b1 ∈ ((X + X) List)
13. x1 : X + X
14. y1 : X + X
15. b : (X + X) List
16. x1 = -y1
17. x = [x1; [y1 / b]] ∈ ((X + X) List)
18. z = b ∈ ((X + X) List)
19. x@0 = x1 ∈ (X + X)
20. [y@0 / b1] = [y1 / b] ∈ ((X + X) List)
⊢ (b1 = b ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;b1;w) ∧ word-rel(X;b;w)))

2
1. [X] : Type
2. n : ℕ
3. x : (X + X) List
4. ∀x1:(X + X) List
     (||x1|| < ||x||
     ⇒ (∀y,z:(X + X) List.
           (word-rel(X;x1;y)
           ⇒ word-rel(X;x1;z)
           ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))))
5. y : (X + X) List
6. z : (X + X) List
7. x@0 : X + X
8. y@0 : X + X
9. b1 : (X + X) List
10. x@0 = -y@0
11. x = [x@0; [y@0 / b1]] ∈ ((X + X) List)
12. y = b1 ∈ ((X + X) List)
13. x1 : X + X
14. y1 : X + X
15. u : X + X
16. v : (X + X) List
17. b : (X + X) List
18. x1 = -y1
19. x = [u / (v @ [x1; [y1 / b]])] ∈ ((X + X) List)
20. z = [u / (v @ b)] ∈ ((X + X) List)
21. x@0 = u ∈ (X + X)
22. [y@0 / b1] = (v @ [x1; [y1 / b]]) ∈ ((X + X) List)

⊢ (b1 = [u / (v @ b)] ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;b1;w) ∧ word-rel(X;[u / (v @ b)];w)))

3
1. [X] : Type
2. n : ℕ
3. x : (X + X) List
4. ∀x1:(X + X) List
     (||x1|| < ||x||
     ⇒ (∀y,z:(X + X) List.
           (word-rel(X;x1;y)
           ⇒ word-rel(X;x1;z)
           ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))))
5. y : (X + X) List
6. z : (X + X) List
7. x@0 : X + X
8. y@0 : X + X
9. u : X + X
10. v : (X + X) List
11. b1 : (X + X) List
12. x@0 = -y@0
13. x = [u / (v @ [x@0; [y@0 / b1]])] ∈ ((X + X) List)
14. y = [u / (v @ b1)] ∈ ((X + X) List)
15. x1 : X + X
16. y1 : X + X
17. b : (X + X) List
18. x1 = -y1
19. x = [x1; [y1 / b]] ∈ ((X + X) List)
20. z = b ∈ ((X + X) List)
21. u = x1 ∈ (X + X)
22. (v @ [x@0; [y@0 / b1]]) = [y1 / b] ∈ ((X + X) List)

⊢ ([u / (v @ b1)] = b ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;[u / (v @ b1)];w) ∧ word-rel(X;b;w)))

4
1. [X] : Type
2. n : ℕ
3. x : (X + X) List
4. ∀x1:(X + X) List
     (||x1|| < ||x||
     ⇒ (∀y,z:(X + X) List.
           (word-rel(X;x1;y)
           ⇒ word-rel(X;x1;z)
           ⇒ ((y = z ∈ ((X + X) List)) ∨ (∃w:(X + X) List. (word-rel(X;y;w) ∧ word-rel(X;z;w)))))))
5. y : (X + X) List
6. z : (X + X) List
7. x@0 : X + X
8. y@0 : X + X
9. u : X + X
10. v : (X + X) List
11. b1 : (X + X) List
12. x@0 = -y@0
13. x = [u / (v @ [x@0; [y@0 / b1]])] ∈ ((X + X) List)
14. y = [u / (v @ b1)] ∈ ((X + X) List)
15. x1 : X + X
16. y1 : X + X
17. u1 : X + X
18. v1 : (X + X) List
19. b : (X + X) List
20. x1 = -y1
21. x = [u1 / (v1 @ [x1; [y1 / b]])] ∈ ((X + X) List)
22. z = [u1 / (v1 @ b)] ∈ ((X + X) List)
23. u = u1 ∈ (X + X)
24. (v @ [x@0; [y@0 / b1]]) = (v1 @ [x1; [y1 / b]]) ∈ ((X + X) List)
⊢ ([u / (v @ b1)] = [u1 / (v1 @ b)] ∈ ((X + X) List))
∨ (∃w:(X + X) List. (word-rel(X;[u / (v @ b1)];w) ∧ word-rel(X;[u1 / (v1 @ b)];w)))

Latex:

Latex:
1. [X] : Type 2. n : \mBbbN{} 3. x : (X + X) List 4. \mforall{}x1:(X + X) List (||x1|| < ||x|| {}\mRightarrow{} (\mforall{}y,z:(X + X) List. (word-rel(X;x1;y) {}\mRightarrow{} word-rel(X;x1;z) {}\mRightarrow{} ((y = z) \mvee{} (\mexists{}w:(X + X) List. (word-rel(X;y;w) \mwedge{} word-rel(X;z;w))))))) 5. y : (X + X) List 6. z : (X + X) List 7. x@0 : X + X 8. y@0 : X + X 9. a1 : (X + X) List 10. b1 : (X + X) List 11. x@0 = -y@0 12. x = (a1 @ [x@0; y@0] @ b1) 13. y = (a1 @ b1) 14. x1 : X + X 15. y1 : X + X 16. a : (X + X) List 17. b : (X + X) List 18. x1 = -y1 19. x = (a @ [x1; y1] @ b) 20. z = (a @ b) 21. (a1 @ [x@0; y@0] @ b1) = (a @ [x1; y1] @ b) \mvdash{} ((a1 @ b1) = (a @ b)) \mvee{} (\mexists{}w:(X + X) List. (word-rel(X;a1 @ b1;w) \mwedge{} word-rel(X;a @ b;w))) By Latex: ((DVar `a1' THEN All Reduce) THEN DVar `a' THEN All Reduce THEN (RWO "cons\_one\_one" (-1) THENA Auto) THEN D -1) Home Index