Relation

📁 Source: Mathlib/Data/WSeq/Relation.lean

Statistics

Metric	Count
Definitions BisimO, LiftRel, LiftRelO, «term_~ʷ_»	4
Theorems imp, equivalence, ext, refl, trans, equiv, refl, swap, swap_lem, trans, imp, imp_right, swap, bind_assoc, bind_assoc_comp, bind_congr, bind_ret, cons_congr, destruct_congr, destruct_congr_iff, dropn_congr, exists_of_liftRel_left, exists_of_liftRel_right, flatten_congr, flatten_equiv, get?_congr, head_congr, join_append, join_congr, join_join, join_map_ret, join_ret, liftRel_append, liftRel_bind, liftRel_cons, liftRel_destruct, liftRel_destruct_iff, liftRel_dropn_destruct, liftRel_flatten, liftRel_join, lem, liftRel_map, liftRel_nil, liftRel_think_left, liftRel_think_right, map_congr, mem_congr, ret_bind, tail_congr, think_congr, think_equiv	51
Total	55

Stream'.WSeq

Definitions

Name	Category	Theorems
BisimO 📖	MathDef	2 math math: destruct_congr_iff, destruct_congr
LiftRel 📖	MathDef	10 math math: liftRel_cons, LiftRel.equiv, LiftRel.refl, liftRel_nil, liftRel_think_right, liftRel_destruct_iff, LiftRel.symm, liftRel_think_left, LiftRel.swap, LiftRel.trans
LiftRelO 📖	MathDef	5 math math: liftRel_join.lem, liftRel_destruct, liftRel_destruct_iff, liftRel_dropn_destruct, LiftRelO.swap
«term_~ʷ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind_assoc 📖	mathematical	—	Equiv bind	—	bind_assoc_comp
bind_assoc_comp 📖	mathematical	—	Equiv bind Stream'.WSeq	—	map_join map_comp Function.comp_assoc join_join
bind_congr 📖	mathematical	Equiv	bind	—	liftRel_bind
bind_ret 📖	mathematical	—	Equiv bind Stream'.WSeq ret map	—	map_comp join_map_ret
cons_congr 📖	mathematical	Equiv	cons	—	—
destruct_congr 📖	mathematical	Equiv	Computation.LiftRel Stream'.WSeq BisimO destruct	—	liftRel_destruct
destruct_congr_iff 📖	mathematical	—	Equiv Computation.LiftRel Stream'.WSeq BisimO destruct	—	liftRel_destruct_iff
dropn_congr 📖	mathematical	Equiv	drop	—	—
exists_of_liftRel_left 📖	—	LiftRel Stream'.WSeq membership	—	—	exists_get?_of_mem Computation.exists_of_mem_map liftRel_dropn_destruct get?_mem Computation.mem_map
exists_of_liftRel_right 📖	—	LiftRel Stream'.WSeq membership	—	—	exists_of_liftRel_left LiftRel.swap
flatten_congr 📖	mathematical	Computation.LiftRel Stream'.WSeq Equiv	flatten	—	liftRel_flatten
flatten_equiv 📖	mathematical	Stream'.WSeq Computation Computation.instMembership	Equiv flatten	—	flatten_pure Equiv.trans flatten_think
get?_congr 📖	mathematical	Equiv	Computation.Equiv get?	—	head_congr dropn_congr
head_congr 📖	mathematical	Equiv	Computation.Equiv head	—	Computation.exists_of_mem_map destruct_congr Computation.mem_map Equiv.symm
join_append 📖	mathematical	—	Equiv join append Stream'.WSeq	—	nil_append join_nil destruct_nil join_cons destruct_think Computation.destruct_think join_think cons_append think_append append_assoc destruct_cons
join_congr 📖	mathematical	LiftRel Stream'.WSeq Equiv	join	—	liftRel_join
join_join 📖	mathematical	—	Equiv join Stream'.WSeq map	—	nil_append join_nil destruct_nil join_cons join_think destruct_think map_cons map_think cons_append Computation.destruct_think think_append append_assoc destruct_cons
join_map_ret 📖	mathematical	—	Equiv join map Stream'.WSeq ret	—	join_nil destruct_nil map_cons ofList_cons join_cons cons_append nil_append destruct_think destruct_cons Computation.destruct_think map_think join_think
join_ret 📖	mathematical	—	Equiv join ret Stream'.WSeq	—	ofList_cons join_cons join_nil append_nil think_equiv
liftRel_append 📖	mathematical	LiftRel	append	—	Computation.LiftRel.imp LiftRelO.imp_right liftRel_destruct destruct_append Computation.liftRel_bind
liftRel_bind 📖	mathematical	LiftRel	bind	—	liftRel_join liftRel_map
liftRel_cons 📖	mathematical	—	LiftRel cons	—	destruct_cons
liftRel_destruct 📖	mathematical	LiftRel	Computation.LiftRel Stream'.WSeq LiftRelO destruct	—	Computation.LiftRel.imp LiftRelO.imp_right
liftRel_destruct_iff 📖	mathematical	—	LiftRel Computation.LiftRel Stream'.WSeq LiftRelO destruct	—	liftRel_destruct Computation.LiftRel.imp LiftRelO.imp_right
liftRel_dropn_destruct 📖	mathematical	LiftRel	Computation.LiftRel Stream'.WSeq LiftRelO destruct drop	—	liftRel_destruct destruct_tail Computation.liftRel_bind
liftRel_flatten 📖	mathematical	Computation.LiftRel Stream'.WSeq LiftRel	flatten	—	destruct_flatten Computation.liftRel_bind Computation.LiftRel.imp LiftRelO.imp_right flatten_pure liftRel_destruct
liftRel_join 📖	mathematical	LiftRel Stream'.WSeq	join	—	nil_append destruct_append Computation.liftRel_bind liftRel_destruct liftRel_join.lem LiftRelO.swap LiftRel.swap
liftRel_map 📖	mathematical	LiftRel	map	—	destruct_map Computation.liftRel_map liftRel_destruct
liftRel_nil 📖	mathematical	—	LiftRel nil	—	destruct_nil
liftRel_think_left 📖	mathematical	—	LiftRel think	—	liftRel_destruct_iff destruct_think
liftRel_think_right 📖	mathematical	—	LiftRel think	—	liftRel_destruct_iff destruct_think
map_congr 📖	mathematical	Equiv	map	—	liftRel_map
mem_congr 📖	mathematical	Equiv	Stream'.WSeq membership	—	exists_get?_of_mem get?_mem get?_congr Equiv.symm
ret_bind 📖	mathematical	—	Equiv bind ret	—	map_ret
tail_congr 📖	mathematical	Equiv	tail	—	flatten_congr Computation.bind_pure Computation.liftRel_bind destruct_congr Equiv.refl
think_congr 📖	mathematical	Equiv	think	—	—
think_equiv 📖	mathematical	—	Equiv think	—	Equiv.refl

