StraightLine

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

Statistics

Metric	Count
Definitions IsStraightLine, instDecidableIsStraightLine, straightLine_finalRegs, straightLine_finalState	4
Theorems append, cons, singleton, of_nonJump, straightLine_finalRegs_eq_of_halted, straightLine_finalState_spec, straight_line_halts, straight_line_halts_from_regs, straight_line_state_at_pc	9
Total	13

Cslib.URM

Definitions

Name	Category	Theorems
instDecidableIsStraightLine 📖	CompOp	—
straightLine_finalRegs 📖	CompOp	1 math math: straightLine_finalRegs_eq_of_halted
straightLine_finalState 📖	CompOp	1 math math: straightLine_finalState_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
straightLine_finalRegs_eq_of_halted 📖	mathematical	Program.IsStraightLine Steps State.isHalted	State.regs straightLine_finalRegs	—	Steps.eq_of_halts straightLine_finalState_spec
straightLine_finalState_spec 📖	mathematical	Program.IsStraightLine	Steps straightLine_finalState State.isHalted State.pc Instr	—	straight_line_halts_from_regs
straight_line_halts 📖	mathematical	Program.IsStraightLine	Halts	—	straight_line_halts_from_regs
straight_line_halts_from_regs 📖	mathematical	Program.IsStraightLine	Steps State.isHalted State.pc Instr	—	—
straight_line_state_at_pc 📖	mathematical	Program.IsStraightLine Instr	Steps State.pc	—	—

Cslib.URM.Program

Definitions

Name	Category	Theorems
IsStraightLine 📖	MathDef	1 math math: IsStraightLine.singleton

Cslib.URM.Program.IsStraightLine

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append 📖	mathematical	Cslib.URM.Program.IsStraightLine	Cslib.URM.Program Cslib.URM.Instr	—	—
cons 📖	mathematical	Cslib.URM.Instr.IsJump Cslib.URM.Program.IsStraightLine	Cslib.URM.Instr	—	—
singleton 📖	mathematical	Cslib.URM.Instr.IsJump	Cslib.URM.Program.IsStraightLine Cslib.URM.Instr	—	—

Cslib.URM.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_nonJump 📖	mathematical	Cslib.URM.State.pc Cslib.URM.Instr Cslib.URM.Instr.IsJump Cslib.URM.Program	Cslib.URM.Step	—	—

---

← Back to Index