Step
*
1
of Lemma
opp-side_half-plane-angle-congruence
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. a leftof bp
11. c leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. a # b
17. b # p
18. a' # b'
19. b' # p'
20. a'@0 : Point
21. c1 : Point
22. x1 : Point
23. z1 : Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. p # b
32. b # c
33. p' # b'
34. b' # c'
35. a1 : Point
36. c'@0 : Point
37. x' : Point
38. z' : Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
⊢ ∃a'@0,c'@0,x',z':Point
(B(baa'@0) ∧ B(bcc'@0) ∧ B(b'a'x') ∧ B(b'c'z') ∧ ba'@0 ≅ b'x' ∧ bc'@0 ≅ b'z' ∧ a'@0c'@0 ≅ x'z')
BY
{ ((InstConcl [⌜a'@0⌝;⌜c'@0⌝;⌜x1⌝;⌜z'⌝]⋅ THEN Auto)
THEN ((Assert a'@0 leftof bp BY
(InstLemma `left-convex2` [⌜e⌝;⌜b⌝;⌜p⌝;⌜a⌝;⌜a'@0⌝]⋅ THEN Auto))
THEN (Assert c'@0 leftof pb BY
(InstLemma `left-convex` [⌜e⌝;⌜p⌝;⌜b⌝;⌜c⌝;⌜c'@0⌝]⋅ THEN Auto))
)
THEN (Assert x1 leftof b'p' BY
(InstLemma `left-convex2` [⌜e⌝;⌜b'⌝;⌜p'⌝;⌜a'⌝;⌜x1⌝]⋅ THEN Auto))
THEN (Assert z' leftof p'b' BY
(InstLemma `left-convex` [⌜e⌝;⌜p'⌝;⌜b'⌝;⌜c'⌝;⌜z'⌝]⋅ THEN Auto))) }
1
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. a leftof bp
11. c leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp ≅a a'b'p'
15. pbc ≅a p'b'c'
16. a # b
17. b # p
18. a' # b'
19. b' # p'
20. a'@0 : Point
21. c1 : Point
22. x1 : Point
23. z1 : Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 ≅ b'x1
29. bc1 ≅ b'z1
30. a'@0c1 ≅ x1z1
31. p # b
32. b # c
33. p' # b'
34. b' # c'
35. a1 : Point
36. c'@0 : Point
37. x' : Point
38. z' : Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 ≅ b'x'
44. bc'@0 ≅ b'z'
45. a1c'@0 ≅ x'z'
46. B(baa'@0)
47. B(bcc'@0)
48. B(b'a'x1)
49. B(b'c'z')
50. ba'@0 ≅ b'x1
51. bc'@0 ≅ b'z'
52. a'@0 leftof bp
53. c'@0 leftof pb
54. x1 leftof b'p'
55. z' leftof p'b'
⊢ a'@0c'@0 ≅ x1z'
Latex:
Latex:
1. e : EuclideanPlane
2. b : Point
3. p : Point
4. b' : Point
5. p' : Point
6. a : Point
7. c : Point
8. a' : Point
9. c' : Point
10. a leftof bp
11. c leftof pb
12. a' leftof b'p'
13. c' leftof p'b'
14. abp \mcong{}\msuba{} a'b'p'
15. pbc \mcong{}\msuba{} p'b'c'
16. a \# b
17. b \# p
18. a' \# b'
19. b' \# p'
20. a'@0 : Point
21. c1 : Point
22. x1 : Point
23. z1 : Point
24. B(baa'@0)
25. B(bpc1)
26. B(b'a'x1)
27. B(b'p'z1)
28. ba'@0 \mcong{} b'x1
29. bc1 \mcong{} b'z1
30. a'@0c1 \mcong{} x1z1
31. p \# b
32. b \# c
33. p' \# b'
34. b' \# c'
35. a1 : Point
36. c'@0 : Point
37. x' : Point
38. z' : Point
39. B(bpa1)
40. B(bcc'@0)
41. B(b'p'x')
42. B(b'c'z')
43. ba1 \mcong{} b'x'
44. bc'@0 \mcong{} b'z'
45. a1c'@0 \mcong{} x'z'
\mvdash{} \mexists{}a'@0,c'@0,x',z':Point
(B(baa'@0) \mwedge{} B(bcc'@0) \mwedge{} B(b'a'x') \mwedge{} B(b'c'z') \mwedge{} ba'@0 \mcong{} b'x' \mwedge{} bc'@0 \mcong{} b'z' \mwedge{} a'@0c'@0 \mcong{} x'z')
By
Latex:
((InstConcl [\mkleeneopen{}a'@0\mkleeneclose{};\mkleeneopen{}c'@0\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{} THEN Auto)
THEN ((Assert a'@0 leftof bp BY
(InstLemma `left-convex2` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'@0\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert c'@0 leftof pb BY
(InstLemma `left-convex` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'@0\mkleeneclose{}]\mcdot{} THEN Auto))
)
THEN (Assert x1 leftof b'p' BY
(InstLemma `left-convex2` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (Assert z' leftof p'b' BY
(InstLemma `left-convex` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{} THEN Auto)))
Home
Index