law ej_step

lawful-fields@0.1.1.0 · proof_list.bend:362

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

362# One step of ej, with the induction hypothesis for the rest (t is not empty).
363law ej_step:
364  for +p: List<&2, U32>
365  for +t: List<&2, List<&2, U32>>
366  for +sep: U32
367  for +from: Nat
368  for +k2: Nat
369  for +h: {Nat.is_lt(1n+k2, List.length(&2, List<&2, U32>, p <> t)) == True{} : Bool}
370  for +ih: {List.get(&2, Nat, F.ends(t, Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n)), k2) == Some{Nat.add(Nat.add(Nat.add(from, List.length(&2, U32, p)), 1n), List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, t, 1n+k2), sep)))} : Maybe<&2, Nat>}
371  {List.get(&2, Nat, F.ends(p <> t, from), 1n+k2) == Some{Nat.add(from, List.length(&2, U32, F.join(List.take(&2, List<&2, U32>, p <> t, 1n+1n+k2), sep)))} : Maybe<&2, Nat>}