From c505f5761a545a06f2a80c536262e608021c3955 Mon Sep 17 00:00:00 2001 From: Joseph Chan Date: Thu, 17 Aug 2023 12:13:09 +1000 Subject: [PATCH] Fix the proof of zagier_fix in experimental kernel. --- examples/fermat/twosq/windmillScript.sml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/examples/fermat/twosq/windmillScript.sml b/examples/fermat/twosq/windmillScript.sml index a4266da48a..eb18302539 100644 --- a/examples/fermat/twosq/windmillScript.sml +++ b/examples/fermat/twosq/windmillScript.sml @@ -1354,9 +1354,11 @@ Theorem zagier_fixes: !n. n MOD 4 <> 0 ==> fixes zagier (mills n) = {(x,x,z) | n = windmill (x,x,z)} Proof rw[fixes_def, mills_def, EXTENSION, EQ_IMP_THM] >| [ - `x' <> 0` by metis_tac[windmill_with_no_mind] >> + rename1 `windmill (x,y,z)` >> + `x <> 0` by metis_tac[windmill_with_no_mind] >> fs[zagier_fix, windmill_def], - `x' <> 0` by metis_tac[windmill_with_no_mind] >> + rename1 `windmill (x,x,z)` >> + `x <> 0` by metis_tac[windmill_with_no_mind] >> simp[zagier_fix] ] QED