% These definitions - the "preable" of a .dnt file - are from:
%   http://angg.twu.net/dednat5/preamble.lua.html
%   http://angg.twu.net/dednat5/preamble.lua
%                    (find-dn5 "preamble.lua")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}
\def\ifdedundefined#1{\expandafter\ifx\csname ded-#1\endcsname\relax}
\def\ded#1{\ifdedundefined{#1}
    \errmessage{UNDEFINED DEDUCTION: #1}
  \else
    \csname ded-#1\endcsname
  \fi
}
\def\defdiag#1#2{\expandafter\def\csname diag-#1\endcsname{\bfig#2\efig}}
\def\defdiagprep#1#2#3{\expandafter\def\csname diag-#1\endcsname{{#2\bfig#3\efig}}}
\def\ifdiagundefined#1{\expandafter\ifx\csname diag-#1\endcsname\relax}
\def\diag#1{\ifdiagundefined{#1}
    \errmessage{UNDEFINED DIAGRAM: #1}
  \else
    \csname diag-#1\endcsname
  \fi
}
% End of the preamble.


% From: (find-dn5 "begriff.lua" "begriff_preamble")
\usepackage{begriff}
\def\defbegr#1#2{\expandafter\def\csname begr-#1\endcsname{#2}}
\def\ifbegrundefined#1{\expandafter\ifx\csname begr-#1\endcsname\relax}
\def\begr#1{\ifbegrundefined{#1}
    \errmessage{UNDEFINED BEGRIFFSSCHRIFT DIAGRAM: #1}
  \else
    \csname begr-#1\endcsname
  \fi
}
\def\BGrevconditional#1#2{\BGconditional{#2}{#1}}


\defbegr{126?}{ % no hyperlink yet
  \BGassert\BGrevconditional{
    \BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
           \SRchtb f(m_\cc,y_\bb)
        }{\BGnot \SRctb f(y_\cc,m_\bb)
        }
      }{ \SRctb f(x_\cc,y_\bb)
      }
    }{ \SRctb f(x_\cc,m_\bb)
    }
  }{ \SRdIe f(\dd,\ee)
  }}
\defbegr{69-inner}{ % no hyperlink yet
  \BGquant{d}\BGrevconditional{
    \BGquant{a}\BGrevconditional{
       F(\fra)
    }{ f(\frd,\fra)
    }
  }{ F(\frd)
  }}
\defbegr{115-inner}{ % no hyperlink yet
  \BGquant{e}\BGquant{d}\BGrevconditional{
    \BGquant{a}\BGrevconditional{
       (\fra\equiv\fre)
    }{ f(\frd,\fra)
    }
  }{ f(\frd,\fre)
  }}
\defbegr{20}{ % no hyperlink yet
  \BGassert\BGrevconditional{
    \BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
          \BGrevconditional{
             a 
          }{ c 
          }
        }{ d 
        }
      }{ e 
      }
    }{\BGrevconditional{
         a 
      }{ b 
      }
    }
  }{\BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
           b
        }{ c
        }
      }{ d
      }
    }{ e
    }
  }}
\defbegr{20'}{ % no hyperlink yet
  \BGassert\BGrevconditional{
    \BGrevconditional{
      \BGrevconditional{
         b
      }{ d
      }
    }{\BGrevconditional{
         b
      }{ c
      }
    }
  }{\BGrevconditional{
       c
    }{ d
    }
  }}
\defbegr{21}{ % no hyperlink yet
  \BGassert\BGrevconditional{
    \BGrevconditional{
      \BGrevconditional{
         a 
      }{\BGrevconditional{
           b 
        }{ c 
        }
      }
    }{\BGrevconditional{
         c 
      }{ d 
      }
    }
  }{\BGrevconditional{
       a 
    }{\BGrevconditional{
         b 
      }{ d 
      }
    }
  }}
\defbegr{22}{ % no hyperlink yet
  \BGassert\BGrevconditional{
    \BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
          \BGrevconditional{
            \BGrevconditional{
               a 
            }{ c 
            }
          }{ b 
          }
        }{ d 
        }
      }{ e 
      }
    }{ f 
    }
  }{\BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
          \BGrevconditional{
            \BGrevconditional{
               a 
            }{ b 
            }
          }{ c 
          }
        }{ d 
        }
      }{ e 
      }
    }{ f 
    }
  }}
\defbegr{22'}{ % no hyperlink yet
  \BGassert\BGrevconditional{
    \BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
          \BGrevconditional{
             a
          }{ b
          }
        }{ e
        }
      }{ c
      }
    }{\BGrevconditional{
         d
      }{ e
      }
    }
  }{\BGrevconditional{
      \BGrevconditional{
        \BGrevconditional{
           a
        }{ b
        }
      }{ c
      }
    }{ d
    }
  }}