law step

lawful-bytes@0.1.1.0 · proof_fast_append.bend:755

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
import lawful-arrays@0.1.0.0/proof_index.bend as I

755law step:
756  for +ts: P.Tree<U32>
757  for +e: Nat
758  for +td: P.Tree<U32>
759  for +d: Nat
760  for +p: U32
761  for +lo: U32
762  for +si: U32
763  for +di: U32
764  for +sh: Nat
765  for +l1: Nat
766  for +qn: Nat
767  for +r: Nat
768  for +o: Nat
769  for +np: Nat
770  for +v1: List<&2, U32>
771  for +m: Nat
772  for +hfs: {A.full(U32, P.fromT(U32, ts), e) == True{} : Bool}
773  for +hes: {Nat.is_le(e, 29n) == True{} : Bool}
774  for +hfd: {A.full(U32, P.fromT(U32, td), d) == True{} : Bool}
775  for +hdd: {Nat.is_le(d, 29n) == True{} : Bool}
776  for +hdi: {Nat.mul(U32.to_nat(di), 4n) == Nat.add(l1, o) : Nat}
777  for +hsi: {Nat.add(Nat.mul(U32.to_nat(si), 4n), r) == Nat.add(qn, o) : Nat}
778  for +hp: {U32.to_nat(p) == Nat.add(U32.to_nat(si), 1n) : Nat}
779  for +hlo: {lo == C.WD(ts, si) : U32}
780  for +hsh: {sh == Nat.mul(8n, r) : Nat}
781  for +hr: {Nat.is_lt(r, 4n) == True{} : Bool}
782  for +hq: {Nat.is_le(Nat.add(qn, np), Nat.mul(4n, Nat.pow(2n, e))) == True{} : Bool}
783  for +hl: {Nat.is_le(Nat.add(l1, np), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
784  for +ho: {Nat.is_lt(o, np) == True{} : Bool}
785  for +hm: {Nat.is_le(m, 4n) == True{} : Bool}
786  for +hmv: {Nat.is_le(Nat.add(o, m), np) == True{} : Bool}
787  for +hinv: {List.take(&2, U32, US(td), Nat.add(l1, o)) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), o)) : List<&2, U32>}
788  {List.take(&2, U32, US(I.set_tree(U32, td, di, U32.or(U32.shrn(lo, sh), U32.shln(C.WD(ts, p), Nat.sub(32n, sh))))), Nat.add(l1, Nat.add(o, m))) == List.append(&2, U32, v1, List.take(&2, U32, List.drop(&2, U32, US(ts), qn), Nat.add(o, m))) : List<&2, U32>}