doc-src/Intro/foundations.tex
changeset 1865 484956c42436
parent 331 13660d5f6a77
child 1878 ac8e534b4834
equal deleted inserted replaced
1864:9ac4c2240d89 1865:484956c42436
  1060 lifted rule is
  1060 lifted rule is
  1061 \[ \begin{array}{l@{}l}
  1061 \[ \begin{array}{l@{}l}
  1062   \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\
  1062   \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\
  1063            & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1};    \\
  1063            & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1};    \\
  1064            & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1}     \\
  1064            & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1}     \\
  1065   \rbrakk\;& \Imp \Var{R@1}
  1065   \rbrakk\;& \Imp (P\disj P \Imp \Var{R@1})
  1066   \end{array} 
  1066   \end{array} 
  1067 \]
  1067 \]
  1068 Unification takes the simultaneous equations
  1068 Unification takes the simultaneous equations
  1069 $P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding
  1069 $P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding
  1070 $\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$.  The new proof state
  1070 $\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$.  The new proof state