OAI/Computability/SpaceSimulation/Register/Fold.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Fifths.Comp.ticks line 11
2. theorem OAI.Fifths.Comp.plus1 line 35
3. theorem OAI.Fifths.Comp.minus1 line 37
4. def OAI.Fifths.Comp.notZero line 40
5. theorem OAI.Fifths.Comp.notZero_eq line 42
6. theorem OAI.Fifths.Comp.testnz line 50
7. theorem OAI.Fifths.Comp.fold line 77

   Source documentation

   Accumulating loop. PC logic keeps the original argument, a remaining count, a current index, and the accumulator. Time for the counted loop is not charged.

   theorem fold {n : I → ℕ} (v : I → ℕ → ℕ) (cnt : Comp x S a n)
       (ini : Comp x S a (fun i => v i 0))
       (sizes : Fits (fun i : Through n => S i.1.1) (fun i => v i.1.1 i.1.2))
       (advance : ∀ e : Before n → ℕ,
         Comp (fun i : Before n => x i.1.1) (fun i => S i.1.1) e (fun i => a i.1.1) →
         Comp (fun i : Before n => x i.1.1) (fun i => S i.1.1) e (fun i => i.1.2) →
         Comp (fun i : Before n => x i.1.1) (fun i => S i.1.1) e (fun i => v i.1.1 i.1.2) →
         Comp (fun i : Before n => x i.1.1) (fun i => S i.1.1) e
           (fun i => v i.1.1 (i.1.2+1))) :
       Comp x S a (fun i => v i (n i)) := by
   …

   Mentions: OAI.Fifths.Comp, OAI.Fifths.Fits, OAI.Fifths.Through, OAI.Fifths.Before