Basic

📁 Source: Cslib/Logics/HML/Basic.lean

Statistics

Metric	Count
Definitions Proposition, denotation, finiteAnd, finiteOr, neg, Satisfies, TheoryEq, propositions, theory	9
Theorems bisimulation_TheoryEq, bisimulation_satisfies, neg_denotation, neg_satisfies, not_theoryEq_satisfies, propositions_complete, propositions_satisfies_conjunction, satisfies_finiteAnd, satisfies_finiteOr, satisfies_mem_denotation, satisfies_theory, theoryEq_denotation_eq, theoryEq_eq_bisimilarity, theoryEq_isBisimulation, theoryEq_satisfies	15
Total	24

Cslib.Logic.HML

Definitions

Name	Category	Theorems
Proposition 📖	CompData	6 math math: satisfies_finiteOr, instCongruencePropositionEquiv, instIsEquivPropositionEquiv, not_theoryEq_satisfies, propositions_complete, satisfies_theory
Satisfies 📖	CompData	9 math math: satisfies_mem_denotation, neg_satisfies, satisfies_finiteOr, theoryEq_satisfies, propositions_satisfies_conjunction, satisfies_finiteAnd, Satisfies.bundled_char, not_theoryEq_satisfies, bisimulation_satisfies
TheoryEq 📖	MathDef	4 math math: theoryEq_denotation_eq, bisimulation_TheoryEq, theoryEq_isBisimulation, theoryEq_eq_bisimilarity
propositions 📖	CompOp	2 math math: propositions_satisfies_conjunction, propositions_complete
theory 📖	CompOp	1 math math: satisfies_theory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bisimulation_TheoryEq 📖	mathematical	Cslib.LTS.IsHomBisimulation	TheoryEq	—	—
bisimulation_satisfies 📖	mathematical	Cslib.LTS.IsHomBisimulation Satisfies	Satisfies	—	—
neg_denotation 📖	mathematical	—	Proposition.denotation Proposition.neg	—	—
neg_satisfies 📖	mathematical	—	Satisfies Proposition.neg	—	—
not_theoryEq_satisfies 📖	mathematical	TheoryEq	Proposition Satisfies	—	—
propositions_complete 📖	mathematical	—	Proposition propositions	—	—
propositions_satisfies_conjunction 📖	mathematical	Cslib.LTS.Tr Satisfies	Satisfies Proposition.diamond Proposition.finiteAnd propositions	—	satisfies_finiteAnd
satisfies_finiteAnd 📖	mathematical	—	Satisfies Proposition.finiteAnd	—	—
satisfies_finiteOr 📖	mathematical	—	Satisfies Proposition.finiteOr Proposition	—	—
satisfies_mem_denotation 📖	mathematical	—	Satisfies Proposition.denotation	—	—
satisfies_theory 📖	mathematical	Satisfies	Proposition theory	—	—
theoryEq_denotation_eq 📖	mathematical	—	TheoryEq Proposition.denotation	—	—
theoryEq_eq_bisimilarity 📖	mathematical	Cslib.LTS.image	TheoryEq Cslib.LTS.HomBisimilarity	—	bisimulation_TheoryEq
theoryEq_isBisimulation 📖	mathematical	Cslib.LTS.image	Cslib.LTS.IsHomBisimulation TheoryEq	—	not_theoryEq_satisfies theoryEq_satisfies
theoryEq_satisfies 📖	mathematical	TheoryEq Satisfies	Satisfies	—	—

Cslib.Logic.HML.Proposition

Definitions

Name	Category	Theorems
denotation 📖	CompOp	4 math math: Cslib.Logic.HML.theoryEq_denotation_eq, Cslib.Logic.HML.satisfies_mem_denotation, Cslib.Logic.HML.neg_denotation, equiv_def
finiteAnd 📖	CompOp	2 math math: Cslib.Logic.HML.propositions_satisfies_conjunction, Cslib.Logic.HML.satisfies_finiteAnd
finiteOr 📖	CompOp	1 math math: Cslib.Logic.HML.satisfies_finiteOr
neg 📖	CompOp	2 math math: Cslib.Logic.HML.neg_satisfies, Cslib.Logic.HML.neg_denotation

---

← Back to Index