Wolfram Cloud Page

WOLFRAM NOTEBOOK

Proof Paths

Withg=

[◼]	TwoWayRuleNestGraph

[x_∘y_<->(y_∘x_)∘y_,(a∘b)∘a,5,GraphLayout"SpringElectricalEmbedding",VertexShapeFunctionAutomatic,ImageSizeScaled[0.8`]],HighlightGraphg,StylePathGraph[FindShortestPath[g,(a∘((b∘a)∘(a∘b)))∘a,b∘a],DirectedEdges->True],

[◼]	MetamathematicsStyleData

["ProofPathStyle"]

In[]:=

[◼]	TwoWayRuleNestGraph

[((a_·b_)·c_)·(a_·((a_·c_)·a_))<->c_,a·b,2,GraphLayout"SpringElectricalEmbedding",VertexShapeFunctionAutomatic]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[((a_·b_)·c_)·(a_·((a_·c_)·a_))<->c_,a·b,3,GraphLayout"SpringElectricalEmbedding",VertexShapeFunctionAutomatic]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[((a_·b_)·c_)·(a_·((a_·c_)·a_))<->c_,a·a,3,GraphLayout"SpringElectricalEmbedding",VertexShapeFunctionAutomatic]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[((a_·b_)·c_)·(a_·((a_·c_)·a_))<->c_,a,3,GraphLayout"SpringElectricalEmbedding",VertexShapeFunctionAutomatic]

Out[]=

In[]:=

TakeSmallestBy[VertexList[%],LeafCount,5]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[((a_·b_)·c_)·(a_·((a_·c_)·a_))<->c_,a·a,1,GraphLayout"SpringElectricalEmbedding"]

Out[]=

S23:

In[]:=

[◼]	TwoWayRuleNestGraph

[a_·a_a_·((a_·a_)·a_),a·a,2,GraphLayout"SpringElectricalEmbedding"]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[a_·a_a_·((a_·a_)·a_),a·a,3,GraphLayout"SpringElectricalEmbedding"]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[a_·a_a_·((a_·a_)·a_),a·a,4,GraphLayout"SpringElectricalEmbedding"]

Out[]=

In[]:=

[◼]	TwoWayRuleNestGraph

[a_·a_a_·((a_·a_)·a_),a·a,5,GraphLayout"SpringElectricalEmbedding",VertexShapeFunction->Automatic]

Out[]=

Notation

In[]:=

Text[Grid[({TraditionalForm/@(#/.Xnor->Equal),TraditionalForm[BooleanConvert[ReleaseHold[#],"BinaryNAND"]/.Nand->CenterDot]})&/@{HoldForm[And][p,q],HoldForm[Or][p,q],HoldForm[Not][p],HoldForm[Implies][p,q],HoldForm[Xnor][p,q],HoldForm[Xor][p,q]},Frame->All,Alignment->{{Left,Center}}]]

Out[]=