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 24993
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 24973 . 2  wff  ( ph  until  ps )
43wcirc 24972 . . . 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  24995  imunt  24997  evpexun  24998  albineal  24999  untind  25018  untim1d  25020  untim2d  25021
  Copyright terms: Public domain W3C validator