Documentation Verification Report

Execution

📁 Source: Cslib/Computability/URM/Execution.lean

Statistics

Metric	Count
Definitions `Diverges`, `Halts`, `HaltsWithResult`, `ProgramEquiv`, `Step`, `Steps`, `eval`, `evalState`, `instSetoidProgram`, `«term_↑_»`, `«term_↓_»`, `«term_↓_≫_»`	12
Theorems `toHaltsWithResult`, `toHalts`, `equivalence`, `deterministic`, `no_step_of_halted`, `preserves_register`, `eq_of_halts`, `preserves_register`, `evalState_spec`, `haltsWithResult_iff_eval`, `halts_iff_normalizable`, `isHalted_iff_normal`, `step_confluent`	13
Total	25

Cslib.URM

Definitions

Name	Category	Theorems
`Diverges` 📖	MathDef	—
`Halts` 📖	MathDef	4 math math: `straight_line_halts`, `Halts.toStandardForm_iff`, `HaltsWithResult.toHalts`, `halts_iff_normalizable`
`HaltsWithResult` 📖	MathDef	2 math math: `Halts.toHaltsWithResult`, `haltsWithResult_iff_eval`
`ProgramEquiv` 📖	MathDef	1 math math: `ProgramEquiv.equivalence`
`Step` 📖	CompData	5 math math: `step_confluent`, `halts_iff_normalizable`, `Step.no_step_of_halted`, `isHalted_iff_normal`, `Step.of_nonJump`
`Steps` 📖	MathDef	4 math math: `evalState_spec`, `straight_line_halts_from_regs`, `straight_line_state_at_pc`, `straightLine_finalState_spec`
`eval` 📖	CompOp	2 math math: `haltsWithResult_iff_eval`, `eval_toStandardForm`
`evalState` 📖	CompOp	1 math math: `Halts.toHaltsWithResult`
`instSetoidProgram` 📖	CompOp	1 math math: `toStandardForm_equiv`
`«term_↑_»` 📖	CompOp	—
`«term_↓_»` 📖	CompOp	—
`«term_↓_≫_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalState_spec` 📖	mathematical	`State` `evalState`	`Steps` `State.init` `State.isHalted`	—	—
`haltsWithResult_iff_eval` 📖	mathematical	—	`HaltsWithResult` `eval`	—	`eval.eq_1` `Steps.eq_of_halts` `evalState_spec`
`halts_iff_normalizable` 📖	mathematical	—	`Halts` `Relation.Normalizable` `State` `Step` `State.init`	—	—
`isHalted_iff_normal` 📖	mathematical	—	`State.isHalted` `Relation.Normal` `State` `Step`	—	`Step.no_step_of_halted`
`step_confluent` 📖	mathematical	—	`Relation.Confluent` `State` `Step`	—	`Step.deterministic`

Cslib.URM.Halts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toHaltsWithResult` 📖	mathematical	`Cslib.URM.Halts`	`Cslib.URM.HaltsWithResult` `Cslib.URM.Regs.output` `Cslib.URM.State.regs` `Cslib.URM.State` `Cslib.URM.evalState`	—	`Cslib.URM.evalState_spec`

Cslib.URM.HaltsWithResult

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toHalts` 📖	mathematical	`Cslib.URM.HaltsWithResult`	`Cslib.URM.Halts`	—	—

Cslib.URM.ProgramEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalence` 📖	mathematical	—	`Cslib.URM.Program` `Cslib.URM.ProgramEquiv`	—	—

Cslib.URM.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deterministic` 📖	—	`Cslib.URM.Step`	—	—	—
`no_step_of_halted` 📖	mathematical	`Cslib.URM.State.isHalted`	`Cslib.URM.Step`	—	—
`preserves_register` 📖	mathematical	`Cslib.URM.Step`	`Cslib.URM.Regs.read` `Cslib.URM.State.regs`	—	—

Cslib.URM.Steps

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_halts` 📖	—	`Cslib.URM.Steps` `Cslib.URM.State.isHalted`	—	—	`Cslib.URM.step_confluent` `Cslib.URM.isHalted_iff_normal`
`preserves_register` 📖	mathematical	`Cslib.URM.Steps`	`Cslib.URM.Regs.read` `Cslib.URM.State.regs`	—	—

---

← Back to Index