Some examples of subformula trees.
We use the maps from the previous section to draw some subformulas trees with and without sign, with and without colors.
In[238]:=
A subformula tree.
In[239]:=
![ShowSubformulaTree[F1] ;](../HTMLFiles/index_226.gif){kind=small}
![[Graphics:../HTMLFiles/index_227.gif]](../HTMLFiles/index_227.gif)
In[240]:=
![ShowSubformulaTree[F4, PosSign] ;](../HTMLFiles/index_228.gif){kind=small}
![[Graphics:../HTMLFiles/index_229.gif]](../HTMLFiles/index_229.gif)
A subjudgement coloured tree.
In[241]:=
![ShowColouredTree[Impl["MP", Ex["x", "f(x)<=f(x+27)"]], PosSign] ;](../HTMLFiles/index_230.gif){kind=small}
![[Graphics:../HTMLFiles/index_231.gif]](../HTMLFiles/index_231.gif)
In[242]:=
![ShowColouredTree[Unfold["MP"], PosSign] ;](../HTMLFiles/index_232.gif){kind=small}
![[Graphics:../HTMLFiles/index_233.gif]](../HTMLFiles/index_233.gif)
Created by Mathematica (October 17, 2006)