| Metric | Count |
|---|
DefinitionsComputation, f, g, BisimO, f, IsBisimulation, LiftRel, LiftRelAux, Promises, Results, Terminates, bind, corec, destruct, empty, get, head, instAlternativeComputation, instBind, instCoeTC, instInhabited, instMembership, join, length, lmap, map, memRecOn, monad, orElse, pure, recOn, rmap, run, runFor, tail, terminatesRecOn, think, thinkN, «term_~>_», «term_~__1» | 40 |
Theoremsequivalence, refl, trans, equiv, imp, refl, swap, trans, ret_left, ret_right, swap, lem, left_unique, len_unique, length, mem, terminates, val_unique, term, bind_assoc, bind_congr, bind_promises, bind_pure, bind_pure', corec_eq, destruct_empty, destruct_eq_pure, destruct_eq_think, destruct_map, destruct_pure, destruct_think, empty_orElse, empty_promises, eq_empty_of_not_terminates, eq_of_bisim, eq_of_pure_mem, eq_thinkN, eq_thinkN', equiv_of_mem, equiv_pure_of_mem, exists_of_liftRel_left, exists_of_liftRel_right, exists_of_mem_bind, exists_of_mem_map, exists_results_of_mem, get_bind, get_eq_of_mem, get_eq_of_promises, get_equiv, get_mem, get_promises, get_pure, get_think, get_thinkN, has_bind_eq_bind, has_map_eq_map, head_empty, head_pure, head_think, instLawfulMonad, le_stable, length_bind, length_pure, length_think, length_thinkN, liftRelAux_inl_inl, liftRelAux_inl_inr, liftRelAux_inr_inl, liftRelAux_inr_inr, liftRel_bind, liftRel_congr, liftRel_def, liftRel_map, liftRel_mem_cases, liftRel_of_mem, liftRel_pure, liftRel_pure_left, liftRel_pure_right, liftRel_rec, liftRel_think_left, liftRel_think_right, lift_eq_iff_equiv, map_comp, map_congr, map_id, map_pure, map_pure', map_think, map_think', mem_bind, mem_map, mem_of_get_eq, mem_of_promises, mem_promises, mem_pure_iff, mem_unique, notMem_empty, not_terminates_empty, of_results_bind, of_results_think, of_thinkN_terminates, of_think_mem, of_think_terminates, orElse_empty, orElse_pure, orElse_think, promises_congr, pure_def, rel_of_liftRel, results_bind, results_of_terminates, results_of_terminates', results_pure, results_think, results_thinkN, results_thinkN_pure, results_think_iff, ret_bind, ret_mem, ret_orElse, ret_terminates, tail_empty, tail_pure, tail_think, terminates_bind, terminates_congr, terminates_def, terminates_iff, terminates_map, terminates_map_iff, terminates_of_liftRel, terminates_of_mem, thinkN_equiv, thinkN_mem, thinkN_terminates, think_bind, think_empty, think_equiv, think_mem, think_terminates | 140 |
| Total | 180 |
| Name | Category | Theorems |
|---|
BisimO 📖 | MathDef | — |
IsBisimulation 📖 | MathDef | — |
LiftRel 📖 | MathDef | 21 mathmath: liftRel_congr, liftRel_pure, liftRel_pure_left, Stream'.WSeq.liftRel_destruct, liftRel_think_right, Stream'.WSeq.destruct_congr_iff, LiftRel.swap, LiftRel.refl, LiftRel.equiv, LiftRel.trans, Stream'.WSeq.liftRel_destruct_iff, Stream'.WSeq.destruct_congr, LiftRelRec.lem, liftRel_pure_right, LiftRel.symm, liftRel_rec, Stream'.WSeq.liftRel_dropn_destruct, liftRel_of_mem, lift_eq_iff_equiv, liftRel_def, liftRel_think_left
|
LiftRelAux 📖 | MathDef | 7 mathmath: LiftRelAux.swap, LiftRelAux.ret_left, liftRelAux_inr_inr, liftRelAux_inr_inl, liftRelAux_inl_inl, liftRelAux_inl_inr, LiftRelAux.ret_right
|
Promises 📖 | MathDef | 5 mathmath: promises_congr, get_promises, mem_promises, parallel_congr_lem, empty_promises
|
Results 📖 | MathDef | 6 mathmath: exists_results_of_mem, results_of_terminates, results_pure, results_of_terminates', results_think_iff, results_thinkN_pure
|
Terminates 📖 | CompData | 30 mathmath: Stream'.WSeq.productive_iff, Stream'.WSeq.head_terminates_iff, Stream'.WSeq.toList_terminates, terminates_parallel, Stream'.WSeq.destruct_terminates_of_get?_terminates, terminates_map_iff, of_thinkN_terminates, not_terminates_empty, Stream'.WSeq.IsFinite.out, think_terminates, Stream'.WSeq.head_terminates, terminates_map, Stream'.WSeq.get?_terminates_le, Stream'.WSeq.Productive.get?_terminates, Results.terminates, terminates_bind, of_think_terminates, Stream'.WSeq.get?_terminates, terminates_of_mem, terminates_parallel.aux, terminates_def, terminates_congr, terminates_of_liftRel, terminates_iff, ret_terminates, Stream'.WSeq.head_terminates_of_head_tail_terminates, Stream'.WSeq.head_terminates_of_mem, liftRel_def, Stream'.WSeq.head_terminates_of_get?_terminates, thinkN_terminates
|
bind 📖 | CompOp | 16 mathmath: bind_assoc, Stream'.WSeq.destruct_join, bind_pure, results_bind, terminates_bind, bind_promises, bind_congr, liftRel_bind, has_bind_eq_bind, Stream'.WSeq.destruct_append, get_bind, think_bind, ret_bind, bind_pure', length_bind, mem_bind
|
corec 📖 | CompOp | — |
destruct 📖 | CompOp | 7 mathmath: destruct_empty, destruct_pure, LiftRelAux.ret_left, destruct_map, destruct_think, corec_eq, LiftRelAux.ret_right
|
empty 📖 | CompOp | 11 mathmath: destruct_empty, orElse_empty, not_terminates_empty, tail_empty, think_empty, parallel_empty, empty_orElse, notMem_empty, head_empty, eq_empty_of_not_terminates, empty_promises
|
get 📖 | CompOp | 12 mathmath: eq_thinkN', get_think, get_promises, get_pure, get_mem, get_eq_of_mem, results_of_terminates, get_equiv, get_thinkN, get_bind, length_bind, get_eq_of_promises
|
head 📖 | CompOp | 3 mathmath: head_pure, head_think, head_empty
|
instAlternativeComputation 📖 | CompOp | 7 mathmath: Stream'.WSeq.toList'_map, orElse_empty, ret_orElse, Stream'.WSeq.toList_cons, empty_orElse, orElse_think, orElse_pure
|
instBind 📖 | CompOp | 4 mathmath: has_bind_eq_bind, Stream'.WSeq.destruct_tail, Stream'.WSeq.destruct_dropn, Stream'.WSeq.destruct_flatten
|
instCoeTC 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
instMembership 📖 | CompOp | 20 mathmath: liftRel_pure_left, LiftRelAux.ret_left, Stream'.WSeq.exists_get?_of_mem, liftRelAux_inr_inl, Stream'.WSeq.toList_ofList, Terminates.term, get_mem, thinkN_mem, liftRelAux_inl_inr, mem_pure_iff, Mem.left_unique, liftRel_pure_right, Results.mem, LiftRelAux.ret_right, mem_of_promises, Stream'.WSeq.exists_dropn_of_mem, notMem_empty, mem_of_get_eq, ret_mem, terminates_iff
|
join 📖 | CompOp | — |
length 📖 | CompOp | 8 mathmath: length_pure, eq_thinkN', length_thinkN, Results.length, results_of_terminates, results_of_terminates', length_think, length_bind
|
lmap 📖 | CompOp | 1 mathmath: destruct_map
|
map 📖 | CompOp | 15 mathmath: map_pure, terminates_map_iff, Stream'.WSeq.destruct_map, map_id, Stream'.WSeq.length_eq_map, map_think, map_parallel, map_comp, has_map_eq_map, bind_pure, terminates_map, destruct_map, mem_map, map_congr, liftRel_map
|
memRecOn 📖 | CompOp | — |
monad 📖 | CompOp | 5 mathmath: map_think', has_map_eq_map, pure_def, instLawfulMonad, map_pure'
|
orElse 📖 | CompOp | — |
pure 📖 | CompOp | 36 mathmath: length_pure, eq_thinkN', map_pure, liftRel_pure, liftRel_pure_left, destruct_pure, Stream'.WSeq.destruct_ofSeq, Stream'.WSeq.head_ofSeq, Stream'.WSeq.head_nil, Stream'.WSeq.toList'_nil, get_pure, equiv_pure_of_mem, bind_pure, Stream'.WSeq.destruct_nil, Stream'.WSeq.drop.aux_none, ret_orElse, destruct_eq_pure, eq_thinkN, pure_def, mem_pure_iff, results_pure, liftRel_pure_right, Stream'.WSeq.flatten_pure, head_pure, Stream'.WSeq.toList_nil, Stream'.WSeq.destruct_cons, ret_mem, Stream'.WSeq.get?_ofSeq, results_thinkN_pure, ret_bind, Stream'.WSeq.head_cons, bind_pure', ret_terminates, orElse_pure, map_pure', tail_pure
|
recOn 📖 | CompOp | — |
rmap 📖 | CompOp | 2 mathmath: destruct_map, corec_eq
|
run 📖 | CompOp | — |
runFor 📖 | CompOp | — |
tail 📖 | CompOp | 3 mathmath: tail_think, tail_empty, tail_pure
|
terminatesRecOn 📖 | CompOp | — |
think 📖 | CompOp | 25 mathmath: liftRel_think_right, tail_think, think_mem, Stream'.WSeq.flatten_think, get_think, Stream'.WSeq.toList'_cons, map_think, map_think', results_think, think_terminates, Stream'.WSeq.toList_cons, think_empty, destruct_think, head_think, results_think_iff, think_equiv, orElse_think, think_bind, length_think, Stream'.WSeq.toList'_think, Stream'.WSeq.destruct_think, orElse_pure, Stream'.WSeq.head_think, liftRel_think_left, destruct_eq_think
|
thinkN 📖 | CompOp | 9 mathmath: eq_thinkN', length_thinkN, thinkN_mem, eq_thinkN, get_thinkN, results_thinkN, results_thinkN_pure, thinkN_equiv, thinkN_terminates
|
«term_~>_» 📖 | CompOp | — |
«term_~__1» 📖 | CompOp | — |