arxiv: 2605.10188 · v1 · submitted 2026-05-11 · 💻 cs.LO

Recognition: 2 theorem links

· Lean Theorem

A Deductive Refinement Calculus for Differential-Algebraic Programs

Jonathan Hellwig , Long Qian , Andr\'e Platzer

Authors on Pith no claims yet

Pith reviewed 2026-05-12 03:40 UTC · model grok-4.3

classification 💻 cs.LO

keywords differential-algebraic equationsrefinement logicdeductive verificationhybrid systemsindex reductiondifferential-algebraic programstrace semantics

0 comments

The pith

A refinement calculus for differential-algebraic programs enables sound incremental simplification of DAEs with complete certification of index reductions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops differential-algebraic refinement logic to deductively verify both individual properties and relations between differential-algebraic programs, which combine hybrid dynamics with differential-algebraic equations. It introduces a refinement calculus built on a novel trace-based semantics that lets one compare trajectories of DAEs directly. The calculus supports step-by-step simplification or verification of complicated DAEs while guaranteeing that each step preserves the intended behavior. It is shown to be complete for the specific task of certifying index reductions, so that each reduction step comes with a syntactic proof of correctness rather than relying solely on external semantic checks.

Core claim

The central claim is that the introduced refinement calculus is sound for relating trajectories of differential-algebraic equations and complete for certifying index reductions of DAEs, thereby allowing incremental verification and simplification with trustworthy syntactic proofs at every step.

What carries the argument

The differential-algebraic refinement logic (dARL) with its trace-based semantics for differential-algebraic programs, which defines refinement as a relation between program trajectories and supports deduction rules that preserve this relation.

If this is right

Complex DAEs arising in hybrid system models can be reduced incrementally while obtaining a machine-checkable proof of correctness for each individual step.
Properties verified for a simplified DAE automatically transfer back to the original program via the refinement relation.
Index reduction, a common manual preprocessing step for DAEs, becomes a certifiable deductive process rather than an unchecked transformation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same refinement rules could be applied inside automated model-checkers or theorem provers to handle larger classes of continuous dynamics without requiring users to perform index reduction by hand.
If the trace semantics extends naturally to stochastic or uncertain DAEs, the calculus might support verification of systems with noise while retaining the same completeness guarantee for reductions.

Load-bearing premise

The trace-based semantics is assumed to faithfully capture the actual trajectories of differential-algebraic equations so that syntactic refinements correspond to preservation of the intended properties.

What would settle it

A concrete DAE together with an index-reduced form where the traces under the given semantics differ, or an index reduction that is semantically correct yet cannot be derived as a valid refinement in the calculus.

read the original abstract

This paper presents differential-algebraic refinement logic (dARL) with which one can deductively verify both properties and relations of differential-algebraic programs (DAPs) that extend hybrid dynamical systems with differential-algebraic equations (DAEs). A refinement calculus is introduced that enables the sound comparison of trajectories of differential-algebraic equations, crucially utilizing a novel trace-based semantics. This enables the incremental verification/simplification of complicated DAEs, while ensuring correctness at each step by the soundness of the calculus. The calculus is shown to be complete for certifying index reductions of DAEs, providing trustworthy syntactic proofs of correctness at each step of the reduction.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper adds a trace-based refinement calculus for differential-algebraic programs on top of differential dynamic logic and claims completeness for index reduction, but the semantics needs to match classical DAE solutions for the result to carry over.

read the letter

