MODULE RightAngle;

IMPORT R2, R3;

PRED V1(a, b, c) IS 
      (E y ~ -1 :: c = (1, y) REL (a, b)) 
END;

PRED V2(a, b, c) IS 
      (E y ~ 1 :: a = (0, y) REL (b, c)) 
END;

PRED V3(a, b, c) IS 
      R2.Dot(R2.Minus(a, b), 
               R2.Minus(c, b)) = 0 
END;

PRED V4(a, b, c) IS 
      (E v1 ~ R3.FromR2(R2.Minus(c, b))
       , v2 ~ R3.FromR2(R2.Minus(a, b))
       , y ~ R3.Z(R3.Cross(v1, v2)) :: 
        c = (1, y) REL (a, b)) 
END;

FUNC p = RelInv(a, b, c) IS 
      c = p REL (a, b) 
END;

PRED V5(a, b, c) IS 
      (E y ~ CDR(RelInv(a, b, c)) :: 
        c = (1, y) REL (a, b)) 
END;