In[]:=
ProofObject
Logic: Predicate/EquationalLogic
Steps: 272
Theorem: and[congruent[line[a,b],line[a,c]],congruent[1,1]]

Out[]=
ProofObject
Logic: Predicate/EquationalLogic
Steps: 272
Theorem: and[congruent[line[a,b],line[a,c]],congruent[line[b,a],line[b,c]]]

In[]:=
%["ProofDataset"]
Out[]=
In[]:=
pgraph=
Contents cannot be rendered at this time; please try again later
;
In[]:=
Select[VertexList[pgraph],VertexInDegree[pgraph,#]==0&]
Out[]=

∀
{x,y,z}
implies[congruent[line[x,y],line[z,z]],congruent[x,y]],
∀
{x,y,z,u,v,w}
implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]],
∀
{x,y,z}
implies[between[x,y,z],equal[x,y]],
∀
{x,y,z,u,v}
implies[and[between[x,u,z],between[y,v,z]],
∃
a
and[between[u,a,y],between[v,a,x]]],
∀
{x,y,z,u,v}
implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]],
∀
{x,y,z,u,v,w}
implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]],
∀
{x,y,z,a,b,c,u,v}
implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]],
∀
{x,y}
implies[equal[x,y],equal[y,x]],
∀
{x,y,z}
implies[and[equal[x,y],equal[y,z]],equal[x,z]],
∀
x
equal[x,x],
∀
{a,b}
and[a,b]and[b,a],
∀
{a,b}
or[a,b]or[b,a],
∀
{a,b}
and[a,or[b,not[b]]]a,
∀
{a,b}
or[a,and[b,not[b]]]a,
∀
{a,b,c}
and[a,or[b,c]]or[and[a,b],and[a,c]],
∀
{a,b,c}
or[a,and[b,c]]and[or[a,b],or[a,c]],
∀
{a,b}
implies[a,b]or[not[a],b],and[between[x,y,z],between[x,y,w]],or[between[y,z,w],between[y,w,z]]
In[]:=
Length[%]
Out[]=
19
In[]:=
{ForAll[{x,y,z},implies[congruent[line[x,y],line[z,z]],congruent[x,y]]],ForAll[{x,y,z,u,v,w},implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]]],ForAll[{x,y,z},implies[between[x,y,z],equal[x,y]]],ForAll[{x,y,z,u,v},implies[and[between[x,u,z],between[y,v,z]],Exists[a,and[between[u,a,y],between[v,a,x]]]]],ForAll[{x,y,z,u,v},implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]]],ForAll[{x,y,z,u,v,w},implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]]],ForAll[{x,y,z,a,b,c,u,v},implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]]],ForAll[{x,y},implies[equal[x,y],equal[y,x]]],ForAll[{x,y,z},implies[and[equal[x,y],equal[y,z]],equal[x,z]]],ForAll[x,equal[x,x]],ForAll[{a,b},and[a,b]and[b,a]],ForAll[{a,b},or[a,b]or[b,a]],ForAll[{a,b},and[a,or[b,not[b]]]a],ForAll[{a,b},or[a,and[b,not[b]]]a],ForAll[{a,b,c},and[a,or[b,c]]or[and[a,b],and[a,c]]],ForAll[{a,b,c},or[a,and[b,c]]and[or[a,b],or[a,c]]],ForAll[{a,b},implies[a,b]or[not[a],b]],HoldForm[ForAll[{α,β,y,z},implies[Exists[x,implies[and[α[y],β[z]],between[x,y,z]]],Exists[u,implies[and[α[y],β[z]],between[y,u,z]]]]]]}//Length
Out[]=
18
In[]:=
Join[geometry,
∀
{a,b,c}
implies[equal[circle[a,b],circle[a,c]],congruent[line[a,b],line[a,c]]],{equal[circle[a,b],​​circle[a,c]],equal[circle[b,a],circle[b,c]]}]
Out[]=