Stream'.WSeq.BisimO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imp 📖	—	Stream'.WSeq.BisimO	—	—	Stream'.WSeq.LiftRelO.imp_right

Stream'.WSeq.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivalence 📖	mathematical	—	Stream'.WSeq Stream'.WSeq.Equiv	—	refl symm trans
ext 📖	mathematical	Computation.Equiv Stream'.WSeq.get?	Stream'.WSeq.Equiv	—	Computation.liftRel_def Stream'.WSeq.head_terminates_iff Computation.terminates_congr Computation.mem_unique Computation.mem_map Computation.Equiv.trans Computation.Equiv.symm Stream'.WSeq.get?_congr Stream'.WSeq.flatten_equiv Stream'.WSeq.get?_tail
refl 📖	mathematical	—	Stream'.WSeq.Equiv	—	Stream'.WSeq.LiftRel.refl
trans 📖	—	Stream'.WSeq.Equiv	—	—	Stream'.WSeq.LiftRel.trans

Stream'.WSeq.LiftRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv 📖	mathematical	—	Stream'.WSeq Stream'.WSeq.LiftRel	—	refl symm trans
refl 📖	mathematical	Reflexive	Stream'.WSeq Stream'.WSeq.LiftRel	—	Computation.LiftRel.refl
swap 📖	mathematical	—	Function.swap Stream'.WSeq Stream'.WSeq.LiftRel	—	swap_lem
swap_lem 📖	mathematical	Stream'.WSeq.LiftRel	Function.swap	—	Stream'.WSeq.LiftRelO.swap Computation.LiftRel.swap Stream'.WSeq.liftRel_destruct
trans 📖	mathematical	Transitive	Stream'.WSeq Stream'.WSeq.LiftRel	—	Stream'.WSeq.liftRel_destruct Computation.liftRel_def Computation.terminates_of_liftRel Computation.rel_of_liftRel

Stream'.WSeq.LiftRelO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imp 📖	—	Stream'.WSeq.LiftRelO	—	—	—
imp_right 📖	—	Stream'.WSeq.LiftRelO	—	—	imp
swap 📖	mathematical	—	Function.swap Stream'.WSeq Stream'.WSeq.LiftRelO	—	—

Stream'.WSeq.liftRel_join

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lem 📖	mathematical	Stream'.WSeq.LiftRel Stream'.WSeq Computation Computation.instMembership Stream'.WSeq.destruct Stream'.WSeq.join	Stream'.WSeq.LiftRelO	—	Computation.exists_results_of_mem Computation.of_results_bind Stream'.WSeq.destruct_join Computation.exists_of_liftRel_left Stream'.WSeq.liftRel_destruct Computation.Results.mem Computation.mem_bind Computation.ret_mem Computation.eq_of_pure_mem Computation.of_results_think Stream'.WSeq.destruct_append lt_of_lt_of_le Computation.think_mem

---

← Back to Index