| Name | Category | Theorems |
|---|
All 📖 | MathDef | 1 mathmath: all_def
|
Any 📖 | MathDef | 1 mathmath: any_def
|
appendStream' 📖 | CompOp | 21 mathmath: append_right_inj, cons_append_stream, Seq.ofStream_append, append_take_drop, map_append_stream, drop_append_of_le_length, get_append_length, nil_append_stream, get_cons_append_zero, mem_append_stream_right, mem_append_stream_left, append_append_stream, cycle_eq, append_take, take_append_of_le_length, drop_append_stream, get_append_left, append_stream_head_tail, append_eq_cons, get_append_right, zip_inits_tails
|
apply 📖 | CompOp | 5 mathmath: composition, homomorphism, map_eq_apply, identity, interchange
|
cons 📖 | CompOp | 30 mathmath: corec'_eq, cons_append_stream, get_succ_cons, mem_cons, tails_eq, even_cons_cons, inits_core_eq, Seq.ofStream_cons, nats_eq, map_cons, const_eq, corec_eq, cons_injective_right, mem_cons_of_mem, cons_injective_left, head_cons, interleave_eq, inits_eq, cons_injective2, zip_eq, get_zero_cons, eta, take_succ_cons, iterate_eq, unfolds_eq, cons_head_tail, append_eq_cons, map_eq, Seq.val_cons, tail_cons
|
const 📖 | CompOp | 10 mathmath: iterate_id, const_eq, corec_id_id_eq_const, map_const, drop_const, cycle_singleton, mem_const, tail_const, zip_inits_tails, get_const
|
corec 📖 | CompOp | — |
corec' 📖 | CompOp | 1 mathmath: corec'_eq
|
corecOn 📖 | CompOp | — |
corecState 📖 | CompOp | — |
cycle 📖 | CompOp | 3 mathmath: cycle_eq, mem_cycle, cycle_singleton
|
cycleF 📖 | CompOp | — |
cycleG 📖 | CompOp | 1 mathmath: cycle_g_cons
|
drop 📖 | CompOp | 21 mathmath: take_drop, tail_eq_drop, get_tails, drop_succ, append_take_drop, drop_append_of_le_length, drop_tail', head_drop, drop_drop, tail_drop, drop_zip, drop_const, take_add, tail_drop', drop_append_stream, drop_zero, get_of_bisim, Hindman.FS_iter_tail_sub_FS, drop_map, Hindman.FP_drop_subset_FP, get_drop
|
enum 📖 | CompOp | 2 mathmath: get_enum, enum_eq_zip
|
even 📖 | CompOp | 8 mathmath: even_tail, even_cons_cons, odd_eq, even_interleave, head_even, interleave_even_odd, tail_even, get_even
|
get 📖 | CompOp | 45 mathmath: get_unfolds_head_tail, concat_take_get, get_succ, get_nats, ofDigits_cantorToTernary, get_succ_cons, Hindman.FS.finset_sum, get_tails, get_interleave_left, get_interleave_right, Hindman.FP.finset_prod, take_get, get_tail, get_map, take_succ', get_append_length, Hindman.FS.singleton, head_drop, get_cons_append_zero, cantorSequence_mem_cantorSet, get_inits, get_zero_iterate, Hindman.FP.singleton, get_zero_cons, any_def, get_even, get_succ_iterate, getElem?_take, get_enum, mem_iff_exists_get_eq, cons_get_inits_core, get_odd, get_append_left, ext_iff, Hindman.FS.add_two, cantorSequence_eq_self_sub_sum_cantorToTernary, get_succ_iterate', get_of_bisim, Hindman.FP.mul_two, get_append_right, getElem?_take_succ, get_zip, cantorSequence_get_succ, get_drop, get_const
|
head 📖 | CompOp | 19 mathmath: get_unfolds_head_tail, tail_inits, inits_core_eq, take_succ, head_even, head_drop, head_cons, interleave_eq, inits_eq, zip_eq, head_zip, inits_tail, head_map, unfolds_head_eq, eta, append_stream_head_tail, cons_head_tail, head_iterate, map_eq
|
inits 📖 | CompOp | 5 mathmath: tail_inits, get_inits, inits_eq, inits_tail, zip_inits_tails
|
initsCore 📖 | CompOp | 4 mathmath: tail_inits, inits_core_eq, inits_tail, cons_get_inits_core
|
instMembership 📖 | CompOp | 6 mathmath: mem_cons, mem_of_get_eq, mem_append_stream_left, mem_cycle, mem_iff_exists_get_eq, mem_const
|
interleave 📖 | CompOp | 9 mathmath: get_interleave_left, get_interleave_right, even_interleave, interleave_even_odd, interleave_tail_tail, interleave_eq, mem_interleave_left, tail_interleave, mem_interleave_right
|
iterate 📖 | CompOp | 11 mathmath: corec_def, tails_eq_iterate, iterate_id, tail_iterate, corec_id_f_eq_iterate, map_iterate, get_zero_iterate, get_succ_iterate, get_succ_iterate', iterate_eq, head_iterate
|
map 📖 | CompOp | 19 mathmath: corec_def, GenContFract.IntFractPair.coe_stream'_rat_eq, map_take, map_id, nats_eq, get_map, map_cons, map_append_stream, map_tail, map_iterate, tail_map, inits_eq, map_eq_apply, map_map, map_const, mem_map, head_map, drop_map, map_eq
|
nats 📖 | CompOp | 3 mathmath: get_nats, nats_eq, enum_eq_zip
|
odd 📖 | CompOp | 4 mathmath: even_tail, odd_eq, interleave_even_odd, get_odd
|
pure 📖 | CompOp | 5 mathmath: composition, homomorphism, map_eq_apply, identity, interchange
|
tail 📖 | CompOp | 34 mathmath: get_unfolds_head_tail, get_succ, tail_eq_drop, tails_eq_iterate, tail_iterate, tails_eq, get_tails, even_tail, drop_succ, tail_inits, odd_eq, inits_core_eq, get_tail, take_succ, map_tail, drop_tail', tail_drop, interleave_tail_tail, interleave_eq, tail_map, inits_eq, zip_eq, inits_tail, tail_even, tail_zip, tail_drop', tail_const, unfolds_head_eq, eta, tail_interleave, append_stream_head_tail, cons_head_tail, map_eq, tail_cons
|
tails 📖 | CompOp | 4 mathmath: tails_eq_iterate, tails_eq, get_tails, zip_inits_tails
|
take 📖 | CompOp | 19 mathmath: concat_take_get, take_drop, map_take, take_prefix_take_left, append_take_drop, take_succ', take_succ, dropLast_take, get_inits, take_take, append_take, take_add, take_prefix, take_append_of_le_length, getElem?_take, take_zero, take_succ_cons, length_take, getElem?_take_succ
|
unfolds 📖 | CompOp | 3 mathmath: get_unfolds_head_tail, unfolds_head_eq, unfolds_eq
|
zip 📖 | CompOp | 7 mathmath: drop_zip, zip_eq, head_zip, tail_zip, enum_eq_zip, get_zip, zip_inits_tails
|
«term_++ₛ_» 📖 | CompOp | — |
«term_::_» 📖 | CompOp | — |
«term_⊛_» 📖 | CompOp | — |
«term_⋈_» 📖 | CompOp | — |