<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* ------------------------------------------------------------------------- *)
(* Three bugs are crawling on the coordinate plane. They move                *)
(* one at a time, and each bug will only crawl in a direction                *)
(* parallel to the line joining the other two.                               *)
(*                                                                           *)
(*  (a) If the bugs start out at (0,0), (3,0), and (0,3), is it              *)
(*      possible that after some time the first bug will end up              *)
(*      back where it started, while the other two bugs switch               *)
(*      places?                                                              *)
(*                                                                           *)
(*  (b) Can the bugs end up at (1,2), (2,5), and (-2,3)?                     *)
(* ------------------------------------------------------------------------- *)


prioritize_real();;

let move = new_definition
 `move ((ax,ay),(bx,by),(cx,cy)) ((ax',ay'),(bx',by'),(cx',cy')) <=>
        (?a. ax' = ax + a * (cx - bx) /\ ay' = ay + a * (cy - by) /\
             bx' = bx /\ by' = by /\ cx' = cx /\ cy' = cy) \/
        (?b. bx' = bx + b * (ax - cx) /\ by' = by + b * (ay - cy) /\
             ax' = ax /\ ay' = ay /\ cx' = cx /\ cy' = cy) \/
        (?c. ax' = ax /\ ay' = ay /\ bx' = bx /\ by' = by /\
             cx' = cx + c * (bx - ax) /\ cy' = cy + c * (by - ay))`;;

let reachable_RULES,reachable_INDUCT,reachable_CASES =
 new_inductive_definition
  `(!p. reachable p p) /\
   (!p q r. move p q /\ reachable q r ==> reachable p r)`;;


let oriented_area = new_definition
 `oriented_area ((ax,ay),(bx,by),(cx,cy)) =
      ((bx - ax) * (cy - ay) - (cx - ax) * (by - ay)) / &2`;;

let MOVE_INVARIANT = prove
 (`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
  REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area] THEN CONV_TAC REAL_RING);;

let REACHABLE_INVARIANT = prove
 (`!p p'. reachable p p' ==> oriented_area p = oriented_area p'`,
  MATCH_MP_TAC reachable_INDUCT THEN MESON_TAC[MOVE_INVARIANT]);;


let IMPOSSIBILITY_B = prove
 (`~(reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(&2,&5),(-- &2,&3)) \/
     reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(-- &2,&3),(&2,&5)) \/
     reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(&1,&2),(-- &2,&3)) \/
     reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(-- &2,&3),(&1,&2)) \/
     reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&1,&2),(&2,&5)) \/
     reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&2,&5),(&1,&2)))`,
  STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP REACHABLE_INVARIANT) THEN
  REWRITE_TAC[oriented_area] THEN REAL_ARITH_TAC);;