Tree.complete_step: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as Tree
Lines 191-208 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&start_line=191&end_line=208

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS

def complete_step(+g: Nat, +xs: List<&2,T.Out>, +t: K.Stack,
    ne: {S.is_nil(xs) == False{} : Bool},
    nd: {S.is_nil(SC.drop(T.Out,xs,SC.pow2(g))) == False{} : Bool},
    ih1: {push_all(E(g,lift(t)),cvs(SC.take(T.Out,xs,SC.pow2(g)))) == E(g,K.push(lift(t),S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))))) : K.Stack},
    ih2: {push_all(E(g,K.SFull{S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),t}),cvs(SC.drop(T.Out,xs,SC.pow2(g)))) == E(g,K.push(K.SFull{S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),t},S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g)))))) : K.Stack}
  ) -> {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(S.tree(1n+g,xs)))) : K.Stack}:
  %Equal.sym(T.Out,S.tree(1n+g,xs),S.join(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))),S.is_nil(SC.drop(T.Out,xs,SC.pow2(g)))),tree_con(g,xs,ne)) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(_))) : K.Stack}
  %Equal.sym(Bool,S.is_nil(SC.drop(T.Out,xs,SC.pow2(g))),False{},nd) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(S.join(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))),_)))) : K.Stack}
  %Equal.sym(T.Out,S.join(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))),False{}),S.parent(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))),join_false(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))),S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,S.cv(_))) : K.Stack}
  %parent_cv_correct(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))) : {push_all(E(1n+g,t),cvs(xs)) == E(1n+g,K.push(t,_)) : K.Stack}
  %Equal.sym(K.Stack,E(1n+g,K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))),E(g,lift(K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g)))))))),E_succ(g,K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g)))))))) : {push_all(E(1n+g,t),cvs(xs)) == _ : K.Stack}
  %Equal.sym(K.Stack,lift(K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))),K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))},lift_push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))) : {push_all(E(1n+g,t),cvs(xs)) == E(g,_) : K.Stack}
  %LS.take_drop(T.Out,xs,SC.pow2(g)) : {push_all(E(1n+g,t),cvs(_)) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
  %Equal.sym(K.Stack,E(1n+g,t),E(g,lift(t)),E_succ(g,t)) : {push_all(_,cvs(SC.append(T.Out,SC.take(T.Out,xs,SC.pow2(g)),SC.drop(T.Out,xs,SC.pow2(g))))) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
  %Equal.sym(K.Stack,push_all(E(g,lift(t)),cvs(SC.append(T.Out,SC.take(T.Out,xs,SC.pow2(g)),SC.drop(T.Out,xs,SC.pow2(g))))),push_all(push_all(E(g,lift(t)),cvs(SC.take(T.Out,xs,SC.pow2(g)))),cvs(SC.drop(T.Out,xs,SC.pow2(g)))),push_split(E(g,lift(t)),SC.take(T.Out,xs,SC.pow2(g)),SC.drop(T.Out,xs,SC.pow2(g)))) : {_ == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
  %Equal.sym(K.Stack,push_all(E(g,lift(t)),cvs(SC.take(T.Out,xs,SC.pow2(g)))),E(g,K.push(lift(t),S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))))),ih1) : {push_all(_,cvs(SC.drop(T.Out,xs,SC.pow2(g)))) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
  %Equal.sym(K.Stack,K.push(lift(t),S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g))))),K.SFull{S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),t},push_lift(t,S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))))) : {push_all(E(g,_),cvs(SC.drop(T.Out,xs,SC.pow2(g)))) == E(g,K.SEmpty{K.push(t,K.parent_cv(S.cv(S.tree(g,SC.take(T.Out,xs,SC.pow2(g)))),S.cv(S.tree(g,SC.drop(T.Out,xs,SC.pow2(g))))))}) : K.Stack}
  ih2

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend&name=take_drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=E
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=E_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=cvs
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=join_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=lift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=lift_push
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=parent_cv_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_all
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_lift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=push_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend&name=tree_con
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=cv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=is_nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=join
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=parent
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=Stack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=parent_cv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend&name=push
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend&name=Out