def fav.go

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1576

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/fast.bend as FA
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-bytes@0.1.1.0/proof_append.bend as X
import lawful-words@0.1.0.0/proof_nat.bend as N
import lawful-arrays@0.1.0.0/proof_base.bend as AB
import lawful-arrays@0.1.0.0/proof_tree.bend as P

1576def fav.go(+ld: U32, +td: P.Tree<U32>, +ls: U32, +ts: P.Tree<U32>, +d: Nat, +e: Nat, +s: U32, +n: U32,
1577  +hd: {D.ok(C.BT(ld, td), d) == True{} : Bool},
1578  +he: {D.ok(C.BT(ls, ts), e) == True{} : Bool},
1579  +hs: {Nat.is_le(Nat.add(U32.to_nat(s), U32.to_nat(n)), D.size(C.BT(ls, ts))) == True{} : Bool},
1580  +hc: {Nat.is_le(Nat.add(D.size(C.BT(ld, td)), U32.to_nat(n)), D.cap(C.BT(ld, td))) == True{} : Bool},
1581  m: C.BMirror(D1(ld, td, ls, ts, s, n))) ->
1582  {D.view(Pair.fst(D.Bytes, D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n))) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), U32.to_nat(s), U32.to_nat(n))) : List<&2, U32>}:
1583  (+l1, m2) = m
1584  (+t1, +e1) = m2
1585  +sn = U32.to_nat(s)
1586  +nn = U32.to_nat(n)
1587  +hhn = U32.to_nat(HH(ld, n))
1588  +L1 = U32.to_nat(l1)
1589  +NP = U32.to_nat(NPw(ld, n))
1590  +RHS = List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, nn))
1591  +el = el1(ld, td, ls, ts, d, s, n, l1, t1, e1, hd, hc)
1592  +hl0 = hlen0(ld, td, l1, d, n, el, hd, hc)
1593  +hss = N.le_trans(Nat.add(sn, hhn), Nat.add(sn, nn), U32.to_nat(ls), N.le_add_mono_l(sn, hhn, nn, hh_le(ld, n)), hs)
1594  +vd1 = AB.subst(D.Bytes, y => {D.view(y) == List.append(&2, U32, D.view(C.BT(ld, td)), D.slice(D.view(C.BT(ls, ts)), sn, hhn)) : List<&2, U32>},
1595    D1(ld, td, ls, ts, s, n), C.BT(l1, t1), Equal.sym(D.Bytes, C.BT(l1, t1), D1(ld, td, ls, ts, s, n), e1),
1596    X.append_view_t(ld, td, ls, ts, d, e, s, HH(ld, n), hd, he, hss, hc_h(ld, td, n, hc)))
1597  +eq = C.add_fits(s, HH(ld, n), e, C.ok_d(ls, ts, e, he),
1598    N.le_trans(Nat.add(sn, hhn), U32.to_nat(ls), Nat.mul(4n, Nat.pow(2n, e)), hss, C.ok_len(ls, ts, e, he)))
1599  %Equal.sym(D.Bytes & D.Bytes, FA.append(C.BT(ld, td), C.BT(ls, ts), s, n), (C.BT(U32.add(l1, NPw(ld, n)), TF(ld, ts, s, n, l1, t1)), C.BT(ls, ts)),
1600    fa_eq(ld, td, ls, ts, s, n, l1, t1, e1)) :
1601    {D.view(Pair.fst(D.Bytes, D.Bytes, _)) == RHS : List<&2, U32>}
1602  %Equal.sym(Nat, U32.to_nat(U32.add(l1, NPw(ld, n))), Nat.add(L1, NP), C.add_fits(l1, NPw(ld, n), d, C.ok_d(ld, td, d, hd), hl0)) :
1603    {List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), _) == RHS : List<&2, U32>}
1604  Equal.trans(List<&2, U32>, List.take(&2, U32, US(TF(ld, ts, s, n, l1, t1)), Nat.add(L1, NP)),
1605    List.append(&2, U32, D.view(C.BT(l1, t1)), List.take(&2, U32, List.drop(&2, U32, US(ts), U32.to_nat(QQ(ld, s, n))), NP)), RHS,
1606    avc(Nat.is_lt(U32.to_nat(H0(ld)), nn), ld, td, ls, ts, d, e, s, n, l1, t1, {==}, e1, hd, he, hs, hc),
1607    fin_eq(D.view(C.BT(l1, t1)), D.view(C.BT(ld, td)), US(ts), U32.to_nat(ls), sn, hhn, U32.to_nat(QQ(ld, s, n)), NP, nn, vd1, eq, enp(ld, n), hh_le(ld, n), hs))