OAI/Computability/WLIdentification/ExpressionBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.WordExpressions.Expr.outputCode line 10
2. theorem OAI.WLIdentification.WordExpressions.Expr.outputCode_exec line 13
3. theorem OAI.WLIdentification.WordExpressions.Expr.computes line 55

   Source documentation

   A complete local, finite-alphabet output producer from a proved bounded word expression. Uniformity is in the expression, not in its inputs.

   theorem computes (e : Expr 1) (B : ℕ → ℕ)
       (hw : ∀ n, n ≤ B n) (h : ∀ w, e.Bounded (fun _ => w) (B w.length)) :
       ∃ M : Machine, ComputesWithin M (fun w => e.eval (fun _ => w))
         (fun n => e.outputBound (B n)) := by
   …

   Mentions: OAI.WLIdentification.WordExpressions.Expr, OAI.WLIdentification.Machine, OAI.WLIdentification.ComputesWithin

4. theorem OAI.WLIdentification.ComputationBounds.compose line 88
5. theorem OAI.WLIdentification.ComputationBounds.dominates line 101
6. def OAI.WLIdentification.WordExpressions.Expr.liftRen line 109
7. def OAI.WLIdentification.WordExpressions.Expr.rename line 112
8. theorem OAI.WLIdentification.WordExpressions.Expr.snoc_liftRen line 121
9. theorem OAI.WLIdentification.WordExpressions.Expr.stages_rename line 126
10. theorem OAI.WLIdentification.WordExpressions.Expr.eval_rename line 134
11. theorem OAI.WLIdentification.WordExpressions.Expr.bounded_rename line 149
12. theorem OAI.WLIdentification.WordExpressions.Expr.bounded_mono line 165
13. def OAI.WLIdentification.WordExpressions.Expr.liftSub line 182
14. def OAI.WLIdentification.WordExpressions.Expr.subst line 185
15. theorem OAI.WLIdentification.WordExpressions.Expr.eval_liftSub line 194
16. theorem OAI.WLIdentification.WordExpressions.Expr.stages_subst line 199
17. theorem OAI.WLIdentification.WordExpressions.Expr.eval_subst line 208
18. theorem OAI.WLIdentification.WordExpressions.Expr.bounded_liftSub line 223
19. theorem OAI.WLIdentification.WordExpressions.Expr.bounded_subst line 231