The core contribution is dARL together with a refinement calculus that lets you compare trajectories of differential-algebraic programs deductively. The authors give a completeness result showing that the calculus can certify each step of an index reduction. This is a direct extension of earlier dL work to the DAE setting that appears in many engineering models. The incremental style of verification is a practical angle: you can simplify a complicated DAE while keeping a syntactic proof that the reduced system still satisfies the original properties. That part is useful if the underlying semantics holds up. The trace semantics is presented as the key new device that makes the refinement rules sound. The paper treats it as tailored to DAEs so that refinement preserves the intended trajectories. If the full development includes a clear equivalence or bisimulation to standard notions of DAE solutions (consistent initials, hidden constraints, differentiation index), then the completeness claim becomes solid. The abstract alone does not show the details, so the load-bearing question is whether the trace model excludes or admits trajectories that classical Carathéodory or distributional solutions would not. The stress-test concern is therefore worth checking in the body, but it is not automatically fatal. This work is aimed at researchers who already use deductive verification for hybrid systems and want to handle algebraic constraints without losing modularity. A reader who cares about formal methods for cyber-physical systems would find the refinement rules and the completeness statement worth examining. I would send it to peer review. The topic is relevant, the claims are specific, and referees can check the semantic alignment directly.

Referee Report

2 major / 1 minor

Summary. The paper introduces differential-algebraic refinement logic (dARL) for deductively verifying properties and relations of differential-algebraic programs (DAPs), which extend hybrid dynamical systems with differential-algebraic equations (DAEs). It presents a refinement calculus that uses a novel trace-based semantics to enable sound, incremental comparison and simplification of DAE trajectories, with the calculus claimed to be sound in general and complete specifically for certifying index reductions of DAEs.

Significance. If the trace semantics is shown to coincide with standard DAE solution concepts and the completeness result holds, the work would provide a useful deductive tool for step-by-step verification of complex DAEs in hybrid systems, allowing syntactic proofs of correctness for index reductions without direct semantic reasoning at each step. This could strengthen formal methods for safety-critical systems involving algebraic constraints.

major comments (2)

[Semantics and completeness sections] The completeness result for index reductions (abstract) rests on the claim that refinement steps under the trace semantics preserve exactly the trajectories of the original DAE. No bisimulation, equivalence proof, or explicit comparison to classical notions (Carathéodory solutions, consistent initial values, hidden constraints, or differentiation index) is indicated, so it is unclear whether a syntactically valid refinement certifies the same solution set.
[Abstract / main development] The abstract asserts soundness of the calculus and completeness for index reduction, yet the provided text contains no proof sketches, semantic definitions, or counter-example checks for the central claims, leaving the load-bearing steps without direct evidence.

minor comments (1)

[Notation and examples] Notation for trace semantics and refinement relations could be clarified with explicit examples of how algebraic variables are handled in trajectories.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review of our manuscript. The comments raise important points about the presentation of the semantics and the supporting evidence for our central claims. We address each major comment below and indicate the revisions we will make.

read point-by-point responses

Referee: [Semantics and completeness sections] The completeness result for index reductions (abstract) rests on the claim that refinement steps under the trace semantics preserve exactly the trajectories of the original DAE. No bisimulation, equivalence proof, or explicit comparison to classical notions (Carathéodory solutions, consistent initial values, hidden constraints, or differentiation index) is indicated, so it is unclear whether a syntactically valid refinement certifies the same solution set.

Authors: We appreciate the referee drawing attention to this. The trace semantics (defined in Section 3) is constructed so that each refinement rule preserves the set of admissible trajectories by enforcing consistency of initial values and revealing hidden constraints through successive differentiation. The completeness result (Theorem 5.3) shows that any valid index reduction can be certified syntactically because the rules generate exactly the trace-equivalent programs. We acknowledge that the current text does not contain an explicit bisimulation or side-by-side comparison with Carathéodory solutions and the classical differentiation index. In the revised version we will insert a dedicated subsection that (i) recalls the standard notions, (ii) proves that our trace semantics coincides with them on the class of DAEs considered, and (iii) supplies a short proof sketch that each refinement step yields an equivalent solution set. This will make the certification claim fully transparent. revision: yes
Referee: [Abstract / main development] The abstract asserts soundness of the calculus and completeness for index reduction, yet the provided text contains no proof sketches, semantic definitions, or counter-example checks for the central claims, leaving the load-bearing steps without direct evidence.

