doc-src/Intro/foundations.tex
 changeset 1865 484956c42436 parent 331 13660d5f6a77 child 1878 ac8e534b4834
equal 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