prooftree.tex

\begin{coeden}[label=nythod]{Nested structure of proof tree}
\begin{prooftree}
  {
    to prove={(\exists x)((\forall y)(Py \lif x = y) \land Px) \sststile{}{} (\exists x)(\forall y)(Py \liff x = y)},
    just sep*=3,
    line no sep*=3,
    for root={%
      tikz+={%
        \foreach \i [evaluate=\i as \j using 100*\i/14, evaluate=\i as \k using (11*(\i-7))-30, evaluate=\i as \m using (11*(7-\i))-30] in {13,...,1}
        {%
          \ifnum\i<8
            \coordinate (p\i) at ([yshift=-1 pt,xshift=\k pt]current bounding box.south);
          \else
            \ifnum\i<10
              \coordinate (p\i) at ([yshift=-1 pt,xshift=\m pt]current bounding box.south);
            \else
              \ifnum\i=10
                \coordinate (p\i) at ([yshift=-1 pt,xshift=\k+40 pt]current bounding box.south);
              \else
                \coordinate (p\i) at ([yshift=-1 pt,xshift=\k-52 pt]current bounding box.south);
              \fi
            \fi
          \fi
          \node [fill=WildStrawberry!\j!blue, circle, font=\sffamily\small, text width=12pt, text centered, text=white, inner sep=0pt] at (p\i) {\i};
          \ifnum\i>7
            \ifnum\i<10
              \coordinate (q\i) at ([xshift=\k+40 pt]current bounding box.south |- p\i);
              \node [fill=WildStrawberry!\j!blue, circle, font=\sffamily\small, text width=12pt, text centered, text=white, inner sep=0pt] at (q\i) {\i};
            \else
              \ifnum\i<13
                \ifnum\i>11
                  \coordinate (q\i) at ([xshift=\m pt]current bounding box.south |- p\i);
                  \node [fill=WildStrawberry!\j!blue, circle, font=\sffamily\small, text width=12pt, text centered, text=white, inner sep=0pt] at (q\i) {\i};
                \fi
              \fi
            \fi
          \fi
        }
      },
    },
    for tree={%
      s sep+=30pt,
      if={((level()>=1)&&(proof_tree_rhifo()==1)))}{%
        node options/.wrap pgfmath arg={draw, rounded corners, WildStrawberry!#1!blue}{(level()+proof_tree_toing_by())*100/14},
        fill=white,
        delay={%
          tempcounta=int(level()+proof_tree_toing_by()),
          if={(tempcounta)<=7}{% proof_tree_toing_by is zero here
            nyth/.wrap pgfmath arg={{(!r211111111112111) (!Luu) (!Luuu) (!11) (!Fuu) (!r21111111111)}{#1}{p}}{tempcounta},
          }{%
            if={(tempcounta)>9}{%
              if={n("!uu")==2}{}{%
                tempcounta'+=1,
                if={(n()==1)&&(n_children("!u")==2)}{%
                  nyth/.wrap pgfmath arg={{}{#1}{q}}{tempcounta},
                }{%
                  nyth/.wrap pgfmath arg={{}{#1}{p}}{tempcounta},
                },
              },
            }{%
              if={((tempcounta)==8)&&(n()==1)}{%
                nyth={(!1111) (!llll) (!lllll)}{8}{p},
                !1.nyth={(!111) (!lll) (!llll)}{9}{p},
              }{%
                if={n()==2}{%
                  nyth/.wrap pgfmath arg={{(!1)}{#1}{q}}{tempcounta},
                  tempcounta'+=1,
                  !1.nyth/.wrap pgfmath arg={{(!1)}{#1}{q}}{tempcounta},
                  tempcounta'+=1,
                  !11.nyth/.wrap pgfmath arg={{(!1)}{#1}{p}}{tempcounta},
                }{},
              },
            },
          },
        },
      }{},
    },
  }
  [{(\exists x)((\forall y)(Py \lif x = y) \land Px)}, checked=a, just=Pr., name=pr
    [{\lnot (\exists x)(\forall y)(Py \liff x = y)}, subs=a, just=Conc.~neg., name=neg conc
      [{(\forall y)(Py \lif a = y) \land Pa}, checked, just=$\exists\elim$:pr
        [{(\forall y)(Py \lif a = y)}, subs=b, just=$\land\elim$:!u, name=mark
          [Pa, just=$\land\elim$:!uu, name=simple
            [{\lnot (\forall y)(Py \liff a = y)}, checked=b, just=$\lnot\exists\elim$:neg conc
              [{\lnot (Pb \liff a = b)}, checked, just=$\lnot\forall\elim$:!u
                  [Pb, just=$\liff\elim$:!u, name=to Pb or not to Pb
                    [a \neq b, just=$\liff\elim$:!u
                    [{Pb \lif a = b}, checked, just=$\forall\elim$:mark, move by=1
                        [\lnot Pb, close={:to Pb or not to Pb,!c}, just=$\lif\elim$:!u
                        ]
                        [{a = b}
                          [a \neq a, close={:!c}, just={$=\elim$:{!uuu,!u}}
                          ]
                        ]
                      ]
                    ]
                  ]
                  [\lnot Pb
                    [{a = b}
                      [Pb, just={$=\elim$:{simple,!u}}, close={:to Pb or not to Pb,!c}
                      ]
                    ]
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}
\end{coeden}