Fix some proofs

xrchz · xrchz · commit 0978a59702cf · 2026-01-13T07:10:08.000Z
diff --git a/compiler/bootstrap/translation/decodeProgScript.sml b/compiler/bootstrap/translation/decodeProgScript.sml
@@ -227,6 +227,7 @@ Proof
   \\ rpt gen_tac \\ strip_tac
   \\ rpt var_eq_tac
   \\ gen_tac \\ disch_then (assume_tac o SYM)
+  \\ rename1 ‘SUC x6’
   \\ Cases_on ‘x6 = 0’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
   \\ ‘n ≠ 1 ∧ n ≠ 0’ by decide_tac
   \\ Cases_on ‘x6 = 1’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
diff --git a/compiler/bootstrap/translation/sexp_parserProgScript.sml b/compiler/bootstrap/translation/sexp_parserProgScript.sml
@@ -201,6 +201,7 @@ val decode_control_side = Q.prove(
   rw[Once(theorem"decode_control_side_def")] \\ rfs[] \\
   rw[num_from_hex_string_alt_length_2] \\
   rfs [num_from_hex_string_alt_intro] \\
+  rename1 `decode_control_side x1` \\
   Cases_on`x1` \\ fs[] \\
   rw[Once(theorem"decode_control_side_def")] \\
   rw[Once(theorem"decode_control_side_def")])
