def swap_full.fin

lawful-arrays@0.1.0.0 · proof_shape.bend:136

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

136# The array a swap leaves is perfect: the steps after Array.size.
137def swap_full.fin(-T: Type, -a: Array<T>, -b: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
138  hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array<T>},
139  w: SwapW(T, b, n, U32.and(i, U32.sub(n, 1)), v, U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)), d)) ->
140  {D.full(T, Pair.fst(Array<T>, T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
141    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}:
142  (na, old, e, f) = w
143  %Equal.sym(Array<T> & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
144    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) :
145    {D.full(T, Pair.fst(Array<T>, T, _), d) == True{} : Bool}
146  Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f,
147    Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{},
148      Equal.cong(Array<T>, Bool, x => D.full(T, x, d), b, a, q), hf))