Documentation Verification Report

StandardForm

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

Statistics

Metric	Count
Definitions `IsStandardForm`, `instDecidableIsStandardForm`, `toStandardForm`	3
Theorems `of_toStandardForm`, `toStandardForm`, `toStandardForm_iff`, `getElem?_toStandardForm`, `toStandardForm_idempotent`, `toStandardForm_isStandardForm`, `toStandardForm_length`, `from_toStandardForm`, `toStandardForm`, `from_toStandardForm_halts`, `toStandardForm_halts`, `evalState_toStandardForm_regs`, `eval_toStandardForm`, `straight_line_IsStandardForm`, `toStandardForm_equiv`	15
Total	18

Cslib.URM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalState_toStandardForm_regs` 📖	mathematical	`State` `evalState` `Program.toStandardForm`	`State.regs`	—	`evalState_spec` `Steps.toStandardForm_halts` `Steps.eq_of_halts`
`eval_toStandardForm` 📖	mathematical	—	`eval` `Program.toStandardForm`	—	`Halts.toStandardForm_iff` `evalState_toStandardForm_regs`
`straight_line_IsStandardForm` 📖	mathematical	`Program.IsStraightLine`	`Program.IsStandardForm`	—	`Instr.jumpsBoundedBy_of_nonJump`
`toStandardForm_equiv` 📖	mathematical	—	`Program` `instSetoidProgram` `Program.toStandardForm`	—	`eval_toStandardForm`

Cslib.URM.Halts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_toStandardForm` 📖	—	`Cslib.URM.Halts` `Cslib.URM.Program.toStandardForm`	—	—	`Cslib.URM.Steps.from_toStandardForm_halts`
`toStandardForm` 📖	mathematical	`Cslib.URM.Halts`	`Cslib.URM.Program.toStandardForm`	—	`Cslib.URM.Steps.toStandardForm_halts`
`toStandardForm_iff` 📖	mathematical	—	`Cslib.URM.Halts` `Cslib.URM.Program.toStandardForm`	—	`toStandardForm` `of_toStandardForm`

Cslib.URM.Program

Definitions

Name	Category	Theorems
`IsStandardForm` 📖	MathDef	2 math math: `Cslib.URM.straight_line_IsStandardForm`, `toStandardForm_isStandardForm`
`instDecidableIsStandardForm` 📖	CompOp	—
`toStandardForm` 📖	CompOp	10 math math: `Cslib.URM.Step.toStandardForm`, `getElem?_toStandardForm`, `Cslib.URM.Halts.toStandardForm_iff`, `Cslib.URM.Halts.toStandardForm`, `Cslib.URM.eval_toStandardForm`, `Cslib.URM.Steps.toStandardForm_halts`, `Cslib.URM.toStandardForm_equiv`, `toStandardForm_length`, `toStandardForm_isStandardForm`, `toStandardForm_idempotent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getElem?_toStandardForm` 📖	mathematical	—	`Cslib.URM.Program` `Cslib.URM.Instr` `toStandardForm` `Cslib.URM.Instr.capJump`	—	—
`toStandardForm_idempotent` 📖	mathematical	—	`toStandardForm`	—	`Cslib.URM.Instr.capJump_idempotent`
`toStandardForm_isStandardForm` 📖	mathematical	—	`IsStandardForm` `toStandardForm`	—	`Cslib.URM.Instr.JumpsBoundedBy.capJump`
`toStandardForm_length` 📖	mathematical	—	`Cslib.URM.Instr` `toStandardForm`	—	—

Cslib.URM.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`from_toStandardForm` 📖	mathematical	`Cslib.URM.Step` `Cslib.URM.Program.toStandardForm`	`Cslib.URM.State.isHalted` `Cslib.URM.State.regs`	—	`Cslib.URM.Program.getElem?_toStandardForm`
`toStandardForm` 📖	mathematical	`Cslib.URM.Step`	`Cslib.URM.Program.toStandardForm` `Cslib.URM.State.isHalted` `Cslib.URM.State.regs`	—	`Cslib.URM.Program.getElem?_toStandardForm`

Cslib.URM.Steps

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`from_toStandardForm_halts` 📖	mathematical	`Cslib.URM.Steps` `Cslib.URM.Program.toStandardForm` `Cslib.URM.State.isHalted`	`Cslib.URM.State.regs`	—	`Cslib.URM.Program.toStandardForm_length` `Cslib.URM.Step.from_toStandardForm` `eq_of_halts`
`toStandardForm_halts` 📖	mathematical	`Cslib.URM.Steps` `Cslib.URM.State.isHalted`	`Cslib.URM.Program.toStandardForm` `Cslib.URM.State.regs`	—	`Cslib.URM.Program.toStandardForm_length` `Cslib.URM.Step.toStandardForm`

---

← Back to Index