Documentation Verification Report

Flatten

📁 Source: Cslib/Foundations/Data/OmegaSequence/Flatten.lean

Statistics

Metric	Count
Definitions `cumLen`, `flatten`, `toSegs`	3
Theorems `append_flatten`, `cons_flatten`, `cumLen_one_add_drop`, `cumLen_segment_one_add`, `cumLen_segment_zero`, `cumLen_strictMono`, `cumLen_succ`, `cumLen_zero`, `extract_flatten`, `flatten_def`, `flatten_drop`, `flatten_take`, `flatten_take_drop`, `length_flatten_take`, `segment_toSegs_cumLen`, `strictMono_flatten`, `toSegs_def`	17
Total	20

Cslib.ωSequence

Definitions

Name	Category	Theorems
`cumLen` 📖	CompOp	16 math math: `segment_toSegs_cumLen`, `cumLen_zero`, `Cslib.LTS.IsExecution.flatten`, `cumLen_one_add_drop`, `extract_flatten`, `flatten_take_drop`, `flatten_take`, `Cslib.LTS.ωTr.flatten`, `length_flatten_take`, `flatten_drop`, `cumLen_strictMono`, `cumLen_succ`, `flatten_def`, `cumLen_segment_zero`, `Cslib.Automata.NA.loop_run_exists`, `cumLen_segment_one_add`
`flatten` 📖	CompOp	14 math math: `Cslib.LTS.IsExecution.flatten`, `Cslib.ωLanguage.flatten_mem_omegaPow`, `extract_flatten`, `flatten_take_drop`, `flatten_take`, `strictMono_flatten`, `Cslib.LTS.ωTr.flatten`, `Cslib.ωLanguage.mem_omegaPow`, `flatten_drop`, `Cslib.ωLanguage.omegaPow_def`, `flatten_def`, `append_flatten`, `Cslib.Automata.NA.loop_run_exists`, `cons_flatten`
`toSegs` 📖	CompOp	3 math math: `segment_toSegs_cumLen`, `toSegs_def`, `strictMono_flatten`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_flatten` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`appendωSequence` `take` `flatten` `drop`	—	—
`cons_flatten` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`appendωSequence` `head` `flatten` `tail`	—	`ext` `flatten_def` `head.eq_1` `tail_eq_drop` `get_append_left` `cumLen_segment_zero` `get_append_right'` `get_drop` `cumLen_segment_one_add` `cumLen_one_add_drop`
`cumLen_one_add_drop` 📖	mathematical	—	`cumLen` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `drop`	—	—
`cumLen_segment_one_add` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`Nat.segment` `cumLen` `drop`	—	`Nat.segment_plus_one` `cumLen_one_add_drop`
`cumLen_segment_zero` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`Nat.segment` `cumLen`	—	`Nat.segment_range_val` `cumLen_strictMono`
`cumLen_strictMono` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`cumLen`	—	—
`cumLen_succ` 📖	mathematical	—	`cumLen` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	—
`cumLen_zero` 📖	mathematical	—	`cumLen`	—	—
`extract_flatten` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`extract` `flatten` `cumLen`	—	`flatten_drop` `flatten_take`
`flatten_def` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `flatten` `Nat.segment` `cumLen`	—	—
`flatten_drop` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`flatten` `drop` `cumLen`	—	`flatten_take_drop`
`flatten_take` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`take` `cumLen` `flatten`	—	`flatten_take_drop`
`flatten_take_drop` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`take` `cumLen` `flatten` `drop`	—	`append_left_right_injective` `append_flatten` `append_take_drop` `length_flatten_take` `length_take`
`length_flatten_take` 📖	mathematical	—	`take` `cumLen`	—	—
`segment_toSegs_cumLen` 📖	mathematical	—	`cumLen` `toSegs`	—	—
`strictMono_flatten` 📖	mathematical	—	`flatten` `toSegs`	—	`ext` `flatten_def` `segment_toSegs_cumLen` `toSegs_def` `Nat.segment_lower_bound` `Nat.segment_upper_bound`
`toSegs_def` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `toSegs` `extract`	—	—

---

← Back to Index