Bisimilarity congr choice
Cslib.CCS.bisimilarity_congr_choice
Plain-language statement
P ~ Q → P + R ~ Q + R
Exact Lean statement
theorem bisimilarity_congr_choice :
(p ~[lts (defs := defs)] q) → (choice p r) ~[lts (defs := defs)] (choice q r)Formal artifact
Lean source
theorem bisimilarity_congr_choice : (p ~[lts (defs := defs)] q) → (choice p r) ~[lts (defs := defs)] (choice q r) := by intro h exists @ChoiceBisim _ _ defs constructor · constructor; assumption intro s1 s2 r μ constructor case left => intro s1' htr cases r case choice p q r hbisim => obtain ⟨rel, hr, hb⟩ := hbisim cases htr case choiceL a b c htr => obtain ⟨s2', htr2, hr2⟩ := hb.follow_fst hr htr exists s2' constructor · apply Tr.choiceL htr2 · constructor apply hb.le_bisimilarity _ _ hr2 case choiceR a b c htr => exists s1' constructor · apply Tr.choiceR htr · constructor apply HomBisimilarity.refl case bisim hbisim => obtain ⟨rel, hr, hb⟩ := hbisim obtain ⟨s2', htr2, hr2⟩ := hb.follow_fst hr htr exists s2' constructor · assumption constructor apply hb.le_bisimilarity _ _ hr2 case right => intro s2' htr cases r case choice p q r hbisim => obtain ⟨rel, hr, hb⟩ := hbisim cases htr case choiceL a b c htr => obtain ⟨s1', htr1, hr1⟩ := hb.follow_snd hr htr exists s1' constructor · apply Tr.choiceL htr1 · constructor apply hb.le_bisimilarity _ _ hr1 case choiceR a b c htr => exists s2' constructor · apply Tr.choiceR htr · constructor apply HomBisimilarity.refl case bisim hbisim => obtain ⟨rel, hr, hb⟩ := hbisim obtain ⟨s1', htr1, hr1⟩ := hb.follow_snd hr htr exists s1' constructor · assumption · constructor apply hb.le_bisimilarity _ _ hr1- Project
- Lean Computer Science Library
- License
- Apache-2.0
- Commit
- f36649cff2c9
- Source
- Cslib/Languages/CCS/BehaviouralTheory.lean:311-372
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Unique minimal
Cslib.Automata.DA.FinAcc.unique_minimal
Plain-language statement
The minimal DFA M accepting the language l is unique up to unique isomorphism.
Source project: Lean Computer Science Library
Person-level attribution pending.
Buchi Family cover
Cslib.Automata.NA.Buchi.buchiFamily_cover
Project documentation
na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.
Source project: Lean Computer Science Library
Person-level attribution pending.
Buchi Family saturation
Cslib.Automata.NA.Buchi.buchiFamily_saturation
Plain-language statement
na.buchiFamily saturates the ω-language accepted by na.
Source project: Lean Computer Science Library
Person-level attribution pending.