def AP.perf_swap

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

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

679def AP.perf_swap(-T: Data, t: AP.Tree<T>, n: U32, +i: U32, v: T, z: Bool, +d: Nat) -> {A.Arrays.is_perfect(T, d, AP.build(T, AP.swap_t(T, t, n, i, v, z))) == A.Arrays.is_perfect(T, d, AP.build(T, t)) : Bool}:
680  match t z:
681    case APLeaf{x} _:
682      match d:
683        case 0n:
684          {==}
685        case 1n+p:
686          {==}
687    case APNode{xs, ys} True{}:
688      match d:
689        case 0n:
690          {==}
691        case 1n+p:
692          +h = U32.shr(n)
693          +z1 = U32.is_lt(i, U32.shr(h))
694          %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.swap_t(T, xs, h, i, v, z1))), A.Arrays.is_perfect(T, p, AP.build(T, xs)), AP.perf_swap(T, xs, h, i, v, z1, p)) : {Bool.and(_, A.Arrays.is_perfect(T, p, AP.build(T, ys))) == Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys))) : Bool}
695          {==}
696    case APNode{xs, ys} False{}:
697      match d:
698        case 0n:
699          {==}
700        case 1n+p:
701          +h = U32.shr(n)
702          +j = U32.sub(i, h)
703          +z1 = U32.is_lt(j, U32.shr(h))
704          %Equal.sym(Bool, A.Arrays.is_perfect(T, p, AP.build(T, AP.swap_t(T, ys, h, j, v, z1))), A.Arrays.is_perfect(T, p, AP.build(T, ys)), AP.perf_swap(T, ys, h, j, v, z1, p)) : {Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), _) == Bool.and(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys))) : Bool}
705          {==}