Presburger arithmetic

Index, feed.

formula: ∃ x . (((16|x) ∧ (3|x)) ∧ ((31 < x) ∧ (x < 33)))

expandjd: (((((16|1×((1 + 31) + 0)) ∧ (3|1×((1 + 31) + 0))) ∧ ((31 < (1 + 31) + 0) ∧ ((1 + 31) + 0 < 33))) ∧ (1|1 + 31)) ∨ F) ∨ ((((((16|1×((2 + 31) + 0)) ∧ (3|1×((2 + 31) + 0))) ∧ ((31 < (2 + 31) + 0) ∧ ((2 + 31) + 0 < 33))) ∧ (1|2 + 31)) ∨ F) ∨ ((((((16|1×((3 + 31) + 0)) ∧ (3|1×((3 + 31) + 0))) ∧ ((31 < (3 + 31) + 0) ∧ ((3 + 31) + 0 < 33))) ∧ (1|3 + 31)) ∨ F) ∨ ((((((16|1×((4 + 31) + 0)) ∧ (3|1×((4 + 31) + 0))) ∧ ((31 < (4 + 31) + 0) ∧ ((4 + 31) + 0 < 33))) ∧ (1|4 + 31)) ∨ F) ∨ ((((((16|1×((5 + 31) + 0)) ∧ (3|1×((5 + 31) + 0))) ∧ ((31 < (5 + 31) + 0) ∧ ((5 + 31) + 0 < 33))) ∧ (1|5 + 31)) ∨ F) ∨ ((((((16|1×((6 + 31) + 0)) ∧ (3|1×((6 + 31) + 0))) ∧ ((31 < (6 + 31) + 0) ∧ ((6 + 31) + 0 < 33))) ∧ (1|6 + 31)) ∨ F) ∨ ((((((16|1×((7 + 31) + 0)) ∧ (3|1×((7 + 31) + 0))) ∧ ((31 < (7 + 31) + 0) ∧ ((7 + 31) + 0 < 33))) ∧ (1|7 + 31)) ∨ F) ∨ ((((((16|1×((8 + 31) + 0)) ∧ (3|1×((8 + 31) + 0))) ∧ ((31 < (8 + 31) + 0) ∧ ((8 + 31) + 0 < 33))) ∧ (1|8 + 31)) ∨ F) ∨ ((((((16|1×((9 + 31) + 0)) ∧ (3|1×((9 + 31) + 0))) ∧ ((31 < (9 + 31) + 0) ∧ ((9 + 31) + 0 < 33))) ∧ (1|9 + 31)) ∨ F) ∨ ((((((16|1×((10 + 31) + 0)) ∧ (3|1×((10 + 31) + 0))) ∧ ((31 < (10 + 31) + 0) ∧ ((10 + 31) + 0 < 33))) ∧ (1|10 + 31)) ∨ F) ∨ ((((((16|1×((11 + 31) + 0)) ∧ (3|1×((11 + 31) + 0))) ∧ ((31 < (11 + 31) + 0) ∧ ((11 + 31) + 0 < 33))) ∧ (1|11 + 31)) ∨ F) ∨ ((((((16|1×((12 + 31) + 0)) ∧ (3|1×((12 + 31) + 0))) ∧ ((31 < (12 + 31) + 0) ∧ ((12 + 31) + 0 < 33))) ∧ (1|12 + 31)) ∨ F) ∨ ((((((16|1×((13 + 31) + 0)) ∧ (3|1×((13 + 31) + 0))) ∧ ((31 < (13 + 31) + 0) ∧ ((13 + 31) + 0 < 33))) ∧ (1|13 + 31)) ∨ F) ∨ ((((((16|1×((14 + 31) + 0)) ∧ (3|1×((14 + 31) + 0))) ∧ ((31 < (14 + 31) + 0) ∧ ((14 + 31) + 0 < 33))) ∧ (1|14 + 31)) ∨ F) ∨ ((((((16|1×((15 + 31) + 0)) ∧ (3|1×((15 + 31) + 0))) ∧ ((31 < (15 + 31) + 0) ∧ ((15 + 31) + 0 < 33))) ∧ (1|15 + 31)) ∨ F) ∨ ((((((16|1×((16 + 31) + 0)) ∧ (3|1×((16 + 31) + 0))) ∧ ((31 < (16 + 31) + 0) ∧ ((16 + 31) + 0 < 33))) ∧ (1|16 + 31)) ∨ F) ∨ ((((((16|1×((17 + 31) + 0)) ∧ (3|1×((17 + 31) + 0))) ∧ ((31 < (17 + 31) + 0) ∧ ((17 + 31) + 0 < 33))) ∧ (1|17 + 31)) ∨ F) ∨ ((((((16|1×((18 + 31) + 0)) ∧ (3|1×((18 + 31) + 0))) ∧ ((31 < (18 + 31) + 0) ∧ ((18 + 31) + 0 < 33))) ∧ (1|18 + 31)) ∨ F) ∨ ((((((16|1×((19 + 31) + 0)) ∧ (3|1×((19 + 31) + 0))) ∧ ((31 < (19 + 31) + 0) ∧ ((19 + 31) + 0 < 33))) ∧ (1|19 + 31)) ∨ F) ∨ ((((((16|1×((20 + 31) + 0)) ∧ (3|1×((20 + 31) + 0))) ∧ ((31 < (20 + 31) + 0) ∧ ((20 + 31) + 0 < 33))) ∧ (1|20 + 31)) ∨ F) ∨ ((((((16|1×((21 + 31) + 0)) ∧ (3|1×((21 + 31) + 0))) ∧ ((31 < (21 + 31) + 0) ∧ ((21 + 31) + 0 < 33))) ∧ (1|21 + 31)) ∨ F) ∨ ((((((16|1×((22 + 31) + 0)) ∧ (3|1×((22 + 31) + 0))) ∧ ((31 < (22 + 31) + 0) ∧ ((22 + 31) + 0 < 33))) ∧ (1|22 + 31)) ∨ F) ∨ ((((((16|1×((23 + 31) + 0)) ∧ (3|1×((23 + 31) + 0))) ∧ ((31 < (23 + 31) + 0) ∧ ((23 + 31) + 0 < 33))) ∧ (1|23 + 31)) ∨ F) ∨ ((((((16|1×((24 + 31) + 0)) ∧ (3|1×((24 + 31) + 0))) ∧ ((31 < (24 + 31) + 0) ∧ ((24 + 31) + 0 < 33))) ∧ (1|24 + 31)) ∨ F) ∨ ((((((16|1×((25 + 31) + 0)) ∧ (3|1×((25 + 31) + 0))) ∧ ((31 < (25 + 31) + 0) ∧ ((25 + 31) + 0 < 33))) ∧ (1|25 + 31)) ∨ F) ∨ ((((((16|1×((26 + 31) + 0)) ∧ (3|1×((26 + 31) + 0))) ∧ ((31 < (26 + 31) + 0) ∧ ((26 + 31) + 0 < 33))) ∧ (1|26 + 31)) ∨ F) ∨ ((((((16|1×((27 + 31) + 0)) ∧ (3|1×((27 + 31) + 0))) ∧ ((31 < (27 + 31) + 0) ∧ ((27 + 31) + 0 < 33))) ∧ (1|27 + 31)) ∨ F) ∨ ((((((16|1×((28 + 31) + 0)) ∧ (3|1×((28 + 31) + 0))) ∧ ((31 < (28 + 31) + 0) ∧ ((28 + 31) + 0 < 33))) ∧ (1|28 + 31)) ∨ F) ∨ ((((((16|1×((29 + 31) + 0)) ∧ (3|1×((29 + 31) + 0))) ∧ ((31 < (29 + 31) + 0) ∧ ((29 + 31) + 0 < 33))) ∧ (1|29 + 31)) ∨ F; (1|31 + 31)) ∨ F) ∨ ((((((16|1×((32 + 31) + 0)) ∧ (3|1×((32 + 31) + 0))) ∧ ((31 < (32 + 31) + 0) ∧ ((32 + 31) + 0 < 33))) ∧ (1|32 + 31)) ∨ F) ∨ ((((((16|1×((33 + 31) + 0)) ∧ (3|1×((33 + 31) + 0))) ∧ ((31 < (33 + 31) + 0) ∧ ((33 + 31) + 0 < 33))) ∧ (1|33 + 31)) ∨ F) ∨ ((((((16|1×((34 + 31) + 0)) ∧ (3|1×((34 + 31) + 0))) ∧ ((31 < (34 + 31) + 0) ∧ ((34 + 31) + 0 < 33))) ∧ (1|34 + 31)) ∨ F) ∨ ((((((16|1×((35 + 31) + 0)) ∧ (3|1×((35 + 31) + 0))) ∧ ((31 < (35 + 31) + 0) ∧ ((35 + 31) + 0 < 33))) ∧ (1|35 + 31)) ∨ F) ∨ ((((((16|1×((36 + 31) + 0)) ∧ (3|1×((36 + 31) + 0))) ∧ ((31 < (36 + 31) + 0) ∧ ((36 + 31) + 0 < 33))) ∧ (1|36 + 31)) ∨ F) ∨ ((((((16|1×((37 + 31) + 0)) ∧ (3|1×((37 + 31) + 0))) ∧ ((31 < (37 + 31) + 0) ∧ ((37 + 31) + 0 < 33))) ∧ (1|37 + 31)) ∨ F) ∨ ((((((16|1×((38 + 31) + 0)) ∧ (3|1×((38 + 31) + 0))) ∧ ((31 < (38 + 31) + 0) ∧ ((38 + 31) + 0 < 33))) ∧ (1|38 + 31)) ∨ F) ∨ ((((((16|1×((39 + 31) + 0)) ∧ (3|1×((39 + 31) + 0))) ∧ ((31 < (39 + 31) + 0) ∧ ((39 + 31) + 0 < 33))) ∧ (1|39 + 31)) ∨ F) ∨ ((((((16|1×((40 + 31) + 0)) ∧ (3|1×((40 + 31) + 0))) ∧ ((31 < (40 + 31) + 0) ∧ ((40 + 31) + 0 < 33))) ∧ (1|40 + 31)) ∨ F) ∨ ((((((16|1×((41 + 31) + 0)) ∧ (3|1×((41 + 31) + 0))) ∧ ((31 < (41 + 31) + 0) ∧ ((41 + 31) + 0 < 33))) ∧ (1|41 + 31)) ∨ F) ∨ ((((((16|1×((42 + 31) + 0)) ∧ (3|1×((42 + 31) + 0))) ∧ ((31 < (42 + 31) + 0) ∧ ((42 + 31) + 0 < 33))) ∧ (1|42 + 31)) ∨ F) ∨ ((((((16|1×((43 + 31) + 0)) ∧ (3|1×((43 + 31) + 0))) ∧ ((31 < (43 + 31) + 0) ∧ ((43 + 31) + 0 < 33))) ∧ (1|43 + 31)) ∨ F) ∨ ((((((16|1×((44 + 31) + 0)) ∧ (3|1×((44 + 31) + 0))) ∧ ((31 < (44 + 31) + 0) ∧ ((44 + 31) + 0 < 33))) ∧ (1|44 + 31)) ∨ F) ∨ ((((((16|1×((45 + 31) + 0)) ∧ (3|1×((45 + 31) + 0))) ∧ ((31 < (45 + 31) + 0) ∧ ((45 + 31) + 0 < 33))) ∧ (1|45 + 31)) ∨ F) ∨ ((((((16|1×((46 + 31) + 0)) ∧ (3|1×((46 + 31) + 0))) ∧ ((31 < (46 + 31) + 0) ∧ ((46 + 31) + 0 < 33))) ∧ (1|46 + 31)) ∨ F) ∨ ((((((16|1×((47 + 31) + 0)) ∧ (3|1×((47 + 31) + 0))) ∧ ((31 < (47 + 31) + 0) ∧ ((47 + 31) + 0 < 33))) ∧ (1|47 + 31)) ∨ F) ∨ (((((16|1×((48 + 31) + 0)) ∧ (3|1×((48 + 31) + 0))) ∧ ((31 < (48 + 31) + 0) ∧ ((48 + 31) + 0 < 33))) ∧ (1|48 + 31)) ∨ F)))))))))))))))))))))))))))))))))))))))))))))))

interp: true → initial prop would be true

www.kurokatta.org

David Haguenauer <www@kurokatta.org>
$Id: presburger.malblog,v 1.3 2011/11/13 00:23:35 homer Exp $