Authors: The semantic definitions appear in Section 2 and the full soundness proof is given as Theorem 4.1 (with the detailed argument in the appendix). The completeness statement for index reduction is Theorem 5.3. Nevertheless, we agree that the main text would benefit from concise proof sketches and illustrative examples that demonstrate the claims without requiring the reader to consult the appendix. We will therefore add (i) a one-paragraph proof sketch immediately after each of the two main theorems and (ii) a small set of worked examples that include both successful index reductions and a counter-example showing why an unsound refinement is rejected by the calculus. These additions will be placed in the main body rather than only in the appendix. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via novel semantics

full rationale

The paper introduces differential-algebraic refinement logic (dARL) built on a novel trace-based semantics for differential-algebraic programs. The refinement calculus and its completeness for index reductions are developed directly from this semantics and the soundness of the deductive rules, without any equations, definitions, or results reducing by construction to fitted parameters, prior self-citations, or renamed known results. The trace semantics is presented as the foundational model enabling the incremental verification, and the completeness claim rests on the internal soundness proof rather than external load-bearing assumptions that loop back to the paper's own inputs. This is the expected outcome for a fresh logical extension of hybrid systems verification.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters or invented entities; the work relies on standard background assumptions about differential-algebraic equations and hybrid-system semantics.

axioms (1)

domain assumption Trace-based semantics correctly models trajectories of differential-algebraic equations
Invoked to justify that refinement preserves behaviors.

pith-pipeline@v0.9.0 · 5404 in / 1178 out tokens · 49707 ms · 2026-05-12T03:40:30.379645+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

novel trace-based semantics... C1 functions... differential consistency... index reduction completeness
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

refinement calculus... dARL axioms DW, DI, DHC, AG, DG, DC, DR

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

33 extracted references · 33 canonical work pages

[1]

Structural Analysis of Multi-Mode DAE Systems

Albert Benveniste, Benoît Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin Otter, and Marc Pouzet. “Structural Analysis of Multi-Mode DAE Systems”. In:Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, HSCC 2017, Pittsburgh, PA, USA, April 18-20, 2017. Ed. by Goran Frehse and Sayan Mitra. ACM, 2017, pp. 253–263....

work page doi:10.1145/3049797.3049806 2017
[2]

The math- ematical foundations of physical systems modeling languages

Albert Benveniste, Benoît Caillaud, and Mathias Malandain. “The math- ematical foundations of physical systems modeling languages”. In:Annu. Rev. Control.50 (2020), pp. 72–118.doi:10.1016/J.ARCONTROL.2020. 08.001

work page doi:10.1016/j.arcontrol.2020 2020
[3]

Representation for the Radical of a Finitely Generated Differential Ideal

François Boulier, Daniel Lazard, François Ollivier, and Michel Petitot. “Representation for the Radical of a Finitely Generated Differential Ideal”. In:Proceedings of the 1995 International Symposium on Symbolic and Al- gebraic Computation, ISSAC ’95, Montreal, Canada, July 10-12, 1995. Ed. by A. H. M. Levelt. ACM, 1995, pp. 158–166.doi:10.1145/220346. 220367

work page doi:10.1145/220346 1995
[4]

Cox, John Little, and Donal O’Shea.Ideals, Varieties, and Algo- rithms: An Introduction to Computational Algebraic Geometry and Com- mutative Algebra

David A. Cox, John Little, and Donal O’Shea.Ideals, Varieties, and Algo- rithms: An Introduction to Computational Algebraic Geometry and Com- mutative Algebra. 5th ed. Undergraduate Texts in Mathematics. Springer, 2025.doi:https://doi.org/10.1007/978-3-031-91841-4

work page doi:10.1007/978-3-031-91841-4 2025
[5]

KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems

Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, and An- dré Platzer. “KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems”. en. In:Automated Deduction - CADE-25. Vol. 9195. LNCS. Cham: Springer International Publishing, 2015, pp. 527–538.isbn: 978-3-319-21400-9.doi:10.1007/978-3-319-21401-6_36

