| Metric | Count |
|---|
DefinitionsIsSeq, BisimO, f, IsBisimulation, TerminatedAt, Terminates, append, coeList, coeMLList, coeStream, cons, corec, destruct, drop, enum, fold, forceToList, get?, head, instInhabited, instMembership, join, length, length', map, nats, nil, ofList, ofMLList, ofStream, omap, recOn, splitAt, tail, take, terminatedAtDecidable, toList, toList', toListOrStream, toMLList, toStream, unzip, update, zip, zipWith, Seq1 | 46 |
Theoremscoinduction, coinduction2, cons_eq_cons, cons_injective2, cons_left_injective, cons_ne_nil, cons_not_terminatedAt_zero, cons_right_injective, cons_terminatedAt_succ_iff, corec_cons, corec_eq, corec_nil, destruct_cons, destruct_eq_cons, destruct_eq_none, destruct_nil, eq_of_bisim, eq_of_bisim', eq_of_bisim_strong, eq_or_mem_of_mem_cons, ext, ext_iff, ge_stable, get?_cons_succ, get?_cons_zero, get?_mem, get?_mk, get?_nil, get?_tail, get?_zero_eq_none, head_cons, head_eq_destruct, head_eq_none, head_eq_none_iff, head_eq_some, head_nil, le_stable, mem_cons, mem_cons_iff, mem_cons_of_mem, mem_iff_exists_get?, mem_rec_on, nil_ne_cons, notMem_nil, not_terminates_iff, ofList_cons, ofList_get?, ofList_injective, ofList_nil, tail_cons, tail_nil, terminatedAt_nil, terminatedAt_zero_iff, terminated_stable, terminates_cons_iff, terminates_nil, val_cons, val_eq_get | 58 |
| Total | 104 |
| Name | Category | Theorems |
|---|
BisimO 📖 | MathDef | — |
IsBisimulation 📖 | MathDef | — |
TerminatedAt 📖 | MathDef | 12 mathmath: length_le_iff, cons_terminatedAt_succ_iff, terminatedAt_map_iff, length'_le_iff, toList_nil, terminatedAt_zero_iff, cons_not_terminatedAt_zero, terminatedAt_nil, terminatedAt_ofList, GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAt, length_le_iff', GenContFract.terminatedAt_iff_s_terminatedAt
|
Terminates 📖 | MathDef | 5 mathmath: terminates_cons_iff, terminates_ofList, terminates_map_iff, not_terminates_iff, terminates_nil
|
append 📖 | CompOp | 10 mathmath: ofStream_append, map_append, join_append, append_nil, ofList_append, append_assoc, mem_append_left, join_cons, cons_append, nil_append
|
coeList 📖 | CompOp | — |
coeMLList 📖 | CompOp | — |
coeStream 📖 | CompOp | — |
cons 📖 | CompOp | 49 mathmath: Pairwise_cons_nil, ofList_cons, tail_cons, Tactic.ComputeAsymptotics.Seq.dist_cons_nil, cons_terminatedAt_succ_iff, cons_injective2, Tactic.ComputeAsymptotics.Seq.gcorec_some, update_cons_zero, join_cons_cons, take_succ_cons, terminates_cons_iff, destruct_eq_cons, get?_cons_zero, drop_succ_cons, map_cons, length'_cons, Tactic.ComputeAsymptotics.Seq.dist_cons_cons_eq_one, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point, cons_left_injective, set_cons_succ, ofStream_cons, Tactic.ComputeAsymptotics.Seq.dist_cons_cons, length'_ne_zero_iff_cons, cons_not_terminatedAt_zero, Tactic.ComputeAsymptotics.Seq.dist_nil_cons, cons_right_injective, mem_cons_of_mem, fold_cons, cons_eq_cons, head_cons, join_cons_nil, get?_cons_succ, Stream'.Seq1.join_cons, zipWith_cons_cons, join_cons, mem_cons, destruct_cons, fold_nil, head_eq_some, cons_append, enum_cons, zip_cons_cons, length_cons, update_cons_succ, mem_cons_iff, set_cons_zero, val_cons, corec_cons, Pairwise.cons
|
corec 📖 | CompOp | — |
destruct 📖 | CompOp | 11 mathmath: Stream'.WSeq.seq_destruct_cons, Stream'.WSeq.seq_destruct_think, Stream'.WSeq.toList'_map, Stream'.WSeq.seq_destruct_nil, destruct_nil, Stream'.WSeq.toList'_nil, Stream'.WSeq.toList'_cons, corec_eq, destruct_cons, head_eq_destruct, Stream'.WSeq.toList'_think
|
drop 📖 | CompOp | 13 mathmath: dropn_tail, all_coind_drop_motive, drop_succ_cons, Pairwise_drop, drop_length', dropn_add, Stream'.WSeq.dropn_ofSeq, drop_zero, take_drop, drop_get?, drop_nil, drop_set_of_lt, head_dropn
|
enum 📖 | CompOp | 3 mathmath: get?_enum, enum_nil, enum_cons
|
fold 📖 | CompOp | 3 mathmath: fold_cons, fold_nil, fold_head
|
forceToList 📖 | CompOp | — |
get? 📖 | CompOp | 42 mathmath: lt_length_iff, nats_get?, get?_tail, get?_zipWith, get?_zero_eq_none, GenContFract.terminatedAt_iff_partNum_none, get?_cons_zero, get?_enum, get?_nil, val_eq_get, get?_set_of_not_terminatedAt, mem_iff_exists_get?, get?_zip, GenContFract.of_s_head_aux, GenContFract.coe_of_s_get?_rat_eq, getElem?_toList, ext_iff, GenContFract.squashSeq_nth_of_lt, not_terminates_iff, GenContFract.IntFractPair.get?_seq1_eq_succ_get?_stream, get?_cons_succ, GenContFract.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero, map_get?, get?_set_of_terminatedAt, GenContFract.partNum_none_iff_s_none, get?_mk, GenContFract.get?_of_eq_some_of_succ_get?_intFractPair_stream, getElem?_take, Stream'.WSeq.get?_ofSeq, get?_update, GenContFract.terminatedAt_iff_s_none, getLast?_toList, drop_get?, GenContFract.squashGCF_nth_of_lt, GenContFract.terminatedAt_iff_partDen_none, head_dropn, get?_set_of_ne, lt_length'_iff, lt_length_iff', GenContFract.of_s_succ, GenContFract.partDen_none_iff_s_none, ofList_get?
|
head 📖 | CompOp | 10 mathmath: Stream'.WSeq.destruct_ofSeq, Stream'.WSeq.head_ofSeq, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.ite, head_eq_none_iff, GenContFract.of_s_head, head_cons, head_eq_destruct, head_nil, fold_head, head_dropn
|
instInhabited 📖 | CompOp | — |
instMembership 📖 | CompOp | 5 mathmath: mem_iff_exists_get?, notMem_nil, get?_mem, mem_cons, mem_cons_iff
|
join 📖 | CompOp | 10 mathmath: join_cons_cons, Stream'.Seq1.join_map_ret, join_append, join_cons_nil, Stream'.Seq1.join_cons, join_cons, Stream'.Seq1.map_join', Stream'.Seq1.join_join, Stream'.Seq1.join_nil, join_nil
|
length 📖 | CompOp | 11 mathmath: lt_length_iff, length_le_iff, length_nil, length'_of_terminates, length_toList, length_map, length_eq_zero, length_le_iff', length_cons, getLast?_toList, lt_length_iff'
|
length' 📖 | CompOp | 10 mathmath: length'_of_terminates, length'_le_iff, length'_cons, drop_length', length'_nil, at_least_as_long_as_coind, length'_of_not_terminates, length'_eq_zero_iff_nil, length'_map, lt_length'_iff
|
map 📖 | CompOp | 25 mathmath: map_id, GenContFract.coe_of_s_rat_eq, terminatedAt_map_iff, map_append, zip_map_right, map_cons, Stream'.Seq1.join_map_ret, zip_map_left, zipWith_map_left, GenContFract.coe_of_rat_eq, map_nil, map_tail, terminates_map_iff, map_comp, GenContFract.coe_toGenContFract, Stream'.Seq1.map_pair, Stream'.Seq1.map_join', length'_map, Stream'.Seq1.join_join, map_get?, zipWith_map, enum_cons, zipWith_map_right, zip_map, mem_map
|
nats 📖 | CompOp | 1 mathmath: nats_get?
|
nil 📖 | CompOp | 42 mathmath: Pairwise_cons_nil, Tactic.ComputeAsymptotics.Seq.dist_cons_nil, Tactic.ComputeAsymptotics.Seq.gcorec_nil, length_nil, get?_zero_eq_none, destruct_nil, toList_nil, length_eq_zero, get?_nil, destruct_eq_none, Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point, terminatedAt_zero_iff, length'_nil, map_nil, corec_nil, append_nil, Tactic.ComputeAsymptotics.Seq.dist_nil_cons, set_nil, head_eq_none_iff, notMem_nil, GenContFract.of_s_of_int, terminatedAt_nil, Pairwise.nil, length'_eq_zero_iff_nil, join_cons_nil, zipWith_nil_left, update_nil, tail_nil, enum_nil, zipWith_nil_right, head_eq_none, Stream'.Seq1.join_nil, take_nil, fold_nil, drop_nil, head_nil, nil_append, ofList_nil, terminates_nil, zip_nil_right, join_nil, zip_nil_left
|
ofList 📖 | CompOp | 10 mathmath: ofList_cons, ofStream_append, ofList_append, toList_ofList, terminates_ofList, ofList_toList, terminatedAt_ofList, ofList_nil, ofList_injective, ofList_get?
|
ofMLList 📖 | CompOp | — |
ofStream 📖 | CompOp | 2 mathmath: ofStream_append, ofStream_cons
|
omap 📖 | CompOp | 1 mathmath: corec_eq
|
recOn 📖 | CompOp | — |
splitAt 📖 | CompOp | — |
tail 📖 | CompOp | 13 mathmath: dropn_tail, get?_tail, tail_cons, Stream'.WSeq.destruct_ofSeq, GenContFract.squashSeq_succ_n_tail_eq_squashSeq_tail_n, map_tail, GenContFract.convs'Aux_succ_some, tail_nil, GenContFract.of_s_tail, Stream'.WSeq.tail_ofSeq, head_eq_some, Tactic.ComputeAsymptotics.Seq.dist_eq_half_of_head, Pairwise_tail
|
take 📖 | CompOp | 8 mathmath: take_succ_cons, length_take_of_le_length, take_zero, get?_mem_take, take_nil, take_drop, getElem?_take, length_take_le
|
terminatedAtDecidable 📖 | CompOp | — |
toList 📖 | CompOp | 6 mathmath: length_toList, toList_nil, toList_ofList, getElem?_toList, ofList_toList, getLast?_toList
|
toList' 📖 | CompOp | — |
toListOrStream 📖 | CompOp | — |
toMLList 📖 | CompOp | — |
toStream 📖 | CompOp | — |
unzip 📖 | CompOp | — |
update 📖 | CompOp | 4 mathmath: update_cons_zero, update_nil, get?_update, update_cons_succ
|
zip 📖 | CompOp | 7 mathmath: zip_map_right, zip_map_left, get?_zip, zip_cons_cons, zip_map, zip_nil_right, zip_nil_left
|
zipWith 📖 | CompOp | 7 mathmath: get?_zipWith, zipWith_map_left, zipWith_nil_left, zipWith_cons_cons, zipWith_nil_right, zipWith_map, zipWith_map_right
|