equal
deleted
inserted
replaced
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 |