the_w:World, e:E. 
first(e) 
pred(e) 
Ethe_w:World, e:E. <loc(e),time(e)> ~ ethe_w:World, t:
, i:Id. first(<i,t>) pred(<i,t>) E| Theorem | Name |
| the_w:World, e:E. first(e) pred(e) E | [w-pred_wf] |
| cites the following: | |
| the_w:World, e:E. <loc(e),time(e)> ~ e | [w-loc-time] |
| the_w:World, t:, i:Id. first(<i,t>) pred(<i,t>) E | [w-pred-aux] |