~/jendhub

def advanced

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:176

import stelliferous@0.0.2.0/proofs/traversal_lanes_refinement.bend as TraversalLanesRefinement
import Base
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

176def advanced(+steps: Nat,+start: Nat) -> {stepped(steps,start) == U32.from_nat(Nat.add(steps,start)) : U32}:
177  match steps:
178    case 0n: {==}
179    case 1n+ +rest:
180      %Equal.sym(U32,stepped(rest,start),U32.from_nat(Nat.add(rest,start)),advanced(rest,start)) : {(_ + 1 : U32) == U32.from_nat(1n+Nat.add(rest,start)) : U32}
181      Bounds.add_one(U32.from_nat(Nat.add(rest,start)))

Uses (8)

Used by (1)