def set_full.fin

lawful-arrays@0.1.0.0 · proof_shape.bend:170

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

170def set_full.fin(-T: Type, -a: Array<T>, -b: Array<T>, +n: U32, +i: U32, -v: T, +d: Nat,
171  hf: {D.full(T, a, d) == True{} : Bool}, q: {b == a : Array<T>},
172  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)) ->
173  {D.full(T, Array.set.fin(T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
174    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n)))), d) == True{} : Bool}:
175  (na, old, e, f) = w
176  %Equal.sym(Array<T> & T, Array.swap.go(T, b, n, U32.and(i, U32.sub(n, 1)), v,
177    U32.is_lt(U32.and(i, U32.sub(n, 1)), U32.shr(n))), (na, old), e) :
178    {D.full(T, Array.set.fin(T, _), d) == True{} : Bool}
179  Equal.trans(Bool, D.full(T, na, d), D.full(T, b, d), True{}, f,
180    Equal.trans(Bool, D.full(T, b, d), D.full(T, a, d), True{},
181      Equal.cong(Array<T>, Bool, x => D.full(T, x, d), b, a, q), hf))