CONTEXT
  Car_C1
EXTENDS
  ControlledSystemCtx
CONSTANTS
  stabilizing
  accelerating
  braking
  nearing_stop
  stopped
  A
  b
  v0
  SP
  f2_speed
  f1_deceleration
  f1_stable
  f1_acceleration
  f_deceleration
  f_stable
  f_acceleration
  eod
AXIOMS
  axm1: partition(STATES,{stabilizing},{accelerating},{braking},{nearing_stop},{stopped})
  axm2: A : RReal
  axm3: Rzero |-> A : lt
  axm4: b : RReal
  axm5: Rzero |-> b : lt
  axm51: b /= Rzero
  axm6: v0 : RReal
  axm7: Rzero |-> v0 : lt
  axm8: SP : RReal
  axm9: Rzero |-> SP : lt
  axm154: f2_speed : (RRealPlus*S) --> RReal
  axm155: f2_speed = (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S | v_)
  axm156: f1_deceleration : ((RRealPlus*RRealPlus) --> (RRealPlus*S --> RReal))
  axm11: 
    ! t_init,v_init . t_init : RRealPlus & v_init : RRealPlus => (
      f1_deceleration(t_init |-> v_init) =
        (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S & (t_ |-> plus(divide(v_init |-> b) |-> t_init) : lt) | uminus(b)) \/
        (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S & (t_ |-> plus(divide(v_init |-> b) |-> t_init) :geq) | Rzero)
    )
  axm10: f_deceleration : ((RRealPlus*RRealPlus) --> (RRealPlus*S --> S))
  axm102: ! t_init, v_init . t_init : RRealPlus & v_init : RRealPlus => (f1_deceleration(t_init|->v_init) : RRealPlus*S --> RReal)
  axm101: 
    ! t_init, v_init . t_init : RRealPlus & v_init : RRealPlus =>
      f_deceleration(t_init |-> v_init) = bind(f1_deceleration(t_init |-> v_init),f2_speed)
  axm12: f1_stable : (RRealPlus*S --> RReal)
  axm13: f1_stable = (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S | Rzero)
  axm130: f_stable : (RRealPlus*S --> S)
  axm131: f_stable = bind(f1_stable,f2_speed)
  axm132: f_stable : C0(RRealPlus*S,S)
  axm14: f1_acceleration : (RRealPlus*S --> RReal)
  axm15: f1_acceleration = (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S | A)
  axm150: f_acceleration : (RRealPlus*S --> S)
  axm151: f_acceleration = bind(f1_acceleration,f2_speed)
  axm152: f_acceleration : C0(RRealPlus*S,S)
  axm16: ! t0 . t0 : RRealPlus => lipschitzContinuous(S,S,partial2(f_stable,t0))
  axm17: ! t0 . t0 : RRealPlus => lipschitzContinuous(S,S,partial2(f_acceleration,t0))
  axm22: eod : (RRealPlus*RRealPlus --> RRealPlus)
  axm21: eod = (% ti|->vi . ti : RRealPlus & vi : RRealPlus | plus(divide(vi |-> b) |-> ti))
  axm20: 
    ! eta1,eta2,t_init,v_init,x_init .
        t_init : RRealPlus & v_init : RRealPlus & x_init : RReal &
      eta1 : Closed2Closed(t_init,eod(t_init|->v_init)) --> S &
      solutionOf(
        Closed2Closed(t_init,eod(t_init|->v_init)), eta1,
        ode(
          (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S & (t_ |-> eod(t_init|->v_init) : lt) | (uminus(b) |-> v_)),
          (v_init |-> x_init),
          t_init
        )
      ) &
      eta2 : Closed2Infinity(eod(t_init|->v_init)) --> S &
      solutionOf(
        Closed2Infinity(eod(t_init|->v_init)), eta2,
        ode(
          (% t_ |-> (v_ |-> x_) . t_ : RRealPlus & (v_ |-> x_) : S & (t_ |-> eod(t_init|->v_init) :geq) | (Rzero |-> v_)),
          eta1(eod(t_init|->v_init)),
          eod(t_init|->v_init)
        )
      ) =>
        solutionOf(
          Closed2Infinity(t_init), eta1 \/ eta2,
                ode(
              f_deceleration(t_init |-> v_init),
              (v_init |-> x_init),
              t_init
            )
            )
  axm153: 
    ! t_init,v_init,x_init .
      t_init : RRealPlus & v_init : RRealPlus & x_init : RReal =>
        Solvable(
          Closed2Infinity(t_init),
          ode(
            f_deceleration(t_init |-> v_init),
            (v_init |-> x_init),
            t_init
          )
        )
END