(* This figure demonstrates a theorem credited 
   to Napoleon Bonaparte. Start with any 
   triangle abc (the red triangle in the 
   figure). Construct three equalateral 
   triangles off the edges of abc (the black 
   triangles in the figure). Then Napoleon 
   showed that the triangle formed from the 
   centers of these three triangles (the blue 
   triangle in the figure) is itself 
   equalateral. *)

PROC DrawSides(a, b, c) IS 
  SAVE PS IN 
    PS.MoveTo(a); 
    PS.LineTo(b); 
    PS.LineTo(c); 
    PS.SetColor(Color.Black); 
    PS.Stroke() 
  END 
END;

UI PointTool(DrawSides);

PRED IsEqTri(a, b, c) IS 
  (a, c) CONG (c, b) AND (c, b) CONG (b, a) 
END;

UI PointTool(IsEqTri);

FUNC h = EqTriHint(a, b, c) IS 
  (E y = Rel.InvY(c, a, b) :: 
    h = (0.5, -y) REL (a, b)) 
END;

PROC Cmd0() IS 
  VAR a = (-90.13, 9.86), b = (-3.03, -116), c = (53.02, 8.343) IN 
    PS.SetWidth(2); 
    PS.SetColor(Color.Red); 
    Triangle.Draw(a, b, c); 
    PS.SetJointStyle(PS.BevelJoints); 
    PS.Stroke(); 
    IF 
      VAR 
        d ~ EqTriHint(a, b, c), e ~ EqTriHint(b, c, a), 
        f ~ EqTriHint(c, a, b) 
      IN 
        IsEqTri(a, d, b) AND IsEqTri(b, e, c) AND IsEqTri(c, f, a) -> 
          DrawSides(a, d, b); 
          DrawSides(b, e, c); 
          DrawSides(c, f, a); 
          IF 
            VAR g ~ (201.9, 399.5), h ~ (263.3, 249.8), i ~ (102.9, 271.5) IN 
              g = Triangle.OutCenter(a, f, c) AND 
              h = Triangle.OutCenter(c, b, e) AND 
              i = Triangle.OutCenter(a, b, d) -> 
                Triangle.Draw(i, h, g); 
                PS.SetColor(Color.Blue); 
                PS.Stroke() 
            END | SKIP 
          FI 
      END | SKIP 
    FI 
  END 
END;