law fin_eq

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1246

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

1246# The last list step: the bytes of the prefix and of the words make the slice.
1247law fin_eq:
1248  for +v1: List<&2, U32>
1249  for +vd: List<&2, U32>
1250  for +us: List<&2, U32>
1251  for +ls: Nat
1252  for +s: Nat
1253  for +hh: Nat
1254  for +qn: Nat
1255  for +np: Nat
1256  for +nn: Nat
1257  for +hv: {v1 == List.append(&2, U32, vd, D.slice(List.take(&2, U32, us, ls), s, hh)) : List<&2, U32>}
1258  for +hq: {qn == Nat.add(s, hh) : Nat}
1259  for +hnp: {np == Nat.sub(nn, hh) : Nat}
1260  for +hhn: {Nat.is_le(hh, nn) == True{} : Bool}
1261  for +hb: {Nat.is_le(Nat.add(s, nn), ls) == True{} : Bool}
1262  {List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, us, qn), np)) == List.append(&2, U32, vd, D.slice(List.take(&2, U32, us, ls), s, nn)) : List<&2, U32>}