Loop.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Conditional and iteration rules. Iteration does not require a computable iteration bound. Needs a uniform continuation check.

theorem OAI.Fifths.Comp.flag line 17
Source documentation
Get a finite truth flag without erasing the register argument. Pair the computed boolean and the argument; check first bit for zero of first paired natural.
```
theorem flag (h : Comp x S a (fun i => (B i).toNat)) :
    Works (fun i => files (x i)) S (fun i => file (a i)) (fun i => file (a i)) B := by
…
```
Mentions: OAI.Fifths.Comp, OAI.Fifths.Works, OAI.Fifths.file
theorem OAI.Fifths.Comp.casesB line 46
theorem OAI.Fifths.Comp.iteB line 54
abbrev OAI.Fifths.Before line 64
Source documentation
Iterates before and through stop.
```
abbrev Before (n : I → ℕ) := { v : I × ℕ // v.2 < n v.1 }
```
abbrev OAI.Fifths.Through line 65
theorem OAI.Fifths.Works.fixed line 68
theorem OAI.Fifths.Works.eq_targets line 74
theorem OAI.Fifths.Comp.loop line 83