Defs

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

Statistics

Metric	Count
Definitions instCoeForallNatωSequence, instFunLikeωSequenceNat, ωSequence, appendωSequence, cons, const, drop, extract, get, head, iterate, map, tail, take, zip, «term_++ω_», «term_::ω_»	17
Theorems	0
Total	17

Cslib

Definitions

Name	Category	Theorems
instCoeForallNatωSequence 📖	CompOp	—
instFunLikeωSequenceNat 📖	CompOp	45 math math: ωSequence.getElem?_take, ωSequence.get_drop, ωSequence.extract_succ_right, ωSequence.get_append_right', ωSequence.get_succ_cons, ωSequence.getElem?_take_succ, ωSequence.extract_eq_ofFn, ωSequence.get_map, Automata.NA.totalize_mtr_run, ωSequence.cumLen_one_add_drop, ωSequence.get_succ_iterate, ωSequence.toSegs_def, ωSequence.get_cons_append_zero, ωSequence.get_append_right, ωSequence.extract_eq_extract, ωSequence.ext_iff, ωSequence.get_append_left, ωSequence.get_tail, LTS.ωTr_mTr, LTS.Total.mTr_ωTr, ωSequence.get_extract, ωLanguage.mem_omegaPow, ωSequence.frequently_in_finite_type, Automata.DA.run_succ, ωSequence.get_succ, ωSequence.take_succ', ωSequence.get_const, ωSequence.take_get, ωSequence.take_one, ωSequence.get_append_length, ωSequence.get_succ_iterate', ωSequence.cumLen_succ, Automata.DA.run_zero, ωSequence.get_fun, LTS.Total.ωTr_exists, Automata.DA.mtr_extract_eq_run, ωSequence.flatten_def, Automata.NA.Run.start, ωSequence.get_iterate, ωSequence.drop_frequently_iff_frequently, ωSequence.get_zero_iterate, ωSequence.get_zip, ωSequence.head_drop, ωSequence.concat_take_get, ωSequence.get_zero_cons
ωSequence 📖	CompData	74 math math: ωLanguage.iSup_def, ωLanguage.iInf_def, ωSequence.getElem?_take, ωLanguage.omegaPow_seq_prop, ωSequence.get_drop, ωSequence.extract_succ_right, ωSequence.get_append_right', ωSequence.get_succ_cons, ωSequence.getElem?_take_succ, ωSequence.extract_eq_ofFn, ωLanguage.sup_def, ωSequence.get_map, ωLanguage.compl_def, Automata.NA.Buchi.inter_language_eq, Automata.NA.totalize_mtr_run, ωSequence.cumLen_one_add_drop, ωSequence.get_succ_iterate, ωLanguage.mem_top, ωLanguage.ext_iff, ωSequence.toSegs_def, ωLanguage.mem_compl, ωLanguage.map_def, ωSequence.get_cons_append_zero, ωSequence.get_append_right, ωSequence.extract_eq_extract, ωSequence.ext_iff, ωSequence.get_append_left, ωSequence.get_tail, LTS.ωTr_mTr, LTS.Total.mTr_ωTr, ωSequence.get_extract, ωLanguage.hmul_seq_prop, ωLanguage.mem_omegaPow, ωSequence.frequently_in_finite_type, Automata.DA.run_succ, ωSequence.get_succ, ωSequence.cons_injective_left, ωSequence.cons_injective2, ωLanguage.omegaPow_def, Automata.ωAcceptor.mem_language, ωLanguage.hmul_def, Automata.NA.Buchi.iSum_language_eq, ωLanguage.mem_inf, ωSequence.take_succ', ωSequence.get_const, ωSequence.take_get, ωSequence.take_one, ωLanguage.mem_iSup, ωLanguage.mem_iInf, ωSequence.get_append_length, ωSequence.get_succ_iterate', ωLanguage.bot_def, ωSequence.cumLen_succ, ωLanguage.mem_omegaLim, Automata.DA.run_zero, ωSequence.get_fun, LTS.Total.ωTr_exists, Automata.DA.mtr_extract_eq_run, ωSequence.flatten_def, ωLanguage.mem_hmul, ωLanguage.notMem_bot, Automata.NA.Run.start, ωSequence.get_iterate, ωLanguage.mem_sup, ωSequence.drop_frequently_iff_frequently, ωSequence.get_zero_iterate, ωLanguage.top_def, ωLanguage.inf_def, ωSequence.get_zip, ωSequence.cons_injective_right, ωLanguage.omegaLim_def, ωSequence.head_drop, ωSequence.concat_take_get, ωSequence.get_zero_cons

Cslib.ωSequence

Definitions

