ArchiveEntry "16: Dual Filibuster Game" Description "Example 16.4". ProgramVariables Real x; End. Problem x=0 -> <{{{x:=0; ++ x:=1;}^@}*}^@> x=0 End. Tactic "16: Dual Filibuster Game: Proof: positional" implyR(1) ; duald(1) ; box(1) ; loop("x=0", 1) ; <( "Init": id, "Step": dualb(1) ; diamond(1) ; choiced(1) ; orR(1) ; assignd(1) ; hideR(2) ; QE, "Post": id ) End. Tactic "16: Dual Filibuster Game: Proof: named" implyR('R=="x=0-><{{{x:=0;++x:=1;}^@}*}^@>x=0"); duald('R=="<{{{x:=0;++x:=1;}^@}*}^@>x=0"); box('R=="!<{{x:=0;++x:=1;}^@}*>(!x=0)"); loop("x=0", 'R=="[{{x:=0;++x:=1;}^@}*]x=0"); <( "Init": id, "Step": dualb('R=="[{x:=0;++x:=1;}^@]x=0"); diamond('R=="![x:=0;++x:=1;](!x=0)"); choiced('R=="x=0"); orR('R=="x=0|x=0"); assignd('R=="x=0"); hideR('R=="x=0"); QE, "Post": id ) End. End. ArchiveEntry "16: Push-around Cart" Description "Proposition 16.1: Push-around carts are safe". ProgramVariables /* program variables may change their value over time */ Real x; /* position of cart */ Real v; /* velocity of cart */ Real a; /* Angel's acceleration pushing/pulling the cart */ Real 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: positional" implyR(1) ; loop("x>=0&v>=0", 1) ; <( "Init": prop, "Step": 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 ), "Post": prop ) End. Tactic "16: Push-around Cart: Proof: named" implyR('R=="x>=0&v>=0->[{{d:=1;++d:=(-1);}^@{a:=1;++a:=(-1);}{x'=v,v'=a+d}}*]x>=0"); loop("x>=0&v>=0", 'R=="[{{d:=1;++d:=(-1);}^@{a:=1;++a:=(-1);}{x'=v,v'=a+d}}*]x>=0"); <( "Init": propClose, "Step": composeb('R=="[{d:=1;++d:=(-1);}^@{a:=1;++a:=(-1);}{x'=v,v'=a+d}](x>=0&v>=0)"); dualb('R=="[{d:=1;++d:=(-1);}^@][{a:=1;++a:=(-1);}{x'=v,v'=a+d}](x>=0&v>=0)"); diamond('R=="![d:=1;++d:=(-1);](![{a:=1;++a:=(-1);}{x'=v,v'=a+d}](x>=0&v>=0))"); composeb('R=="#[{a:=1;++a:=(-1);}{x'=v,v'=a+d}](x>=0&v>=0)#"); choiced('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+d}](x>=0&v>=0)"); orR('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+d}](x>=0&v>=0)|[a:=1;++a:=(-1);][{x'=v,v'=a+d}](x>=0&v>=0)"); assignd('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+d}](x>=0&v>=0)"); assignd('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+d}](x>=0&v>=0)"); choiceb('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+1}](x>=0&v>=0)"); andR('R=="[a:=1;][{x'=v,v'=a+1}](x>=0&v>=0)&[a:=(-1);][{x'=v,v'=a+1}](x>=0&v>=0)"); <( "[a:=1;][{x'=v,v'=a+1}](x>=0&v>=0)": assignb('R=="[a:=1;][{x'=v,v'=a+1}](x>=0&v>=0)"); solve('R=="[{x'=v,v'=1+1}](x>=0&v>=0)"); hideR('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+(-1)}](x>=0&v>=0)"); QE, "[a:=(-1);][{x'=v,v'=a+1}](x>=0&v>=0)": assignb('R=="[a:=(-1);][{x'=v,v'=a+1}](x>=0&v>=0)"); solve('R=="[{x'=v,v'=(-1)+1}](x>=0&v>=0)"); hideR('R=="[a:=1;++a:=(-1);][{x'=v,v'=a+(-1)}](x>=0&v>=0)"); QE ), "Post": propClose ) End. Illustration "https://lfcps.org/info/fig-push-around-cart.png". End. ArchiveEntry "16: Goalie in Robot Soccer" Description "Proof for Example 14.6". ProgramVariables Real x, y; /* x/y-coordinate of ball */ Real v, w; /* ball's velocity in x/y-direction */ Real g; /* y-coordinate of goalie lateral in goal */ Real 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: positional" implyR(1) ; composed(1) ; composed(1.1) ; duald(1) ; box(1) ; choiceb(1) ; andR(1) ; <( assignb(1) ; choiced(1) ; orR(1) ; hideR(2) ; assignd(1) ; solve(1) ; QE("Mathematica"), assignb(1) ; choiced(1) ; orR(1) ; hideR(1) ; assignd(1) ; solve(1) ; QE("Mathematica") ) End. Tactic "16: Goalie in Robot Soccer: Proof: named" implyR('R=="(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"); composed('R=="<{w:=w;++w:=-w;}^@{u:=u;++u:=-u;}{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); composed('R=="<{w:=w;++w:=-w;}^@>#<{u:=u;++u:=-u;}{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1#"); duald('R=="<{w:=w;++w:=-w;}^@><{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); box('R=="!(!<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1)"); choiceb('R=="[w:=w;++w:=-w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); andR('R=="[w:=w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1&[w:=-w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); <( "[w:=w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1": assignb('R=="[w:=w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); choiced('R=="<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); orR('R=="<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1|<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); hideR('R=="<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); assignd('R=="<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); solve('R=="<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); QE, "[w:=-w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1": assignb('R=="[w:=-w;]<{x'=v,y'=w,g'=u}>x^2+(y-g)^2<=1"); choiced('R=="<{x'=v,y'=-w,g'=u}>x^2+(y-g)^2<=1"); orR('R=="<{x'=v,y'=-w,g'=u}>x^2+(y-g)^2<=1|<{x'=v,y'=-w,g'=u}>x^2+(y-g)^2<=1"); hideR('R=="<{x'=v,y'=-w,g'=u}>x^2+(y-g)^2<=1"); assignd('R=="<{x'=v,y'=-w,g'=u}>x^2+(y-g)^2<=1"); solve('R=="<{x'=v,y'=-w,g'=-u}>x^2+(y-g)^2<=1"); QE ) End. Illustration "https://lfcps.org/info/fig-goalie.png". End.