work page doi:10.1007/978-3-319-21401-6_36 2015
[6]

Differential-Algebraic Equation Index Transformations

C. W. Gear. “Differential-Algebraic Equation Index Transformations”. In: SIAM Journal on Scientific and Statistical Computing9.1 (1988), pp. 39– 47.doi:10.1137/0909004

work page doi:10.1137/0909004 1988
[7]

AReal-AnalyticApproachtoDifferential- Algebraic Dynamic Logic

JonathanHellwigandAndréPlatzer.“AReal-AnalyticApproachtoDifferential- Algebraic Dynamic Logic”. In:Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings. Ed. by Clark W. Barrett and Uwe Wald- mann. Vol. 15943. Lecture Notes in Computer Science. Springer, 2025, pp. 696–714.do...

work page doi:10.1007/978-3-031-99984-0 2025
[8]

NotesonTriangularSetsandTriangulation-Decomposition Algorithms II: Differential Systems

EvelyneHubert.“NotesonTriangularSetsandTriangulation-Decomposition Algorithms II: Differential Systems”. In:Symbolic and Numerical Scientific Computation, Second International Conference, SNSC 2001, Hagenberg, Austria, September 10-11, 2001, Revised Papers. Ed.byFranzWinklerand Ulrich Langer. Vol. 2630. Lecture Notes in Computer Science. Springer, 2001, p...

work page doi:10.1007/3-540-45084-x 2001
[9]

Ellis Robert Kolchin.Differential Algebra and Algebraic Groups. Vol. 54. Academic press, 1973

work page 1973
[10]

In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

Sarah M. Loos and André Platzer. “Differential Refinement Logic”. In:Pro- ceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. Ed. by Martin Grohe, Eric Koskinen, and Natarajan Shankar. ACM, 2016, pp. 505–514. doi:10.1145/2933575.2934555

work page doi:10.1145/2933575.2934555 2016
[11]

The Consistent Initialization of Differential- Algebraic Systems

Constantinos C. Pantelides. “The Consistent Initialization of Differential- Algebraic Systems”. In:SIAM Journal on Scientific and Statistical Com- puting9.2 (1988), pp. 213–231.doi:10.1137/0909014

work page doi:10.1137/0909014 1988
[12]

A Complete Uniform Substitution Calculus for Differential Dynamic Logic

André Platzer. “A Complete Uniform Substitution Calculus for Differential Dynamic Logic”. In:J. Autom. Reason.59.2 (2017), pp. 219–265.doi: 10.1007/S10817-016-9385-1

work page doi:10.1007/s10817-016-9385-1 2017
[13]

Journal of Auto- mated Reasoning62, 367–391 (2019).https://doi.org/10.1007/s10817- 018-9459-3

André Platzer. “Differential Dynamic Logic for Hybrid Systems”. In:J. Autom. Reason.41.2 (2008), pp. 143–189.doi:10.1007/S10817- 008- 9103-8

work page doi:10.1007/s10817- 2008
[14]

Differential-algebraicDynamicLogicforDifferential-algebraic Programs

AndréPlatzer.“Differential-algebraicDynamicLogicforDifferential-algebraic Programs”. In:J. Log. Comput.20.1 (2010), pp. 309–352.doi:10.1093/ logcom/exn070

work page 2010
[15]

Heidelberg: Springer, 2010.isbn: 978-3-642-14508-7

André Platzer.Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Heidelberg: Springer, 2010.isbn: 978-3-642-14508-7. doi:10.1007/978-3-642-14509-4

work page doi:10.1007/978-3-642-14509-4 2010
[16]

AndréPlatzer.Logical Foundations of Cyber-Physical Systems.Cham:Springer, 2018.isbn: 978-3-319-63587-3.doi:10.1007/978-3-319-63588-0

work page doi:10.1007/978-3-319-63588-0 2018
[17]

