Re: [isabelle] A beginner's questionu

On 24.11.2010 05:26, Francisco Ferreira wrote:
Regarding my example I eliminated the problematic rule, and now when I reach the proof of the Pred(Z) rule, I don't know how I prove that Z↓m' is not possible as no rule matches Z

Start with proving which form the "n" in "n↓m" has (i.e.
"Succ n'" or "Pred n'"), instead of proving which form it does not have (Z).

  -- Lars

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.