Proof of Nuprl Lemma : lt-angle-irrefl

Step * 4 of Lemma lt-angle-irrefl

1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
⊢ False
BY

{ ((((Assert a ≠ b BY ((D 8 THEN ExRepD) THEN Auto)) THEN (Assert b ≠ c BY ((D 8 THEN ExRepD) THEN Auto)))

    THEN (Assert x ≠ y BY
                ((D 9 THEN ExRepD) THEN Auto))
    THEN (Assert y ≠ z BY
                ((D 9 THEN ExRepD) THEN Auto)))
   THEN (gColinearCases (-7) THEN Auto)
   THEN gColinearCases (-6)
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c ≡ a
19. z ≡ x
⊢ False

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c ≡ a
19. x-y-z
⊢ False

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c ≡ a
19. y-z-x
⊢ False

4
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c ≡ a
19. z-x-y
⊢ False

5
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. a-b-c
19. z ≡ x
⊢ False

6
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. a-b-c
19. x-y-z
⊢ False

7
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. a-b-c
19. y-z-x
⊢ False

8
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. a-b-c
19. z-x-y
⊢ False

9
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. b-c-a
19. z ≡ x
⊢ False

10
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. b-c-a
19. x-y-z
⊢ False

11
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. b-c-a
19. y-z-x
⊢ False

12
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. b-c-a
19. z-x-y
⊢ False

13
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c-a-b
19. z ≡ x
⊢ False

14
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c-a-b
19. x-y-z
⊢ False

15
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c-a-b
19. y-z-x
⊢ False

16
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc < xyz
9. xyz < abc
10. ¬a # bc
11. Colinear(a;b;c)
12. ¬x # yz
13. Colinear(x;y;z)
14. a ≠ b
15. b ≠ c
16. x ≠ y
17. y ≠ z
18. c-a-b
19. z-x-y
⊢ False

Latex:

Latex:
1. e : EuclideanPlane 2. a : Point 3. b : Point 4. c : Point 5. x : Point 6. y : Point 7. z : Point 8. abc < xyz 9. xyz < abc 10. \mneg{}a \# bc 11. Colinear(a;b;c) 12. \mneg{}x \# yz 13. Colinear(x;y;z) \mvdash{} False By Latex: ((((Assert a \mneq{} b BY ((D 8 THEN ExRepD) THEN Auto)) THEN (Assert b \mneq{} c BY ((D 8 THEN ExRepD) THEN Auto)) ) THEN (Assert x \mneq{} y BY ((D 9 THEN ExRepD) THEN Auto)) THEN (Assert y \mneq{} z BY ((D 9 THEN ExRepD) THEN Auto))) THEN (gColinearCases (-7) THEN Auto) THEN gColinearCases (-6) THEN Auto) Home Index