Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `Instr`, `maxRegister`, `readsFrom`, `shiftJumps`, `shiftRegisters`, `writesTo`, `Program`, `maxRegister`, `shiftJumps`, `shiftRegisters`, `Regs`, `ofInputs`, `output`, `read`, `write`, `zero`, `State`, `init`, `instDecidableIsHalted`, `instInhabited`, `instRepr`, `isHalted`, `pc`, `regs`, `instDecidableEqInstr`, `decEq`, `instReprInstr`, `repr`	28
Theorems	0
Total	28

Cslib.URM

Definitions

Name	Category	Theorems
`Instr` 📖	CompData	8 math math: `Program.IsStraightLine.append`, `Program.getElem?_toStandardForm`, `Program.IsStraightLine.singleton`, `Program.IsStraightLine.cons`, `straight_line_halts_from_regs`, `straightLine_finalState_spec`, `Program.toStandardForm_length`, `State.isHalted_iff`
`Program` 📖	CompOp	4 math math: `Program.IsStraightLine.append`, `Program.getElem?_toStandardForm`, `toStandardForm_equiv`, `ProgramEquiv.equivalence`
`Regs` 📖	CompOp	—
`State` 📖	CompData	4 math math: `Halts.toHaltsWithResult`, `step_confluent`, `halts_iff_normalizable`, `isHalted_iff_normal`
`instDecidableEqInstr` 📖	CompOp	—
`instReprInstr` 📖	CompOp	—

Cslib.URM.Instr

Definitions

Name	Category	Theorems
`maxRegister` 📖	CompOp	1 math math: `Cslib.URM.Program.mem_maxRegister`
`readsFrom` 📖	CompOp	—
`shiftJumps` 📖	CompOp	2 math math: `JumpsBoundedBy.shiftJumps`, `shiftJumps_of_nonJump`
`shiftRegisters` 📖	CompOp	—
`writesTo` 📖	CompOp	—

Cslib.URM.Program

Definitions

Name	Category	Theorems
`maxRegister` 📖	CompOp	1 math math: `mem_maxRegister`
`shiftJumps` 📖	CompOp	—
`shiftRegisters` 📖	CompOp	—

Cslib.URM.Regs

Definitions

Name	Category	Theorems
`ofInputs` 📖	CompOp	—
`output` 📖	CompOp	1 math math: `Cslib.URM.Halts.toHaltsWithResult`
`read` 📖	CompOp	4 math math: `Cslib.URM.Steps.preserves_register`, `Cslib.URM.Step.preserves_register`, `write_read_of_ne`, `write_read_self`
`write` 📖	CompOp	2 math math: `write_read_of_ne`, `write_read_self`
`zero` 📖	CompOp	—

Cslib.URM.State

Definitions

Name	Category	Theorems
`init` 📖	CompOp	2 math math: `Cslib.URM.evalState_spec`, `Cslib.URM.halts_iff_normalizable`
`instDecidableIsHalted` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instRepr` 📖	CompOp	—
`isHalted` 📖	MathDef	7 math math: `Cslib.URM.Step.toStandardForm`, `Cslib.URM.evalState_spec`, `Cslib.URM.straight_line_halts_from_regs`, `Cslib.URM.isHalted_iff_normal`, `Cslib.URM.straightLine_finalState_spec`, `Cslib.URM.Step.from_toStandardForm`, `isHalted_iff`
`pc` 📖	CompOp	5 math math: `ext_iff`, `Cslib.URM.straight_line_halts_from_regs`, `Cslib.URM.straight_line_state_at_pc`, `Cslib.URM.straightLine_finalState_spec`, `isHalted_iff`
`regs` 📖	CompOp	10 math math: `Cslib.URM.Step.toStandardForm`, `ext_iff`, `Cslib.URM.Steps.preserves_register`, `Cslib.URM.Step.preserves_register`, `Cslib.URM.Halts.toHaltsWithResult`, `Cslib.URM.Steps.toStandardForm_halts`, `Cslib.URM.Steps.from_toStandardForm_halts`, `Cslib.URM.straightLine_finalRegs_eq_of_halted`, `Cslib.URM.Step.from_toStandardForm`, `Cslib.URM.evalState_toStandardForm_regs`

Cslib.URM.instDecidableEqInstr

Definitions

Name	Category	Theorems
`decEq` 📖	CompOp	—

Cslib.URM.instReprInstr

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index