Name	Category	Theorems
appendωSequence 📖	CompOp	30 math math: append_eq_cons, extract_append_zero_right, get_append_right', append_take_drop, Cslib.ωLanguage.append_mem_hmul, Cslib.Automata.NA.totalize_mtr_run, nil_append_ωSequence, get_cons_append_zero, get_append_right, get_append_left, drop_append_ωSequence, drop_append_of_ge_length, Cslib.LTS.Total.mTr_ωTr, drop_append_of_le_length, Cslib.LTS.ωTr.append, append_ωSequence_head_tail, Cslib.ωLanguage.hmul_def, append_extract_drop, extract_apppend_right_right, get_append_length, take_append_of_le_length, Cslib.Automata.NA.concat_run_exists, Cslib.ωLanguage.mem_hmul, append_flatten, append_right_inj, cons_append_ωSequence, append_append_ωSequence, append_take, map_append_ωSequence, cons_flatten
cons 📖	CompOp	18 math math: map_cons, append_eq_cons, get_succ_cons, tail_cons, map_eq, cons_head_tail, cons_injective_left, cons_injective2, const_eq, head_cons, zip_eq, eta, take_succ_cons, Cslib.LTS.ωTr.cons, cons_append_ωSequence, iterate_eq, cons_injective_right, get_zero_cons
const 📖	CompOp	6 math math: map_const, tail_const, drop_const, const_eq, iterate_id, get_const
drop 📖	CompOp	35 math math: drop_zip, get_drop, append_take_drop, take_drop, Cslib.Automata.NA.loop_run_one_iter, take_add, cumLen_one_add_drop, drop_drop, drop_succ, drop_const, tail_drop, tail_drop', drop_map, flatten_take_drop, drop_append_ωSequence, drop_append_of_ge_length, tail_eq_drop, Cslib.ωLanguage.hmul_seq_prop, extract_drop, flatten_drop, drop_append_of_le_length, Cslib.LTS.ωTr.append, drop_zero, append_extract_drop, Cslib.Automata.NA.concat_run_right, extract_eq_drop_take, Cslib.Automata.NA.concat_run_exists, Cslib.Automata.NA.loop_run_from_left, append_flatten, drop_frequently_iff_frequently, cumLen_segment_one_add, head_drop, Cslib.LTS.divergentTrace_drop, drop_tail', Cslib.Automata.NA.concat_run_proj
extract 📖	CompOp	23 math math: extract_append_zero_right, extract_succ_right, extract_0u_extract_l, extract_eq_nil_iff, extract_eq_ofFn, Cslib.LTS.IsExecution.flatten, length_extract, toSegs_def, extract_flatten, extract_eq_nil, Cslib.LTS.ωTr_mTr, extract_lu_extract_lu, get_extract, extract_drop, append_extract_extract, extract_0u_extract_lu, append_extract_drop, extract_apppend_right_right, Cslib.ωLanguage.mem_omegaLim, extract_eq_drop_take, Cslib.Automata.DA.mtr_extract_eq_run, Cslib.ωLanguage.omegaLim_def, extract_eq_take
get 📖	CompOp	—
head 📖	CompOp	12 math math: head_map, map_eq, cons_head_tail, append_ωSequence_head_tail, head_cons, zip_eq, eta, head_iterate, take_succ, head_zip, head_drop, cons_flatten
iterate 📖	CompOp	9 math math: tail_iterate, get_succ_iterate, iterate_id, map_iterate, get_succ_iterate', get_iterate, get_zero_iterate, head_iterate, iterate_eq
map 📖	CompOp	23 math math: Cslib.Automata.NA.Buchi.reindex_run_iff', tail_map, map_cons, map_map, map_id, head_map, get_map, map_take, map_eq, Cslib.ωLanguage.map_def, map_const, drop_map, Cslib.Automata.NA.iProd_run_iff, Cslib.Automata.NA.iSum_run_iff, map_tail, Cslib.Automata.NA.hist_run_exists, Cslib.Automata.NA.hist_run_proj, Cslib.Automata.NA.concat_run_right, map_iterate, Cslib.Automata.NA.concat_run_exists, Cslib.Automata.NA.Buchi.reindex_run_iff, map_append_ωSequence, Cslib.Automata.NA.concat_run_proj
tail 📖	CompOp	20 math math: tail_map, tail_zip, tail_iterate, tail_cons, map_eq, drop_succ, tail_const, tail_drop, get_tail, tail_drop', tail_eq_drop, cons_head_tail, map_tail, get_succ, append_ωSequence_head_tail, zip_eq, eta, take_succ, drop_tail', cons_flatten
take 📖	CompOp	33 math math: getElem?_take, Cslib.Automata.NA.loop_run_left_right, take_zero, getElem?_take_succ, take_prefix_take_left, map_take, append_take_drop, take_drop, Cslib.Automata.NA.loop_run_one_iter, Cslib.Automata.NA.concat_run_left, take_add, Cslib.Automata.NA.concat_run_left_right, length_take, flatten_take_drop, flatten_take, length_flatten_take, Cslib.ωLanguage.hmul_seq_prop, take_take, take_succ', take_prefix, dropLast_take, Cslib.Automata.NA.totalize_run_mtr, take_one, take_append_of_le_length, extract_eq_drop_take, take_succ_cons, append_flatten, take_succ, Cslib.Automata.NA.loop_run_left_right_left, append_take, extract_eq_take, concat_take_get, Cslib.Automata.NA.concat_run_proj
zip 📖	CompOp	5 math math: drop_zip, tail_zip, zip_eq, get_zip, head_zip
«term_++ω_» 📖	CompOp	—
«term_::ω_» 📖	CompOp	—

---

← Back to Index