(30 . 15)(30 . 15)
1441 -------------------------------------------
1442
1443 -- 1 iff X == Y (branch-free); else 0
1444 function FZ_EqP(X : in FZ; Y: in FZ) return WBool;
1445 pragma Precondition(X'Length = Y'Length);
1446 function FZ_EqP(X : in FZ; Y: in FZ) return WBool
1447 with Pre => X'Length = Y'Length;
1448
1449 -- 1 iff X < Y (branch-free); else 0
1450 function FZ_LessThanP(X : in FZ; Y : in FZ) return WBool;
1451 pragma Precondition(X'Length = Y'Length);
1452 function FZ_LessThanP(X : in FZ; Y : in FZ) return WBool
1453 with Pre => X'Length = Y'Length;
1454
1455 -- 1 iff X > Y (branch-free); else 0
1456 function FZ_GreaterThanP(X : in FZ; Y : in FZ) return WBool;
1457 pragma Precondition(X'Length = Y'Length);
1458 function FZ_GreaterThanP(X : in FZ; Y : in FZ) return WBool
1459 with Pre => X'Length = Y'Length;
1460
1461 end FZ_Cmp;