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

		Statement	Proof
CriticalPairLemma	1	and[x1,or[x2,x3]]or[and[x2,x1],and[x1,x3]]	Construct	{EquationalizedAxiom,6}
			Orientation	-1
			9 total ›
CriticalPairLemma	2	and[x1,or[x2,x3]]or[and[x1,x2],and[x3,x1]]	Construct	{EquationalizedAxiom,6}
			Orientation	-1
			9 total ›
CriticalPairLemma	3	or[x1,and[and[x2,not[x2]],x3]]and[x1,or[x1,x3]]	Construct	{EquationalizedAxiom,7}
			Orientation	1
			9 total ›
CriticalPairLemma	4	((x1&&!x1)\|\|x2)x2	Construct	{EquationalizedAxiom,8}
			Orientation	{-1,1}
			9 total ›
CriticalPairLemma	5	x1(x1&&equal[x2,x2])	Construct	{EquationalizedAxiom,4}
			Orientation	-1
			9 total ›
CriticalPairLemma	6	equal[x1,x1]equal[x2,x2]	Construct	{EquationalizedAxiom,10}
			Orientation	{-1,1}
			9 total ›
SubstitutionLemma	1	equal[ELProver`Const2,ELProver`Const2]equal[circle[b,a],circle[b,c]]	Input	{EquationalizedAxiom,11}
			Position	1
			6 total ›
SubstitutionLemma	2	equal[ELProver`Const2,ELProver`Const2]equal[circle[a,b],circle[a,c]]	Input	{EquationalizedAxiom,12}
			Position	1
			6 total ›
SubstitutionLemma	3	equal[ELProver`Const2,ELProver`Const2]implies[equal[x1,x2],equal[x2,x1]]	Input	{EquationalizedAxiom,13}
			Position	1
			6 total ›
SubstitutionLemma	4	equal[ELProver`Const2,ELProver`Const2]implies[equal[circle[x1,x2],circle[x1,x3]],congruent[line[x1,x2],line[x1,x3]]]	Input	{EquationalizedAxiom,14}
			Position	1
			6 total ›
rows 41–50 of 272

In[]:=

pgraph=

;

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]

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]