def AP.tree_ext

bend-osdev-array@0.1.0.1 · PROOF.bend:1448

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1448# a perfect tree is the tree of its own leaves
1449def AP.tree_ext(-T: Data, +d: Nat, +t: AP.Tree<T>, +f: T, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}) -> {AP.build(T, t) == AP.build(T, AP.tof(T, d, A.Arrays.leaves(T, AP.build(T, t)), f)) : Array<T>}:
1450  match d t:
1451    case 0n APLeaf{x}:
1452      {==}
1453    case 0n APNode{xs, ys}:
1454      Empty.absurd({AP.build(T, APNode{xs, ys}) == AP.build(T, AP.tof(T, 0n, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), f)) : Array<T>}, AP.ft(hp))
1455    case 1n+p APLeaf{x}:
1456      Empty.absurd({AP.build(T, APLeaf{x}) == AP.build(T, AP.tof(T, 1n+p, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), f)) : Array<T>}, AP.ft(hp))
1457    case 1n+ +p APNode{xs, ys}:
1458      +s = A.Arrays.slots(p)
1459      +lx = A.Arrays.leaves(T, AP.build(T, xs))
1460      +ly = A.Arrays.leaves(T, AP.build(T, ys))
1461      +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1462      +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp)
1463      +hl = AP.len_perf(T, p, xs, hpx)
1464      %hl : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, List.take(&2, T, List.append(&2, T, lx, ly), _), f)), AP.build(T, AP.tof(T, p, List.drop(&2, T, List.append(&2, T, lx, ly), _), f))} : Array<T>}
1465      %Equal.sym(List<&2, T>, List.take(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), lx, AP.take_app(T, lx, ly)) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, _, f)), AP.build(T, AP.tof(T, p, List.drop(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), f))} : Array<T>}
1466      %Equal.sym(List<&2, T>, List.drop(&2, T, List.append(&2, T, lx, ly), List.length(&2, T, lx)), ly, AP.drop_app(T, lx, ly)) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, AP.tof(T, p, lx, f)), AP.build(T, AP.tof(T, p, _, f))} : Array<T>}
1467      %AP.tree_ext(T, p, xs, f, hpx) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{_, AP.build(T, AP.tof(T, p, ly, f))} : Array<T>}
1468      %AP.tree_ext(T, p, ys, f, hpy) : {ANode{AP.build(T, xs), AP.build(T, ys)} == ANode{AP.build(T, xs), _} : Array<T>}
1469      {==}