ArchiveEntry "16: Dual Filibuster Game". /** * Dual Filibuster Game Formula */ ProgramVariables. R x. End. Problem. x=0 -> <{{{x:=0; ++ x:=1;}^@}*}^@> x=0 End. Tactic "16: Dual Filibuster Game: Proof 1". implyR(1) ; duald(1) ; box(1) ; loop({`x=0`}, 1) ; <( closeId, dualb(1) ; diamond(1) ; choiced(1) ; orR(1) ; assignd(1) ; hideR(2) ; QE, closeId ) End. End. ArchiveEntry "16: Push-around Cart". /** * 16: Push-around Cart */ ProgramVariables. /* program variables may change their value over time */ R x. /* position of cart */ R v. /* velocity of cart */ R a. /* Angel's acceleration pushing/pulling the cart */ R d. /* Demon's acceleration pushing/pulling the cart */ End. Problem. x>=0 & v>=0 -> [{ {d:=1;++d:=-1;}^@ {a:=1;++a:=-1;} {x'=v,v'=a+d} }*@invariant(x>=0&v>=0) ] x>=0 End. Tactic "16: Push-around Cart: Proof 1". implyR(1) ; loop({`x>=0&v>=0`}, 1) ; <( prop, composeb(1) ; dualb(1) ; diamond(1) ; composeb(1.1) ; choiced(1) ; orR(1) ; assignd(1) ; assignd(2) ; choiceb(1) ; andR(1) ; <( assignb(1) ; solve(1) ; hideR(2) ; QE, assignb(1) ; solve(1) ; hideR(2) ; QE ), prop ) End. End. ArchiveEntry "16: Goalie in Robot Soccer". /** * Goalie in robot soccer */ ProgramVariables. R x. /* x-coordinate of ball */ R y. /* y-coordinate of ball */ R v. /* ball's velocity in x-direction */ R w. /* ball's velocity in y-direction */ R g. /* y-coordinate of goalie lateral in goal */ R u. /* velocity of goalie */ End. Problem. (x/v)^2*(u-w)^2<=1 & x<0&v>0&y=g -> <{w:=w; ++ w:=-w;}^@; {{u:=u; ++ u:=-u;}; {x'=v,y'=w,g'=u}}> x^2+(y-g)^2<=1 End. Tactic "16: Goalie in Robot Soccer: Proof 1". implyR(1) ; composed(1) ; composed(1.1) ; dualDirectd(1) ; choiceb(1) ; andR(1) ; <( assignb(1) ; choiced(1) ; orR(1) ; hideR(2) ; assignd(1) ; solve(1) ; QE, assignb(1) ; choiced(1) ; orR(1) ; hideR(1) ; assignd(1) ; solve(1) ; QE ) End. End.