law gtake

lawful-bytes@0.1.1.0 · proof_grow.bend:414

import Base
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-arrays@0.1.0.0/defs.bend as A
import lawful-arrays@0.1.0.0/proof_tree.bend as P

414# The loop copies words i .. i+n-1 of t.
415law gtake:
416  for +n: Nat
417  for +t: P.Tree<U32>
418  for +td: P.Tree<U32>
419  for +i: U32
420  for +d: Nat
421  for +e: Nat
422  for +hft: {A.full(U32, P.fromT(U32, t), d) == True{} : Bool}
423  for +hfd: {A.full(U32, P.fromT(U32, td), e) == True{} : Bool}
424  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
425  for +he: {Nat.is_le(d, e) == True{} : Bool}
426  for +he29: {Nat.is_le(e, 29n) == True{} : Bool}
427  for +hn: {Nat.is_le(Nat.add(U32.to_nat(i), n), Nat.pow(2n, d)) == True{} : Bool}
428  for +hinv: {List.take(&2, U32, C.WL(td), U32.to_nat(i)) == List.take(&2, U32, C.WL(t), U32.to_nat(i)) : List<&2, U32>}
429  {List.take(&2, U32, C.WL(gtree(n, t, td, i)), Nat.add(U32.to_nat(i), n)) == List.take(&2, U32, C.WL(t), Nat.add(U32.to_nat(i), n)) : List<&2, U32>}