∀
{x,y,z}
implies[congruent[line[x,y],line[z,z]],congruent[x,y]],
∀
{x,y,z,u,v,w}
implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]],
∀
{x,y,z}
implies[between[x,y,z],equal[x,y]],
∀
{x,y,z,u,v}
implies[and[between[x,u,z],between[y,v,z]],
∃
a
and[between[u,a,y],between[v,a,x]]],
∀
{x,y,z,u,v}
implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]],
∀
{x,y,z,u,v,w}
implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]],
∀
{x,y,z,a,b,c,u,v}
implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]],
∀
{x,y}
implies[equal[x,y],equal[y,x]],
∀
{x,y,z}
implies[and[equal[x,y],equal[y,z]],equal[x,z]],
∀
x
equal[x,x],
∀
{a,b}
and[a,b]and[b,a],
∀
{a,b}
or[a,b]or[b,a],
∀
{a,b}
and[a,or[b,not[b]]]a,
∀
{a,b}
or[a,and[b,not[b]]]a,
∀
{a,b,c}
and[a,or[b,c]]or[and[a,b],and[a,c]],
∀
{a,b,c}
or[a,and[b,c]]and[or[a,b],or[a,c]],
∀
{a,b}
implies[a,b]or[not[a],b],
∀
{a,b,c}
implies[equal[circle[a,b],circle[a,c]],congruent[line[a,b],line[a,c]]],equal[circle[a,b],circle[a,c]],equal[circle[b,a],circle[b,c]]
In[]:=
Length[%]
Out[]=
20
In[]:=
Complement[
∀
{x,y,z}
implies[congruent[line[x,y],line[z,z]],congruent[x,y]],
∀
{x,y,z,u,v,w}
implies[and[congruent[line[x,y],line[z,u]],congruent[line[x,y],line[v,w]]],congruent[line[z,u],line[v,w]]],
∀
{x,y,z}
implies[between[x,y,z],equal[x,y]],
∀
{x,y,z,u,v}
implies[and[between[x,u,z],between[y,v,z]],
∃
a
and[between[u,a,y],between[v,a,x]]],
∀
{x,y,z,u,v}
implies[and[and[and[congruent[line[x,u],line[x,v]],congruent[line[y,u],line[y,v]]],congruent[line[z,u],line[z,v]]],not[equal[u,v]]],or[or[between[x,y,z],between[y,z,x]],between[z,x,y]]],
∀
{x,y,z,u,v,w}
implies[and[and[and[between[x,y,w],congruent[line[x,y],line[y,w]]],and[between[x,u,v],congruent[line[x,u],line[u,v]]]],and[between[y,u,z],congruent[line[y,u],line[z,u]]]],congruent[line[y,z],line[v,w]]],
∀
{x,y,z,a,b,c,u,v}
implies[and[and[and[and[and[and[not[equal[x,y]],between[x,y,z]],between[a,b,c]],congruent[line[x,y],line[a,b]]],congruent[line[y,z],line[b,c]]],congruent[line[x,u],line[a,v]]],congruent[line[y,u],line[b,v]]],congruent[line[z,u],line[c,v]]],
∀
{x,y}
implies[equal[x,y],equal[y,x]],
∀
{x,y,z}
implies[and[equal[x,y],equal[y,z]],equal[x,z]],
∀
x
equal[x,x],
∀
{a,b}
and[a,b]and[b,a],
∀
{a,b}
or[a,b]or[b,a],
∀
{a,b}
and[a,or[b,not[b]]]a,
∀
{a,b}
or[a,and[b,not[b]]]a,
∀
{a,b,c}
and[a,or[b,c]]or[and[a,b],and[a,c]],
∀
{a,b,c}
or[a,and[b,c]]and[or[a,b],or[a,c]],
∀
{a,b}
implies[a,b]or[not[a],b],and[between[x,y,z],between[x,y,w]],or[between[y,z,w],between[y,w,z]],%442]
Out[]=
{and[between[x,y,z],between[x,y,w]],or[between[y,z,w],between[y,w,z]]}
In[]:=
Contents cannot be rendered at this time; please try again later
//VertexCount

Group Theory

Other

Font Stuff

Out[]//InputForm=
Framed[Style[#2, LineColor -> Hue[0.62, 1, 0.48], FrontFaceColor -> Hue[0.62, 1, 0.48], BackFaceColor -> Hue[0.62, 1, 0.48], GraphicsColor -> Hue[0.62, 1, 0.48],
FontColor -> Hue[0.62, 1, 0.48]], Background -> Directive[Opacity[0.2], Hue[0.62, 0.45, 0.87]], FrameMargins -> {{2, 2}, {0, 0}},
FrameStyle -> Directive[Opacity[0.5], Hue[0.62, 0.52, 0.82]], RoundingRadius -> 0]