Wolfram Cloud Document

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]],

∃

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]],

∀

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[]=

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[]=

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]],

∃

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}

∀

{x,y,z,a,b,c,u,v}

∀

{x,y}

implies[equal[x,y],equal[y,x]],

∀

{x,y,z}

implies[and[equal[x,y],equal[y,z]],equal[x,z]],

∀

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[]=

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]],

∃

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}

∀

{x,y,z,a,b,c,u,v}

∀

{x,y}

implies[equal[x,y],equal[y,x]],

∀

{x,y,z}

implies[and[equal[x,y],equal[y,z]],equal[x,z]],

∀

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]