REVIEW 2 major objections 5 minor 38 references
Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence
T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash
Pith's one-line read The paper proves that a single syntactic format for transition rules — the (rooted) stability-respecting branching bisimulation format — makes stability-respecting, weakly divergence-preserving, and divergence-preserving branching…
desk verdict A real extension of the divide-and-congruence framework with a clever oracle-lifting proof; the key preservation lemma has an explicitly omitted subcase that must be supplied before the congruence theorems are fully established. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing object is a syntactic format for transition rules — the rooted stability-respecting branching bisimulation format (Definitions 20–21) — whose safety conditions relax the earlier branching bisimulation format. A rule is safe if right-hand sides of positive premises occur only $\Lambda$-liquid in the target; if a variable occurring only $\Lambda$-liquid in the source stays $\Lambda$-liquid throughout the rule; if a variable that is $\aleph$-frozen in the source stays $\aleph$-frozen in the premises; and the novel clause: a variable with exactly one $\aleph\cap\Lambda$-liquid occurrence in the source may occur in several positive premises or in negative premises, provided a premise $v\not\!\xrightarrow{\tau}$ is also present. This last clause is what admits the priority operator. The argument runs on two machines. First, modal decomposition (Definition 17): with every term $t$ and formula $\phi$ it associates decomposition mappings $\psi$ so that $\rho(t)\models\phi$ holds exactly when some $\psi$ has $\rho(x)\models\psi(x)$ for all variables $x$; the congruence proof reduces to showing that formulas of $\mathcal{O}^s_b$ and $\mathcal{O}^s_{rb}$ always decompose into formulas of the same class, which is Proposition 31. Second, the abstraction-free transformation $\mathrm{AFO}$ (Definition 37) with its oracle rules and the decoding map $\mathrm{dec}$: the lifting theorem (Theorem 36) uses these to transfer congruence from stability-respecting to divergence-preserving semantics by making $\sim$ and $\approx$ coincide on the transformed TSS.
What would settle it
Construct a complete standard TSS satisfying Definition 20 and a closed term in it for which the omitted $\langle\varepsilon\rangle(\phi_1\langle a\rangle\phi_2)$ case of Proposition 31 yields a decomposition mapping whose value at some variable is not equivalent to any formula of $\mathcal{O}^s_b$; equivalently, exhibit two stability-respecting branching bisimilar closed terms $p,q$ and a function symbol $f$ allowed by the format for which $f(p)$ and $f(q)$ are not stability-respecting branching bisimilar.
Extended reading notes
Core claim
On the paper's own terms, the central discovery is that the modal characterisation of stability-respecting branching bisimilarity — the logic $\mathcal{O}^s_b$, which adds the clause $\langle\varepsilon\rangle(\neg\langle\tau\rangle\top\wedge\phi)$ to the branching-bisimulation logic $\mathcal{O}_b$ — decomposes into itself under the syntactic restrictions of the (rooted) stability-respecting branching bisimulation format. That preservation result (Proposition 31) yields the congruence theorems for $\leftrightarrow^s_b$ and $\leftrightarrow^s_{rb}$ on every complete standard TSS in the format. Divergence cannot be handled inductively, so the paper proves a general lifting theorem (Theorem 36) with a transformation $\mathrm{AFO}$ that makes a TSS abstraction-free — only patience rules carry $\tau$ in their conclusions — and adds oracle transitions that certify divergence or equivalence-class membership. On the transformed TSS the finer and coarser equivalences coincide, and decoding back into the original system is compositional, so any format that is a congruence format for the coarser equivalence and is preserved by $\mathrm{AFO}$ is also a congruence format for the finer one. Instantiating the lifting to weakly divergence-preserving and divergence-preserving branching bisimilarity, rooted and unrooted, gives Theorems 58, 60, 66 and 68.
Load-bearing premise
The congruence theorems rest on Proposition 31, whose simultaneous induction leaves one case — the decomposition of formulas $\langle\varepsilon\rangle(\phi_1\langle a\rangle\phi_2)$ — unexpanded, with the paper saying only that the adaptation from the $\tau$-case is omitted; if that adaptation cannot be supplied, the claim that the format preserves the modal characterisation, and with it Theorems 32 and 33, would collapse.
Editorial extensions
If this is right
- Any complete standard TSS in the (rooted) stability-respecting branching bisimulation format makes six equivalences congruences at once: stability-respecting, weakly divergence-preserving, and divergence-preserving branching bisimilarity, in rooted and unrooted forms.
- The priority operator, whose rule has negative premises, falls inside the relaxed format, so all six semantics become congruences for it whenever the action ordering satisfies the paper's condition ($\tau$ above every $\beta > \alpha$).
- The rooted stability-respecting format also covers sequencing (the paper's Corollary 25), though the unrooted format does not, by the paper's own counterexample.
- Congruence proofs for divergence-preserving variants no longer need to be repeated from scratch: the lifting theorem shows they follow automatically from the stability-respecting case.
- The lifting framework (Theorem 36) applies to any behavioural equivalences $\sim\subseteq\approx$ containing strong bisimilarity, so the same machinery can be reused for other pairs of weak semantics.
Reading between the lines
- Because the omitted $\langle\varepsilon\rangle(\phi_1\langle a\rangle\phi_2)$ case is structurally analogous to the written $\langle\varepsilon\rangle(\phi_1\langle\hat\tau\rangle\phi_2)$ case, a likely repair is to absorb any negative premises through the conjunct $\neg\langle\tau\rangle\top$ that the format's condition 4a forces to be present; verifying that single adaptation would settle the un
- The oracle-transition technique is not specific to branching bisimilarity: it should transfer to any pair of weak equivalences where the finer one is obtained from the coarser one by adding divergence or convergence information, such as $\eta$-, delay, or weak bisimulation with their divergence-preserving variants.
- The relaxation principle behind condition 4a — negative premises are harmless as long as every problematic variable can be shown not to have a $\tau$-transition — looks like a general recipe for relaxing congruence formats for any $\tau$-based semantics whose modal logic contains a stability clause $\langle\varepsilon\rangle(\neg\langle\tau\rangle\top\wedge\phi)$.
- If the omitted adaptation turned out to be impossible, Theorem 32 would fail on a rule with negative premises and an $a$-labelled conclusion; a search for counterexamples should therefore start with operators that combine negative premises on 'a' with a $\tau$-negative premise requirement, exactly the shape of the priority operator.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper extends the modal-decomposition method for deriving congruence formats to stability-respecting branching bisimilarity and its rooted and divergence-preserving variants. It relaxes the earlier rooted branching bisimulation format by allowing rules such as the priority operator's rule to contain multiple positive or negative premises involving a variable, provided a premise that the variable cannot perform τ is present, and it proves in Theorems 32 and 33 that complete standard TSSs in this format make stability-respecting and rooted stability-respecting branching bisimilarity congruences. A second part introduces a general oracle-based lifting theorem (Theorem 36) and instantiates it in four ways to show that the same formats are also congruence formats for weakly divergence-preserving and divergence-preserving branching bisimilarity and their rooted variants (Theorems 58, 60, 66, 68). The paper includes applications to the priority operator and a sequencing operator, and it motivates the abstraction-free transformation with concrete examples.
Significance. If the main theorems are correct, the paper is a substantial addition to the divide-and-congruence programme. It shows how the modal-decomposition framework can be extended beyond weak semantics that ignore stability, and it provides a novel oracle construction that avoids a direct inductive treatment of the divergence modality. The relaxation of the format is genuinely useful: it brings the priority operator into the stability-respecting branching bisimulation format, which was previously out of scope. The parametric lifting theorem in Section 5.1 is cleanly stated and gives a reusable framework for transferring congruence formats to finer equivalences. The paper is also honest about its limitations, including the explicit note that convergent weak semantics remain outside the method. However, the technical presentation currently leaves some load-bearing proof obligations to the reader, and at least one key case is explicitly omitted.
major comments (2)
- [Section 5.3, requirement 2 of Theorem 36] The proof explicitly omits the case φ = ⟨ε⟩(φ1⟨a⟩φ2), with the sentence 'We take the liberty to omit this adaptation here.' This case is load-bearing: Proposition 31 is the sole bridge from the syntactic format to Theorems 32 and 33. The adaptation is not a purely mechanical copy of the ⟨τ⟩-hat case, because the ruloid used in Definition 17.3 has a conclusion labelled a rather than τ, and condition 4b of Definition 20 interacts with a-labelled conclusions differently: a rule with a positive τ-premise under an ℵ-liquid variable can only satisfy condition 4b if it is a patience rule, which is impossible for a non-τ conclusion. The omitted case must show in full that when condition 4a is triggered — multiple positive premises or negative premises, together with the forced premise x⁄τ→ — the resulting decomposition ψ(x) can be rewritten as a formula of the form ⟨ε⟩(¬⟨τ⟩⊤∧φ′) with φ′ in O_s^rb, taking into account that the a-modality is consumed by the ruloid and does not appear as a conjunct in ψ(x). Until this case is written out, the modal-preservation lemma, and hence the two main congruence theorems for stability-respecting branching bisimilarity, rest on an unverified claim.
- [Section 5.3, paragraph before Sect. 5.3.1] The preservation of the (rooted) stability-respecting branching bisimulation format under the AFO transformation is asserted as 'straightforward to check' and justified only by a brief heuristic. This property is load-bearing for Theorems 58, 60, 66 and 68, because it is what allows Theorem 36 to conclude that ≈_{AFO(P)} is a congruence. A complete proof should verify each condition of Definition 20 for each of the six steps of Definition 37. In particular, the new oracle rules of step 6 must be checked against condition 4a when the argument is Γ-liquid; the rules produced in steps 1–3 must be checked to ensure that no new positive τ-premises are created, so that condition 4b is preserved; and the added negative ι-premises of step 3 must be shown to satisfy condition 4a together with the retained τ-premises. The two-sentence sketch in Section 5.3 does not provide this verification, and the reader is left to reconstruct a substantial technical argument.
minor comments (5)
- [Section 4.2, proof of Proposition 31, Case 2.2] In the last sentence of Case 2.2, 'by induction ξ(y) ∈ O_s^b' should read 'by induction χ(y) ∈ O_s^b'; the variable ξ is not introduced in that case.
- [Section 4.2, proof of Proposition 31, Case 1.1 for φ = ⟨ε⟩(¬⟨τ⟩⊤∧φ)] The sentence 'This gives rise to a ξ ∈ h^{-1}(x) such that ξ(x) = ¬⟨τ⟩⊤' appears to have the negation in the wrong place: the patience ruloid gives ξ(x) = ⟨τ⟩⊤, so that the conjunct ¬ξ(x) contributes ¬⟨τ⟩⊤ as needed.
- [Section 4.1, Example 24] The sentence 'Then p↔b q, but p;r↔ p⁄↔b r↔ q;r' appears garbled; it should be rewritten to say clearly that p;r and q;r are not branching bisimilar.
- [Section 5.2, Definition 37 and following] It would help to state explicitly that when Definitions 1 and 2 are applied to AFO(P) and K, the set A is taken to be the enlarged set of non-τ actions, including O and ι, so that oracle and ι transitions are treated as ordinary observable labels in the bisimulation clauses and in the modal characterisation. Without this clarification, the use of branching bisimulation for Δ⊤-transitions in Proposition 54 is under-specified.
- [Section 5.3.2, Corollary 59] The phrase 'Rooted F' should be replaced by something like 'the rooted format F' for readability.
Circularity Check
No significant circularity; the omitted ⟨ε⟩(φ1⟨a⟩φ2) subcase is an unverified adaptation, not a circular step.
full rationale
The derivation chain is not circular. Theorems 32, 33, 58, 60, 66 and 68 are obtained from the modal-decomposition theorem of [15] plus Proposition 31, which proves preservation of the stability-respecting modal characterisations O^s_b and O^s_rb under decomposition. Proposition 31 is proved by simultaneous induction, and the genuinely new ingredients — the stability clause ⟨ε⟩(¬⟨τ⟩⊤∧φ) and the relaxed ruloid condition 4a of Definition 20 — are handled explicitly for the ⟨τ⟩-modality and for the stability clause. The one unproved subcase is ϕ = ⟨ε⟩(ϕ1⟨a⟩ϕ2), where the text says: “The proof of the case ϕ = ⟨ε⟩(ϕ1⟨a⟩ϕ2) in Ob from [15, Prop. 3] needs to be adapted in a similar fashion as the case ϕ = ⟨ε⟩(ϕ1⟨ˆτ⟩ϕ2). We take the liberty to omit this adaptation here.” This is an incompleteness in the proof of the key lemma and therefore a genuine correctness risk for Theorems 32 and 33, but it is not circularity: the claim does not reduce by definition to a premise, no fitted parameter is renamed as a prediction, and the appeal to [15] is to a prior published decomposition framework, not to the stability-respecting conclusion itself. The divergence-preserving results in Section 5 are established through a new oracle-based abstraction-free transformation, with separate proofs that the relevant equivalences coincide on AFO(P); these arguments do not presuppose the target congruence theorems.
Assumptions & free parameters
assumptions (5)
- domain assumption Well-supported proof semantics from [17] is consistent and complete TSSs define LTSs.
- standard math Modal decomposition theorem (Theorem 18 of [15]) is correct for the full modal logic O.
- standard math Ruloid transformation from [6] preserves ws-provability and the ready simulation format.
- ad hoc to paper For the divergence-preserving case, the oracle action set O contains a unique name for each ↔Δ_b-equivalence class of processes in G.
- domain assumption All TSSs considered are complete standard TSSs.
invented entities (3)
-
Oracle transitions (labels Δ⊤ or unique class names) on constants p̂
-
Fresh internal action ι
-
Abstraction-free oracle transformation AFO(P)
Cite this review
Pith. "Pith review of Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence." pith.science (2026). https://pith.science/paper/LCANUNTL
@misc{pith2026190806550,
author = {Pith},
title = {Pith review of: Divide and Congruence III: From Decomposition of Modal Formulas to Preservation of Stability and Divergence},
year = {2026},
howpublished = {\url{https://pith.science/paper/LCANUNTL}},
note = {Machine review of arXiv:1908.06550}
}
abstract
In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a $\tau$-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of $\tau$-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.
Figures
Reference graph
Works this paper leans on
-
[15]
W.J. F OKKINK , R.J. VAN GLABBEEK & P. DE WIND (2012): Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity. Information and Computation 214, pp. 59–85
work page 2012
-
[1]
J.C.M. B AETEN , J.A. B ERGSTRA & J.W. K LOP (1986): Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae 9(2), pp. 127–167
work page 1986
-
[2]
J.C.M. B AETEN , B. L UTTIK & F. Y ANG (2017): Sequential composition in the presence of intermediate termination (extended abstract). In Proc. EXPRESS/SOS’17, EPTCS 255, pp. 1-17
work page 2017
-
[3]
T. B ASTEN (1996): Branching bisimulation is an equivalence indeed! Information Processing Letters 58(3), pp. 141–147
work page 1996
-
[4]
B LOOM (1994): When is partial trace equivalence adequate? Formal Aspects of Computing 6, pp
B. B LOOM (1994): When is partial trace equivalence adequate? Formal Aspects of Computing 6, pp. 317–338
work page 1994
-
[5]
B LOOM (1995): Structural operational semantics for weak bisimulations
B. B LOOM (1995): Structural operational semantics for weak bisimulations. Theoretical Computer Science 146(1/2), pp. 25–68
work page 1995
-
[6]
B. B LOOM , W.J. F OKKINK & R.J. VAN GLABBEEK (2004): Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic 5(1), pp. 26–78
work page 2004
-
[7]
B. B LOOM , S. I STRAIL & A.R. M EYER (1995): Bisimulation can’t be traced. Journal of the ACM 42(1), pp. 232–268
work page 1995
Show all 38 references
-
[8]
B OL & J.F
R.N. B OL & J.F. G ROOTE (1996): The meaning of negative premises in transition system specifications. Journal of the ACM 43(5), pp. 863–914
1996
-
[9]
F OKKINK (2000): Rooted branching bisimulation as a congruence
W.J. F OKKINK (2000): Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences 60(1), pp. 13–37
2000
-
[10]
F OKKINK & R.J
W.J. F OKKINK & R.J. VAN GLABBEEK (1996): Ntyft/ntyxt rules reduce to ntree rules. Information and Computation 126(1), pp. 1–10
1996
-
[11]
F OKKINK & R.J
W.J. F OKKINK & R.J. VAN GLABBEEK (2016): Divide and congruence II: Delay and weak bisimilarity. In Proc. LICS’16, pp. 778–787, ACM/IEEE
2016
-
[12]
F OKKINK & R.J
W.J. F OKKINK & R.J. VAN GLABBEEK (2017): Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity. Information and Computation 257, pp. 79–113
2017
-
[13]
F OKKINK , R.J
W.J. F OKKINK , R.J. VAN GLABBEEK & B. L UTTIK (2017): Divide and congruence III: Stability & di- vergence. In Proc. CONCUR’17, LIPIcs 85, pp. 15:1–15:16, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Infor- matik
2017
-
[14]
F OKKINK , R.J
W.J. F OKKINK , R.J. VAN GLABBEEK & P. DE WIND (2006): Divide and congruence: From decomposition of modalities to preservation of branching bisimulation. In Proc. FMCO’05, LNCS 4111, pp. 195–218, Springer
2006
-
[16]
VAN GLABBEEK (1993): The linear time-branching time spectrum II: The semantics of sequential systems with silent moves
R.J. VAN GLABBEEK (1993): The linear time-branching time spectrum II: The semantics of sequential systems with silent moves. In Proc. CONCUR’93, LNCS 715, pp. 66–81. Springer
1993
-
[17]
VAN GLABBEEK (2004): The meaning of negative premises in transition system specifications II
R.J. VAN GLABBEEK (2004): The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming 60/61, pp. 229–258. W.J. Fokkink, R.J. van Glabbeek & B. Luttik 39
2004
-
[18]
VAN GLABBEEK , B
R.J. VAN GLABBEEK , B. L UTTIK & N. T R ˘CKA (2009): Branching bisimilarity with explicit divergence. Fundamenta Informaticae, 93(4) pp. 371–392
2009
-
[19]
VAN GLABBEEK , B
R.J. VAN GLABBEEK , B. L UTTIK & N. T R ˘CKA (2009): Computation tree logic with deadlock detection. Logical Methods in Computer Science 5(4):5
2009
-
[20]
VAN GLABBEEK & W.P
R.J. VAN GLABBEEK & W.P. WEIJLAND (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600
1996
-
[21]
G ROOTE (1993): Transition system specifications with negative premises.Theoretical Computer Science 118(2), pp
J.F. G ROOTE (1993): Transition system specifications with negative premises.Theoretical Computer Science 118(2), pp. 263–299
1993
-
[22]
G ROOTE & F.W
J.F. G ROOTE & F.W. VAANDRAGER (1992): Structured operational semantics and bisimulation as a con- gruence. Information and Computation 100(2), pp. 202–260
1992
-
[23]
H ENNESSY & R
M. H ENNESSY & R. M ILNER (1985): Algebraic laws for non-determinism and concurrency. Journal of the ACM 32(1), pp. 137–161
1985
-
[24]
L ANGERAK (1989): A testing theory for LOTOS using deadlock detection
R. L ANGERAK (1989): A testing theory for LOTOS using deadlock detection. In E. Brinksma, G. Scollo & C.A. Vissers, editors: Proceedings 9th IFIP WG6.1 International Symposium on Protocol Specification, Testing, and Verification,Enschede, The Netherlands
1989
-
[25]
M ILNER (1989): Communication and Concurrency
R. M ILNER (1989): Communication and Concurrency. Prentice-Hall
1989
-
[26]
M OUSAVI , I
M.R. M OUSAVI , I. P HILLIPS , M.A. R ENIERS & I. U LIDOWSKI (2009): Semantics and expressiveness of ordered SOS. Information and Computation 207, pp. 85–119
2009
-
[27]
P HILLIPS (1987): Refusal testing
I. P HILLIPS (1987): Refusal testing. Theoretical Computer Science 50, pp. 241–284
1987
-
[28]
P LOTKIN (2004): A structural approach to operational semantics
G.D. P LOTKIN (2004): A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60/61, pp. 17–139. Originally appeared in 1981
2004
-
[29]
P OMELLO (1986): Some equivalence notions for concurrent systems – An overview
L. P OMELLO (1986): Some equivalence notions for concurrent systems – An overview. In G. Rozenberg, editor: Advances in Petri Nets 1985, LNCS 222, Springer, pp. 381–400
1986
-
[30]
U LIDOWSKI (1992): Equivalences on observable processes
I. U LIDOWSKI (1992): Equivalences on observable processes. In Proc. LICS’92, pp. 148–159. IEEE
1992
-
[31]
U LIDOWSKI & I
I. U LIDOWSKI & I. P HILLIPS (2002): Ordered SOS rules and process languages for branching and eager bisimulations. Information and Computation 178, pp. 180–213
2002
-
[32]
U LIDOWSKI & S
I. U LIDOWSKI & S. Y UEN (2000): Process languages for rooted eager bisimulation.In Proc. CONCUR’00, LNCS 1877, pp. 275–289. Springer
2000
-
[33]
V AANDRAGER (1990): Algebraic Techniques for Concurrency and their Application
F.W. V AANDRAGER (1990): Algebraic Techniques for Concurrency and their Application . PhD thesis, University of Amsterdam
1990
-
[34]
W ALKER (1990): Bisimulation and divergence
D. W ALKER (1990): Bisimulation and divergence. Information and Computation 85, pp. 202–241. 40 Divide and Congruence III: Stability and Divergence A Modal characterisations We prove Thm. 8, which states thatOs b is a modal characterisation of p↔s b q, and Os rb of p↔s rb q. S...
1990
-
[35]
Since p1|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2, by induction on n, q|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2
Either p1↔s b q. Since p1|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2, by induction on n, q|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2
-
[36]
Since p1|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2, by induction on n, q′′|= ⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2
Or q ε=⇒ q′ τ−→q′′ with p1↔s b q′′. Since p1|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2, by induction on n, q′′|= ⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2. Hence q|=⟨ε⟩ϕ1⟨ ˆτ⟩ϕ2. • ϕ =⟨ε⟩ϕ1⟨a⟩ϕ2. Then for some n there are p0, . . . ,pn∈ P with p0 = p, pi τ−→ pi+1 for i∈ {0, . . . ,n− 1}, and pn|= ϕ1⟨a⟩ϕ2. We apply induction on n. n ...
-
[37]
Since p|=⟨ε⟩ϕ⟨α⟩ψ∈ Os b and p∼Os b q, also q|=⟨ε⟩ϕ⟨α⟩ψ
α⁄= τ. Since p|=⟨ε⟩ϕ⟨α⟩ψ∈ Os b and p∼Os b q, also q|=⟨ε⟩ϕ⟨α⟩ψ. Hence q ε=⇒ q′ α−→q′′ with q′|= ϕ and q′′|= ψ. By the definition of ϕ and ψ it follows that p∼Os b q′ and p′∼Os b q′′
-
[38]
Let ˜ϕ∈ Os b such that p′|= ˜ϕ and p,q⁄|= ˜ϕ
α = τ and p′⁄∼Os b q. Let ˜ϕ∈ Os b such that p′|= ˜ϕ and p,q⁄|= ˜ϕ. Since p|=⟨ε⟩ϕ⟨ ˆτ⟩( ˜ϕ∧ ψ)∈ Os b and p∼Os b q, also q|=⟨ε⟩ϕ⟨ ˆτ⟩( ˜ϕ∧ ψ). So q ε=⇒ q′ with q′|= ϕ⟨ ˆτ⟩( ˜ϕ∧ ψ). By definition of ϕ it follows that p∼Os b q′. Thus q′⁄|= ˜ϕ, so q′ τ−→q′′ with q′′|= ˜ϕ∧ ψ. By the...
Reviewed August 14, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.