Some axioms for the ﬁrst order case are shown in Table 8.
Let V denote a state variable.
We denote by f [e ∕ V ] that in formula f expression e is substituted for variable V .
ForallSub 
⊢ ∀V f ⊃ f [e ∕ V ], 
where the expression e has the same data 

and temporal type as the variable V and 

is free for V in f. 

ForallImplies 
⊢ ∀V (f_{1} ⊃ f_{2}) ⊃ (f_{1} ⊃ ∀V f_{2}), 
where V doesn’t occur freely in f_{1}. 

SubstAxiom  ⊢ (V _{1} = V _{2}) ⊃ f ≡ f [V _{2} ∕ V _{1}]. 
ExistsChopRight 
⊢ ∃V (f_{1} ; f_{2}) ⊃ (∃V f_{1}) ; f_{2}, 
where V doesn’t occur freely in f_{2}. 

ExistsChopLeft 
⊢ ∃V (f_{1} ; f_{2}) ⊃ f_{1} ; (∃V f_{2}), 
where V doesn’t occur freely in f_{1}. 

ForallGen 
⊢ f ⇒ ⊢ ∀V f, 
for any variable V . 
