Documentation Verification Report

BiTape

📁 Source: Cslib/Foundations/Data/BiTape.lean

Statistics

Metric	Count
Definitions `BiTape`, `head`, `instEmptyCollection`, `instInhabited`, `left`, `mk₁`, `move`, `move_left`, `move_right`, `nil`, `optionMove`, `right`, `space_used`, `write`, `BiTape`	15
Theorems `empty_eq_nil`, `move_left_move_right`, `move_right_move_left`, `space_used_mk₁`, `space_used_move`, `space_used_write`	6
Total	21

Turing

Definitions

Name	Category	Theorems
`BiTape` 📖	CompData	1 math math: `BiTape.empty_eq_nil`

Turing.BiTape

Definitions

Name	Category	Theorems
`head` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	1 math math: `empty_eq_nil`
`instInhabited` 📖	CompOp	—
`left` 📖	CompOp	—
`mk₁` 📖	CompOp	1 math math: `space_used_mk₁`
`move` 📖	CompOp	1 math math: `space_used_move`
`move_left` 📖	CompOp	2 math math: `move_right_move_left`, `move_left_move_right`
`move_right` 📖	CompOp	2 math math: `move_right_move_left`, `move_left_move_right`
`nil` 📖	CompOp	1 math math: `empty_eq_nil`
`optionMove` 📖	CompOp	—
`right` 📖	CompOp	—
`space_used` 📖	CompOp	3 math math: `space_used_move`, `space_used_write`, `space_used_mk₁`
`write` 📖	CompOp	1 math math: `space_used_write`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_eq_nil` 📖	mathematical	—	`Turing.BiTape` `instEmptyCollection` `nil`	—	—
`move_left_move_right` 📖	mathematical	—	`move_right` `move_left`	—	`Turing.StackTape.head_cons` `Turing.StackTape.cons_head_tail` `Turing.StackTape.tail_cons`
`move_right_move_left` 📖	mathematical	—	`move_left` `move_right`	—	`Turing.StackTape.head_cons` `Turing.StackTape.tail_cons` `Turing.StackTape.cons_head_tail`
`space_used_mk₁` 📖	mathematical	—	`space_used` `mk₁`	—	`Turing.StackTape.length_nil` `Turing.StackTape.length_map_some`
`space_used_move` 📖	mathematical	—	`space_used` `move`	—	—
`space_used_write` 📖	mathematical	—	`space_used` `write`	—	—

Turing.SingleTapeTM.Cfg

Definitions

Name	Category	Theorems
`BiTape` 📖	CompOp	—

---

← Back to Index