Problem in AFP / AutoCorres2_Main

[Florian Haftmann]

isabelle: ee3a09458665 tip
afp: 3805fcdc2e54 tip

$ isabelle build AutoCorres2_Main
Running AutoCorres2_Main ...
AutoCorres2_Main FAILED (see also "isabelle build_log -H Error 
AutoCorres2_Main")
*** Failed to finish proof (line 1810 of 
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
***  1. length bs = size_td d ⟹
***     ¬ i < size_td d ⟶
***     bs =
***     bs[i := b]
*** At command "by" (line 1810 of 
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")
*** Failed to finish proof (line 1567 of 
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
***  1. length bs = size_td d ⟹
***     ¬ i < size_td d ⟶
***     bs =
***     bs[i := b]
*** At command "by" (line 1567 of 
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")
*** Failed to finish proof (line 951 of 
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy"):
*** goal (1 subgoal):
***  1. ⟦length bs = size_td s; n ≤ x; x < n + size_td s;
***      size_td s + n ≤ size_of TYPE('a); length pfx = n;
***      length sfx = size_of TYPE('a) - (n + size_td s)⟧
***     ⟹ ¬ x - n < size_td s ⟶
***        bs[0 := b] = bs ∧
***        sfx =
***        sfx[0 := b]
*** At command "by" (line 951 of 
"$AFP/AutoCorres2/c-parser/umm_heap/Padding_Equivalence.thy")

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 25429 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251023/5774b736/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251023/5774b736/attachment-0001.sig>