law pb_push

lawful-fields@0.1.1.0 · proof_cut.bend:495

import Base
import lawful-fields@0.1.1.0/defs.bend as F

495law pb_push:
496  for +x: U32
497  for +ps: List<&2, List<&2, U32>>
498  for +xs: List<&2, U32>
499  for +s: Nat
500  for +hnn: {nn(ps) == True{} : Bool}
501  for +hg: {List.get(&2, U32, xs, s) == Some{x} : Maybe<&2, U32>}
502  for +ih: {PN(F.ends(ps, Nat.add(s, 1n)), xs, Nat.add(s, 1n)) == ps : List<&2, List<&2, U32>>}
503  {PN(F.ends(F.split.push(x, ps), s), xs, s) == F.split.push(x, ps) : List<&2, List<&2, U32>>}