The Complete Proof Theory of Hybrid Systems

André Platzer. “The Complete Proof Theory of Hybrid Systems”. In:Pro- ceedings of the 27th Annual IEEE Symposium on Logic in Computer Sci- ence, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 2012, pp. 541–550.doi:10.1109/LICS.2012.64

work page doi:10.1109/lics.2012.64 2012
[18]

Axiomatization of Compact Initial Value Problems: Open Properties

André Platzer and Long Qian. “Axiomatization of Compact Initial Value Problems: Open Properties”. In:J. ACM(Aug. 2025). Just Accepted.issn: 0004-5411.doi:10.1145/3763228

work page doi:10.1145/3763228 2025
[19]

Differential Equation Invariance Ax- iomatization

André Platzer and Yong Kiam Tan. “Differential Equation Invariance Ax- iomatization”. In:J. ACM67.1 (2020), 6:1–6:66.doi:10.1145/3380825

work page doi:10.1145/3380825 2020
[20]

Uniform Substitution for Differen- tial Refinement Logic

Enguerrand Prebet and André Platzer. “Uniform Substitution for Differen- tial Refinement Logic”. In:IJCAR. Ed. by Christoph Benzmüller, Marijn J. Heule, and Renate A. Schmidt. Vol. 14740. LNCS. Springer, 2024, pp. 196– 215.doi:10.1007/978-3-031-63501-4_11. 18 Jonathan Hellwig , Long Qian, and André Platzer

work page doi:10.1007/978-3-031-63501-4_11 2024
[21]

Johansson, Structural and electronic relationships between the lanthanide and actinide elements, Hy- perfine Interactions 128 (2000) 41–66

John Pryce. “A Simple Structural Analysis Method for DAEs”. In:BIT Numerical Mathematics41 (Mar. 2001), pp. 364–394.doi:10.1023/A: 1021998624799

work page doi:10.1023/a: 2001
[22]

Joseph Fels Ritt.Differential algebra. Vol. 33. American Mathematical Soc., 1950

work page 1950
[23]

Wolfgang Walter.Ordinary Differential Equations. en. Vol. 182. Graduate Texts in Mathematics. Springer New York, 1998.isbn: 978-1-4612-6834-5. doi:10.1007/978-1-4612-0601-9. A Deferred Proofs A.1 Conservative Extension. This section completes the proof of Proposition 1, thatdARLis a conservative extension of the reachability-based semantics ofdL[13]. Proo...

work page doi:10.1007/978-1-4612-0601-9 1998
[24]

Ifv∈x: Then, we haveφ(t)(v) =ψ(t)(v)for allt∈[0, T φ], by the refinement assumption

work page
[25]

Consequently,φ(t)(v) =ψ(t)(v)for allt∈[0, T φ]

Ifv∈(BV(α)∪BV(β)) ∁: By the Bound Effect Lemma, both traces preserve the initial state, i.e.,φ(t)(v) =ω(v)andψ(t)(v) =ω(v)for all t∈[0, T φ]. Consequently,φ(t)(v) =ψ(t)(v)for allt∈[0, T φ]. In both cases,φandψcoincidence. Thus, by a pointwise application of Lemma 1 we concludeφ(Tφ)∈JPK, completing the proof. ≤t x Letω∈Jα≤ xβKandω∈Jβ≤ xγK.Toshowω∈Jα≤ xγK,f...

work page
[26]

IfT φ = 0: The result is immediate asφ(0) =ωandω∈Je⪯0Kby assumption

work page
[27]

By the Mean Value Theorem (Theorem 3), there exists aξ∈(0, T φ)such that: φ(Tφ)JeK=T φ d dt φ(ξ)JeK+φ(0)JeK

IfT φ >0: Sinceφisx-regular andeis differential-free, the valuation of the termealong the trace is continuous on[0, Tφ]and differentiable on(0, T φ)(Lemma 5). By the Mean Value Theorem (Theorem 3), there exists aξ∈(0, T φ)such that: φ(Tφ)JeK=T φ d dt φ(ξ)JeK+φ(0)JeK. Again, sinceeis differential free, by applying the Differential Lemma 5, we obtain: φ(Tφ)...

