Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-ltl5 Unicode version

Axiom ax-ltl5 25096
Description:  ph holds until  ps iff  ps holds in the current step or  ph holds in the current step and in the next step  ph holds until  ps. (Contributed by FL, 27-Feb-2011.)
Assertion
Ref Expression
ax-ltl5  |-  ( (
ph  until  ps )  <->  ( ps  \/  ( ph  /\  () ( ph  until  ps ) ) ) )

Detailed syntax breakdown of Axiom ax-ltl5
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wunt 25076 . 2  wff  ( ph  until  ps )
43wcirc 25075 . . . 4  wff  () (
ph  until  ps )
51, 4wa 358 . . 3  wff  ( ph  /\  () ( ph  until  ps )
)
62, 5wo 357 . 2  wff  ( ps  \/  ( ph  /\  () ( ph  until  ps )
) )
73, 6wb 176 1  wff  ( (
ph  until  ps )  <->  ( ps  \/  ( ph  /\  () ( ph  until  ps ) ) ) )
Colors of variables: wff set class
This axiom is referenced by:  nopsthph  25098  imunt  25100  evpexun  25101  albineal  25102  untind  25121  untim1d  25123  untim2d  25124
  Copyright terms: Public domain W3C validator