1 subgoal
H1 : t_eind > t_begin
H2 : nu in  (t_eind - rinkeltijd, t_eind]
H3 : timer_gezet t_begin t_eind
H4 : timer_gezet t_begin t_eind /\ ~ (exists x : Tijd, timer_gezet t_eind x) ->
     (forall a : Tijd, a in  (t_eind, t_eind + rinkeltijd] /\ rinkelt a) /\
     rinkelt t_eind ->
     exists t_berekend_eind : Tijd,
       t_berekend_eind in  [t_eind - rinkeltijd, t_eind] /\
       (exists t_berekend_begin : Tijd,
          t_berekend_begin in  [t_eind - max_looptijd, t_eind) /\
          timer_gezet t_berekend_begin t_berekend_eind)
______________________________________(1/1)
rinkelt nu





---------------------------------------------------------------------
(*all_e (forall t, t in (t_eind, t_eind+rinkeltijd] /\ rinkelt t) nu. *) (* Mag niet *)
(*all_e (forall t, ((t > t_eind) /\ (t <= (t_eind+rinkeltijd)) /\ (rinkelt t))) nu. *) (* Mag niet *)
all_e (forall t, rinkelt t) nu. (* Mag wel *)