work page
[28]

IfT φ = 0: The goal is immediate asφ(0) =ωandω∈J(e) ′ = 0Kby assumption

work page
[29]

By the semantics of DAPs, we haveφ([0, T φ])⊆Je= 0K

IfT φ >0: Sinceφisx-regular, the valuation of the termealong the trace is differentiable on(0, Tφ)(Lemma 5). By the semantics of DAPs, we haveφ([0, T φ])⊆Je= 0K. It follows that for everyt∈[0, T φ], the valuation satisfiesφ(t)JeK= 0. Differentiating both sides of this equa- tion yields d dt φ(t)JeK= 0. By the Differential Lemma 5, this implies φ(t)J(e)′K=...

work page
[30]

Define the candidate stateν≡(ω) ( z,z ′)(u,v)

By Theorem 4, the system (3) possesses a unique solutionv∈Rn. Define the candidate stateν≡(ω) ( z,z ′)(u,v). It suffices to show that for everyx-regular traceφ∈J{x:F}K(ν), there exists a (x,z)-regular trace ψ∈J{x,z:F∧Az ′ =Bz+c}K(ν)such thatψ∼ x φ. By the box modality assumption and Lemma 6, we haveφ(t)JdetAK= detφ(t)JAK̸= 0for allt∈[0, T φ]. Consequently...

work page
[31]

Also, byz,z ′ /∈A,b,c, applying coincidence of terms yields ψ(t)Jz′K= (ψ(t)JAK) −1ψ(t)JBKψ(t)JzK+ (ψ(t)JAK) −1ψ(t)JcK

Differential constraint: By construction, equation (4) implies for allt∈ [0, Tψ]: ψ(t)Jz′K= (φ(t)JAK) −1φ(t)JBKψ(t)JzK+ (φ(t)JAK) −1φ(t)JcK. Also, byz,z ′ /∈A,b,c, applying coincidence of terms yields ψ(t)Jz′K= (ψ(t)JAK) −1ψ(t)JBKψ(t)JzK+ (ψ(t)JAK) −1ψ(t)JcK. Finally, rearranging this equation and folding the semantics of terms, we obtainψ([0, T ψ])⊆JAz ′...

work page
[32]

Therefore, by the chain rule (Lemma 5) the semantic valuationt7→φ(t)JgK is of classC 1([0, Tφ],R m)

Since theC 2 trajectoryρis locally unique,φandρmust be identical on a neighborhood(t−ε, t+ε), ensuring thatt7→φ(t)(x)isC 2 on[0, T φ]. Therefore, by the chain rule (Lemma 5) the semantic valuationt7→φ(t)JgK is of classC 1([0, Tφ],R m). We define the candidate traceψ∈ Tby ψ(t)(z)≡φ(t)JgK, ψ(t)(z′)≡ d dt φ(t)JgK, ψ(t)(v)≡φ(t)(v)forv̸∈z∪z ′. We show thatψsat...

work page
[33]

Applying the Coincidence Lemma pointwise, by the syntactic side con- ditionz,z ′ ̸∈FV(F)andφ([0, T φ])⊆JFK, we haveψ([0, T ψ])⊆JFK

Differential constraint: By construction, we haveψ([0, Tψ])⊆Jz=gK. Applying the Coincidence Lemma pointwise, by the syntactic side con- ditionz,z ′ ̸∈FV(F)andφ([0, T φ])⊆JFK, we haveψ([0, T ψ])⊆JFK. Thus,ψ([0, T ψ])⊆JFK∩Jz=gK=JF∧z=gK. 26 Jonathan Hellwig , Long Qian, and André Platzer 2.(x,z)-regularity: The regularity oft7→ψ(t)(x)follows directly from th...

work page