<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<title></title>
</head>
<body>
<div name="messageBodySection">
<div dir="auto">Yes I’m fixing them</div>
</div>
<div name="messageSignatureSection"><br>
<div class="matchFont">Larry</div>
</div>
<div name="messageReplySection">On 23 Oct 2025 at 10:08 +0100, Florian Haftmann <florian.haftmann@cit.tum.de>, wrote:<br>
<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">
isabelle: ee3a09458665 tip<br>
afp: 3805fcdc2e54 tip<br>
<br>
$ isabelle build AutoCorres2_Main<br>
Running AutoCorres2_Main ...<br>
AutoCorres2_Main FAILED (see also "isabelle build_log -H Error<br>
AutoCorres2_Main")<br>
*** Failed to finish proof (line 1810 of<br>
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):<br>
*** goal (1 subgoal):<br>
*** 1. length bs = size_td d ⟹<br>
*** ¬ i < size_td d ⟶<br>
*** bs =<br>
*** bs[i := b]<br>
*** At command "by" (line 1810 of<br>
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")<br>
*** Failed to finish proof (line 1567 of<br>
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):<br>
*** goal (1 subgoal):<br>
*** 1. length bs = size_td d ⟹<br>
*** ¬ i < size_td d ⟶<br>
*** bs =<br>
*** bs[i := b]<br>
*** At command "by" (line 1567 of<br>
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")<br>
*** Failed to finish proof (line 951 of<br>
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):<br>
*** goal (1 subgoal):<br>
*** 1. ⟦length bs = size_td s; n ≤ x; x < n + size_td s;<br>
*** size_td s + n ≤ size_of TYPE('a); length pfx = n;<br>
*** length sfx = size_of TYPE('a) - (n + size_td s)⟧<br>
*** ⟹ ¬ x - n < size_td s ⟶<br>
*** bs[0 := b] = bs ∧<br>
*** sfx =<br>
*** sfx[0 := b]<br>
*** At command "by" (line 951 of<br>
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")<br>
<br>
Florian<br>
</blockquote>
</div>
</body>
</html>