def finish_small

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:197

import Base
import stelliferous@0.0.2.0/traversal_lanes.bend as Lanes
import stelliferous@0.0.2.0/traversal_cells.bend as Cells
import stelliferous@0.0.2.0/kernel_tile.bend as Tile
import stelliferous@0.0.2.0/proofs/nat_division.bend as Division
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

197# The shared induction on eight-value rounds. The proposition may carry all
198# owners and bounds, so binary and ternary instances need only local cases.
199def finish_small(~Owner: Type,~Context: Data,~gather: Owner -> U32 -> Context -> Owner & Tile.Tile8,
200  ~scatter: Owner -> U32 -> Tile.Tile8 -> Owner,~finish: Nat -> Cells.State<Owner,Tile.Tile8,Context> -> Owner,
201  +count: Nat,-state: Cells.State<Owner,Tile.Tile8,Context>,small: {Nat.is_lt(count,8n) == True{} : Bool}) ->
202  {Lanes.rounds_with(~Owner,~Context,~gather,~scatter,~finish,count,state) == finish(count,state) : Owner}:
203  match count:
204    case 0n: {==}
205    case 1n: {==}
206    case 2n: {==}
207    case 3n: {==}
208    case 4n: {==}
209    case 5n: {==}
210    case 6n: {==}
211    case 7n: {==}
212    case 1n+1n+1n+1n+1n+1n+1n+1n+ +rest:
213      Empty.absurd({Lanes.rounds_with(~Owner,~Context,~gather,~scatter,~finish,8n+rest,state) == finish(8n+rest,state) : Owner},
214        WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(rest,0n),True{},Equal.sym(Bool,Nat.is_lt(rest,0n),False{},Division.lt_zero(rest)),small)))