/* Exported from KeYmaera X v4.8.0 */ Theorem "Tank_normalConsumption" Functions. R SMALLSTEPSIZE. R DrugConsumptionUPPERLIMIT. R DrugConsumptionLOWERLIMIT. R TankFillUPPERLIMIT. R TankFillLOWERLIMIT. R TankChangeUPPERLIMIT. R TankChangeLOWERLIMIT. R TankCAPACITY. End. ProgramVariables. R simTime. R DrugConsumption. R TankFill. R TankChange. R TankContentOutput. R Switch. R Switch1. R TankContent. R smallStep. /* Added Observer */ R TankContentStart. End. Problem. (simTime = 0.0) & (SMALLSTEPSIZE = 0.01) & (TankContent = TankCAPACITY) & (smallStep = 0.0) & /* Added Assumptions */ (TankCAPACITY > 0) & (TankChangeUPPERLIMIT = 0) & (TankChangeLOWERLIMIT = 0) & (TankFillUPPERLIMIT = 0) & (TankChangeLOWERLIMIT = 0) & (DrugConsumptionUPPERLIMIT > 0) & (DrugConsumptionLOWERLIMIT = 0) & (TankContentStart = TankContent) ->( [ { /* Added Observer */ TankContentStart := TankContent; smallStep:=0.0; TankChange:= *; ?(( TankChange <= TankChangeUPPERLIMIT) & ( TankChange >= TankChangeLOWERLIMIT)); TankFill:= *; ?(( TankFill <= TankFillUPPERLIMIT) & ( TankFill >= TankFillLOWERLIMIT)); DrugConsumption:= *; ?(( DrugConsumption <= DrugConsumptionUPPERLIMIT) & ( DrugConsumption >= DrugConsumptionLOWERLIMIT)); TankContentOutput:=TankContent; { ?( TankChange != 0.0); TankContent:=TankCAPACITY; ++ ?( TankChange = 0.0); } { ?(( TankChange != 0.0) & ( DrugConsumption > 0.0) & ( TankFill > 0.0)); { simTime' = 1.0, TankContent' = 0.0, smallStep' = 1.0 &(( TankChange != 0.0) & ( DrugConsumption > 0.0) & ( TankFill > 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange != 0.0) & ( DrugConsumption > 0.0) & ( TankFill <= 0.0)); { simTime' = 1.0, TankContent' = 0.0, smallStep' = 1.0 &(( TankChange != 0.0) & ( DrugConsumption > 0.0) & ( TankFill <= 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange != 0.0) & ( DrugConsumption <= 0.0) & ( TankFill > 0.0)); { simTime' = 1.0, TankContent' = 0.0, smallStep' = 1.0 &(( TankChange != 0.0) & ( DrugConsumption <= 0.0) & ( TankFill > 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange != 0.0) & ( DrugConsumption <= 0.0) & ( TankFill <= 0.0)); { simTime' = 1.0, TankContent' = 0.0, smallStep' = 1.0 &(( TankChange != 0.0) & ( DrugConsumption <= 0.0) & ( TankFill <= 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange = 0.0) & ( DrugConsumption > 0.0) & ( TankFill > 0.0)); { simTime' = 1.0, TankContent' = (TankFill+((-1.0)*DrugConsumption)), smallStep' = 1.0 &(( TankChange = 0.0) & ( DrugConsumption > 0.0) & ( TankFill > 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange = 0.0) & ( DrugConsumption > 0.0) & ( TankFill <= 0.0)); { simTime' = 1.0, TankContent' = ((-1.0)*DrugConsumption), smallStep' = 1.0 &(( TankChange = 0.0) & ( DrugConsumption > 0.0) & ( TankFill <= 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange = 0.0) & ( DrugConsumption <= 0.0) & ( TankFill > 0.0)); { simTime' = 1.0, TankContent' = (TankFill+0.0), smallStep' = 1.0 &(( TankChange = 0.0) & ( DrugConsumption <= 0.0) & ( TankFill > 0.0)) | ( smallStep <= SMALLSTEPSIZE) } ++ ?(( TankChange = 0.0) & ( DrugConsumption <= 0.0) & ( TankFill <= 0.0)); { simTime' = 1.0, TankContent' = 0.0, smallStep' = 1.0 &(( TankChange = 0.0) & ( DrugConsumption <= 0.0) & ( TankFill <= 0.0)) | ( smallStep <= SMALLSTEPSIZE) } } }* ] (TankContent <= TankContentStart)) End. Tactic "Tank_normalConsumption: Proof" master End. End.