Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsJump`, `JumpsBoundedBy`, `capJump`, `instDecidableIsJump`, `instDecidableJumpsBoundedBy`	5
Theorems `J_IsJump`, `capJump`, `mono`, `shiftJumps`, `S_nonJump`, `T_nonJump`, `Z_nonJump`, `capJump_J`, `capJump_S`, `capJump_T`, `capJump_Z`, `capJump_idempotent`, `jumpsBoundedBy_of_nonJump`, `shiftJumps_of_nonJump`, `mem_maxRegister`, `write_read_of_ne`, `write_read_self`, `ext`, `ext_iff`, `isHalted_iff`	20
Total	25

Cslib.URM.Instr

Definitions

Name	Category	Theorems
`IsJump` 📖	MathDef	4 math math: `Z_nonJump`, `J_IsJump`, `S_nonJump`, `T_nonJump`
`JumpsBoundedBy` 📖	MathDef	2 math math: `jumpsBoundedBy_of_nonJump`, `JumpsBoundedBy.capJump`
`capJump` 📖	CompOp	7 math math: `Cslib.URM.Program.getElem?_toStandardForm`, `capJump_J`, `capJump_Z`, `capJump_S`, `capJump_idempotent`, `JumpsBoundedBy.capJump`, `capJump_T`
`instDecidableIsJump` 📖	CompOp	—
`instDecidableJumpsBoundedBy` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`J_IsJump` 📖	mathematical	—	`IsJump` `J`	—	—
`S_nonJump` 📖	mathematical	—	`IsJump` `S`	—	—
`T_nonJump` 📖	mathematical	—	`IsJump` `T`	—	—
`Z_nonJump` 📖	mathematical	—	`IsJump` `Z`	—	—
`capJump_J` 📖	mathematical	—	`capJump` `J`	—	—
`capJump_S` 📖	mathematical	—	`capJump` `S`	—	—
`capJump_T` 📖	mathematical	—	`capJump` `T`	—	—
`capJump_Z` 📖	mathematical	—	`capJump` `Z`	—	—
`capJump_idempotent` 📖	mathematical	—	`capJump`	—	—
`jumpsBoundedBy_of_nonJump` 📖	mathematical	`IsJump`	`JumpsBoundedBy`	—	—
`shiftJumps_of_nonJump` 📖	mathematical	`IsJump`	`shiftJumps`	—	—

Cslib.URM.Instr.JumpsBoundedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`capJump` 📖	mathematical	—	`Cslib.URM.Instr.JumpsBoundedBy` `Cslib.URM.Instr.capJump`	—	—
`mono` 📖	—	`Cslib.URM.Instr.JumpsBoundedBy`	—	—	—
`shiftJumps` 📖	mathematical	`Cslib.URM.Instr.JumpsBoundedBy`	`Cslib.URM.Instr.shiftJumps`	—	—

Cslib.URM.Program

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_maxRegister` 📖	mathematical	`Cslib.URM.Instr` `Cslib.URM.Program`	`Cslib.URM.Instr.maxRegister` `maxRegister`	—	—

Cslib.URM.Regs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`write_read_of_ne` 📖	mathematical	—	`read` `write`	—	—
`write_read_self` 📖	mathematical	—	`read` `write`	—	—

Cslib.URM.State

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`pc` `regs`	—	—	—
`ext_iff` 📖	mathematical	—	`pc` `regs`	—	`ext`
`isHalted_iff` 📖	mathematical	—	`isHalted` `Cslib.URM.Instr` `pc`	—	—

---

← Back to Index