Step
*
1
of Lemma
geo-orientation_wf
1. g : self:GeometryPrimitives
"Bstable":∀[a,b,c:Point]. Stable{a_b_c}
"Estable":∀[a,b,c,d:Point]. Stable{ab ≅ cd}
"Ssquashstable":∀a,b:Point. SqStable(a ≠ b)
"Lsquashstable":∀a,b,c:Point. SqStable(a leftof bc)
"Lorsquashstable":∀a,b,c:Point. SqStable(a leftof bc ∨ a leftof cb)
"SepOr":∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (a ≠ c ∨ b ≠ c)
"nontrivial":∃a:Point. (∃b:{Point| a ≠ b})
"SS":∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} . (∃x:{Point| (Colinear(a;b;x) ∧ u_x_v)})
"SC":∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (∃x:{Point| (a_b_x ∧ bx ≅ bc)}) ⋂ x:Atom
⟶ if x =a "CC"
then ∀a,b:Point. ∀c:{c:Point| a ≠ c} . ∀d:Point.
∀[p:{p:Point| ab ≅ ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd ≅ cq ∧ ab ≥ aq} ].
∃u:{u:Point| ab ≅ au ∧ cd ≅ cu}
(∃v:{Point| ((ab ≅ av ∧ cd ≅ cv) ∧ ((ab > aq ∧ cd > cp) ⇒ (u leftof ac ∧ v leftof ca)))})
else Top
fi
2. g ∈ GeometryPrimitives
3. a : Point
4. b : Point
5. c : Point
6. a # bc
7. g ∈ EuclideanPlaneStructure
8. g."Bstable" ∈ ∀[a,b,c:Point]. Stable{a_b_c}
9. g."Estable" ∈ ∀[a,b,c,d:Point]. Stable{ab ≅ cd}
10. g."Ssquashstable" ∈ ∀a,b:Point. SqStable(a ≠ b)
11. g."Lsquashstable" ∈ ∀a,b,c:Point. SqStable(a leftof bc)
12. g."Lorsquashstable" ∈ ∀a,b,c:Point. SqStable(a leftof bc ∨ a leftof cb)
13. g."SepOr" ∈ ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (a ≠ c ∨ b ≠ c)
14. g."nontrivial" ∈ ∃a:Point. (∃b:{Point| a ≠ b})
15. g."SS" ∈ ∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} . (∃x:{Point| (Colinear(a;b;x) ∧ u_x_v)}\000C)
16. g."SC" ∈ ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (∃x:{Point| (a_b_x ∧ bx ≅ bc)})
17. g."CC" ∈ ∀a,b:Point. ∀c:{c:Point| a ≠ c} . ∀d:Point.
∀[p:{p:Point| ab ≅ ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd ≅ cq ∧ ab ≥ aq} ].
∃u:{u:Point| ab ≅ au ∧ cd ≅ cu}
(∃v:{Point| ((ab ≅ av ∧ cd ≅ cv) ∧ ((ab > aq ∧ cd > cp) ⇒ (u leftof ac ∧ v leftof ca)))})
⊢ ⋅ ∈ ↓a leftof bc ∨ a leftof cb
BY
{ Fold `geo-lsep` 0 }
1
1. g : self:GeometryPrimitives
"Bstable":∀[a,b,c:Point]. Stable{a_b_c}
"Estable":∀[a,b,c,d:Point]. Stable{ab ≅ cd}
"Ssquashstable":∀a,b:Point. SqStable(a ≠ b)
"Lsquashstable":∀a,b,c:Point. SqStable(a leftof bc)
"Lorsquashstable":∀a,b,c:Point. SqStable(a leftof bc ∨ a leftof cb)
"SepOr":∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (a ≠ c ∨ b ≠ c)
"nontrivial":∃a:Point. (∃b:{Point| a ≠ b})
"SS":∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} . (∃x:{Point| (Colinear(a;b;x) ∧ u_x_v)})
"SC":∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (∃x:{Point| (a_b_x ∧ bx ≅ bc)}) ⋂ x:Atom
⟶ if x =a "CC"
then ∀a,b:Point. ∀c:{c:Point| a ≠ c} . ∀d:Point.
∀[p:{p:Point| ab ≅ ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd ≅ cq ∧ ab ≥ aq} ].
∃u:{u:Point| ab ≅ au ∧ cd ≅ cu}
(∃v:{Point| ((ab ≅ av ∧ cd ≅ cv) ∧ ((ab > aq ∧ cd > cp) ⇒ (u leftof ac ∧ v leftof ca)))})
else Top
fi
2. g ∈ GeometryPrimitives
3. a : Point
4. b : Point
5. c : Point
6. a # bc
7. g ∈ EuclideanPlaneStructure
8. g."Bstable" ∈ ∀[a,b,c:Point]. Stable{a_b_c}
9. g."Estable" ∈ ∀[a,b,c,d:Point]. Stable{ab ≅ cd}
10. g."Ssquashstable" ∈ ∀a,b:Point. SqStable(a ≠ b)
11. g."Lsquashstable" ∈ ∀a,b,c:Point. SqStable(a leftof bc)
12. g."Lorsquashstable" ∈ ∀a,b,c:Point. SqStable(a leftof bc ∨ a leftof cb)
13. g."SepOr" ∈ ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (a ≠ c ∨ b ≠ c)
14. g."nontrivial" ∈ ∃a:Point. (∃b:{Point| a ≠ b})
15. g."SS" ∈ ∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} . (∃x:{Point| (Colinear(a;b;x) ∧ u_x_v)}\000C)
16. g."SC" ∈ ∀a:Point. ∀b:{b:Point| a ≠ b} . ∀c:Point. (∃x:{Point| (a_b_x ∧ bx ≅ bc)})
17. g."CC" ∈ ∀a,b:Point. ∀c:{c:Point| a ≠ c} . ∀d:Point.
∀[p:{p:Point| ab ≅ ap ∧ cd ≥ cp} ]. ∀[q:{q:Point| cd ≅ cq ∧ ab ≥ aq} ].
∃u:{u:Point| ab ≅ au ∧ cd ≅ cu}
(∃v:{Point| ((ab ≅ av ∧ cd ≅ cv) ∧ ((ab > aq ∧ cd > cp) ⇒ (u leftof ac ∧ v leftof ca)))})
⊢ ⋅ ∈ ↓a # bc
Latex:
Latex:
1. g : self:GeometryPrimitives
"Bstable":\mforall{}[a,b,c:Point]. Stable\{a\_b\_c\}
"Estable":\mforall{}[a,b,c,d:Point]. Stable\{ab \00D0 cd\}
"Ssquashstable":\mforall{}a,b:Point. SqStable(a \mneq{} b)
"Lsquashstable":\mforall{}a,b,c:Point. SqStable(a leftof bc)
"Lorsquashstable":\mforall{}a,b,c:Point. SqStable(a leftof bc \mvee{} a leftof cb)
"SepOr":\mforall{}a:Point. \mforall{}b:\{b:Point| a \mneq{} b\} . \mforall{}c:Point. (a \mneq{} c \mvee{} b \mneq{} c)
"nontrivial":\mexists{}a:Point. (\mexists{}b:\{Point| a \mneq{} b\})
"SS":\mforall{}a,b:Point. \mforall{}u:\{u:Point| u leftof ab\} . \mforall{}v:\{v:Point| v leftof ba\} .
(\mexists{}x:\{Point| (Colinear(a;b;x) \mwedge{} u\_x\_v)\})
"SC":\mforall{}a:Point. \mforall{}b:\{b:Point| a \mneq{} b\} . \mforall{}c:Point. (\mexists{}x:\{Point| (a\_b\_x \mwedge{} bx \00D0 bc)\}) \mcap{} x:Atom
{}\mrightarrow{} if x =a "CC"
then \mforall{}a,b:Point. \mforall{}c:\{c:Point| a \mneq{} c\} . \mforall{}d:Point.
\mforall{}[p:\{p:Point| ab \00D0 ap \mwedge{} cd \mgeq{} cp\} ]. \mforall{}[q:\{q:Point| cd \00D0 cq \mwedge{} ab \mgeq{} aq\} ].
\mexists{}u:\{u:Point| ab \00D0 au \mwedge{} cd \00D0 cu\}
(\mexists{}v:\{Point| ((ab \00D0 av \mwedge{} cd \00D0 cv)
\mwedge{} ((ab > aq \mwedge{} cd > cp) {}\mRightarrow{} (u leftof ac \mwedge{} v leftof ca)))\})
else Top
fi
2. g \mmember{} GeometryPrimitives
3. a : Point
4. b : Point
5. c : Point
6. a \# bc
7. g \mmember{} EuclideanPlaneStructure
8. g."Bstable" \mmember{} \mforall{}[a,b,c:Point]. Stable\{a\_b\_c\}
9. g."Estable" \mmember{} \mforall{}[a,b,c,d:Point]. Stable\{ab \00D0 cd\}
10. g."Ssquashstable" \mmember{} \mforall{}a,b:Point. SqStable(a \mneq{} b)
11. g."Lsquashstable" \mmember{} \mforall{}a,b,c:Point. SqStable(a leftof bc)
12. g."Lorsquashstable" \mmember{} \mforall{}a,b,c:Point. SqStable(a leftof bc \mvee{} a leftof cb)
13. g."SepOr" \mmember{} \mforall{}a:Point. \mforall{}b:\{b:Point| a \mneq{} b\} . \mforall{}c:Point. (a \mneq{} c \mvee{} b \mneq{} c)
14. g."nontrivial" \mmember{} \mexists{}a:Point. (\mexists{}b:\{Point| a \mneq{} b\})
15. g."SS" \mmember{} \mforall{}a,b:Point. \mforall{}u:\{u:Point| u leftof ab\} . \mforall{}v:\{v:Point| v leftof ba\} .
(\mexists{}x:\{Point| (Colinear(a;b;x) \mwedge{} u\_x\_v)\})
16. g."SC" \mmember{} \mforall{}a:Point. \mforall{}b:\{b:Point| a \mneq{} b\} . \mforall{}c:Point. (\mexists{}x:\{Point| (a\_b\_x \mwedge{} bx \00D0 bc)\})
17. g."CC" \mmember{} \mforall{}a,b:Point. \mforall{}c:\{c:Point| a \mneq{} c\} . \mforall{}d:Point.
\mforall{}[p:\{p:Point| ab \00D0 ap \mwedge{} cd \mgeq{} cp\} ]. \mforall{}[q:\{q:Point| cd \00D0 cq \mwedge{} ab \mgeq{} aq\} ].
\mexists{}u:\{u:Point| ab \00D0 au \mwedge{} cd \00D0 cu\}
(\mexists{}v:\{Point| ((ab \00D0 av \mwedge{} cd \00D0 cv)
\mwedge{} ((ab > aq \mwedge{} cd > cp) {}\mRightarrow{} (u leftof ac \mwedge{} v leftof ca)))\})
\mvdash{} \mcdot{} \mmember{} \mdownarrow{}a leftof bc \mvee{} a leftof cb
By
Latex:
Fold `geo-lsep` 0
Home
Index