0 JBC
↳1 JBCToGraph (⇒, 100 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 30 ms)
↳7 IDP
↳8 IDPNonInfProof (⇒, 70 ms)
↳9 AND
↳10 IDP
↳11 IDependencyGraphProof (⇔, 0 ms)
↳12 TRUE
↳13 IDP
↳14 IDependencyGraphProof (⇔, 0 ms)
↳15 TRUE
↳16 JBCTerminationSCC
↳17 SCCToIDPv1Proof (⇒, 30 ms)
↳18 IDP
↳19 IDPNonInfProof (⇒, 70 ms)
↳20 AND
↳21 IDP
↳22 IDependencyGraphProof (⇔, 0 ms)
↳23 TRUE
↳24 IDP
↳25 IDependencyGraphProof (⇔, 0 ms)
↳26 TRUE
↳27 JBCTerminationSCC
↳28 SCCToIDPv1Proof (⇒, 20 ms)
↳29 IDP
↳30 IDPNonInfProof (⇒, 70 ms)
↳31 AND
↳32 IDP
↳33 IDependencyGraphProof (⇔, 0 ms)
↳34 TRUE
↳35 IDP
↳36 IDependencyGraphProof (⇔, 0 ms)
↳37 TRUE
↳38 JBCTerminationSCC
↳39 SCCToIDPv1Proof (⇒, 20 ms)
↳40 IDP
↳41 IDPNonInfProof (⇒, 70 ms)
↳42 AND
↳43 IDP
↳44 IDependencyGraphProof (⇔, 0 ms)
↳45 TRUE
↳46 IDP
↳47 IDependencyGraphProof (⇔, 0 ms)
↳48 TRUE
↳49 JBCTerminationSCC
↳50 SCCToIDPv1Proof (⇒, 30 ms)
↳51 IDP
↳52 IDPNonInfProof (⇒, 70 ms)
↳53 AND
↳54 IDP
↳55 IDependencyGraphProof (⇔, 0 ms)
↳56 TRUE
↳57 IDP
↳58 IDependencyGraphProof (⇔, 0 ms)
↳59 TRUE
↳60 JBCTerminationSCC
↳61 SCCToIDPv1Proof (⇒, 20 ms)
↳62 IDP
↳63 IDPNonInfProof (⇒, 60 ms)
↳64 AND
↳65 IDP
↳66 IDependencyGraphProof (⇔, 0 ms)
↳67 TRUE
↳68 IDP
↳69 IDependencyGraphProof (⇔, 0 ms)
↳70 TRUE
↳71 JBCTerminationSCC
↳72 SCCToIDPv1Proof (⇒, 30 ms)
↳73 IDP
↳74 IDPNonInfProof (⇒, 60 ms)
↳75 AND
↳76 IDP
↳77 IDependencyGraphProof (⇔, 0 ms)
↳78 TRUE
↳79 IDP
↳80 IDependencyGraphProof (⇔, 0 ms)
↳81 TRUE
↳82 JBCTerminationSCC
↳83 SCCToIDPv1Proof (⇒, 20 ms)
↳84 IDP
↳85 IDPNonInfProof (⇒, 60 ms)
↳86 AND
↳87 IDP
↳88 IDependencyGraphProof (⇔, 0 ms)
↳89 TRUE
↳90 IDP
↳91 IDependencyGraphProof (⇔, 0 ms)
↳92 TRUE
↳93 JBCTerminationSCC
↳94 SCCToIDPv1Proof (⇒, 20 ms)
↳95 IDP
↳96 IDPNonInfProof (⇒, 70 ms)
↳97 AND
↳98 IDP
↳99 IDependencyGraphProof (⇔, 0 ms)
↳100 TRUE
↳101 IDP
↳102 IDependencyGraphProof (⇔, 0 ms)
↳103 TRUE
↳104 JBCTerminationSCC
↳105 SCCToIDPv1Proof (⇒, 20 ms)
↳106 IDP
↳107 IDPNonInfProof (⇒, 70 ms)
↳108 AND
↳109 IDP
↳110 IDependencyGraphProof (⇔, 0 ms)
↳111 TRUE
↳112 IDP
↳113 IDependencyGraphProof (⇔, 0 ms)
↳114 TRUE
↳115 JBCTerminationSCC
↳116 SCCToIDPv1Proof (⇒, 30 ms)
↳117 IDP
↳118 IDPNonInfProof (⇒, 60 ms)
↳119 AND
↳120 IDP
↳121 IDependencyGraphProof (⇔, 0 ms)
↳122 TRUE
↳123 IDP
↳124 IDependencyGraphProof (⇔, 0 ms)
↳125 TRUE
↳126 JBCTerminationSCC
↳127 SCCToIDPv1Proof (⇒, 20 ms)
↳128 IDP
↳129 IDPNonInfProof (⇒, 70 ms)
↳130 AND
↳131 IDP
↳132 IDependencyGraphProof (⇔, 0 ms)
↳133 TRUE
↳134 IDP
↳135 IDependencyGraphProof (⇔, 0 ms)
↳136 TRUE
↳137 JBCTerminationSCC
↳138 SCCToIDPv1Proof (⇒, 730 ms)
↳139 IDP
↳140 IDPNonInfProof (⇒, 590 ms)
↳141 AND
↳142 IDP
↳143 IDependencyGraphProof (⇔, 0 ms)
↳144 IDP
↳145 IDPNonInfProof (⇒, 540 ms)
↳146 AND
↳147 IDP
↳148 IDependencyGraphProof (⇔, 0 ms)
↳149 TRUE
↳150 IDP
↳151 IDependencyGraphProof (⇔, 0 ms)
↳152 TRUE
↳153 IDP
↳154 IDependencyGraphProof (⇔, 0 ms)
↳155 IDP
↳156 IDPNonInfProof (⇒, 560 ms)
↳157 AND
↳158 IDP
↳159 IDependencyGraphProof (⇔, 0 ms)
↳160 TRUE
↳161 IDP
↳162 IDependencyGraphProof (⇔, 0 ms)
↳163 TRUE
public class Test9 {
public static void main(String[] args) {
long l = args.length;
while (l > 0) {
for (int i = (int) l ; i < 100; i++)
test(i);
l--;
}
}
private static void test(int i) {
int j, k, l, m;
for (j = i; j > 0; j--);
for (k = i; k > 0; k--);
for (l = i; l > 0; l--);
for (m = i; m > 0; m--);
for (j = i; j > 0; j--);
for (k = i; k > 0; k--);
for (l = i; l > 0; l--);
for (m = i; m > 0; m--);
for (j = i; j > 0; j--);
for (k = i; k > 0; k--);
for (l = i; l > 0; l--);
for (m = i; m > 0; m--);
}
}
Generated 6 rules for P and 0 rules for R.
P rules:
549_0_test_LE(EOS(STATIC_549), i161, i161) → 553_0_test_LE(EOS(STATIC_553), i161, i161)
553_0_test_LE(EOS(STATIC_553), i161, i161) → 557_0_test_Inc(EOS(STATIC_557), i161) | >(i161, 0)
557_0_test_Inc(EOS(STATIC_557), i161) → 563_0_test_JMP(EOS(STATIC_563), +(i161, -1)) | >(i161, 0)
563_0_test_JMP(EOS(STATIC_563), i163) → 574_0_test_Load(EOS(STATIC_574), i163)
574_0_test_Load(EOS(STATIC_574), i163) → 546_0_test_Load(EOS(STATIC_546), i163)
546_0_test_Load(EOS(STATIC_546), i158) → 549_0_test_LE(EOS(STATIC_549), i158, i158)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
549_0_test_LE(EOS(STATIC_549), x0, x0) → 549_0_test_LE(EOS(STATIC_549), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
549_0_test_LE(x1, x2, x3) → 549_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_549_0_test_LE(x1, x2, x3, x4) → Cond_549_0_test_LE(x1, x3, x4)
Filtered duplicate args:
549_0_test_LE(x1, x2) → 549_0_test_LE(x2)
Cond_549_0_test_LE(x1, x2, x3) → Cond_549_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
549_0_test_LE(x0) → 549_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
549_0_TEST_LE(x0) → COND_549_0_TEST_LE(>(x0, 0), x0)
COND_549_0_TEST_LE(TRUE, x0) → 549_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 549_0_TEST_LE(x0[0])≥NonInfC∧549_0_TEST_LE(x0[0])≥COND_549_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_549_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 549_0_TEST_LE(x0[0])≥NonInfC∧549_0_TEST_LE(x0[0])≥COND_549_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_549_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_549_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_549_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_549_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_549_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_549_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_549_0_TEST_LE(TRUE, x0[1])≥549_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(549_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(549_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(549_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(549_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(549_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(549_0_TEST_LE(x1)) = [2]x1
POL(COND_549_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_549_0_TEST_LE(TRUE, x0[1]) → 549_0_TEST_LE(+(x0[1], -1))
549_0_TEST_LE(x0[0]) → COND_549_0_TEST_LE(>(x0[0], 0), x0[0])
549_0_TEST_LE(x0[0]) → COND_549_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
515_0_test_LE(EOS(STATIC_515), i150, i150) → 518_0_test_LE(EOS(STATIC_518), i150, i150)
518_0_test_LE(EOS(STATIC_518), i150, i150) → 522_0_test_Inc(EOS(STATIC_522), i150) | >(i150, 0)
522_0_test_Inc(EOS(STATIC_522), i150) → 526_0_test_JMP(EOS(STATIC_526), +(i150, -1)) | >(i150, 0)
526_0_test_JMP(EOS(STATIC_526), i153) → 533_0_test_Load(EOS(STATIC_533), i153)
533_0_test_Load(EOS(STATIC_533), i153) → 512_0_test_Load(EOS(STATIC_512), i153)
512_0_test_Load(EOS(STATIC_512), i144) → 515_0_test_LE(EOS(STATIC_515), i144, i144)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
515_0_test_LE(EOS(STATIC_515), x0, x0) → 515_0_test_LE(EOS(STATIC_515), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
515_0_test_LE(x1, x2, x3) → 515_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_515_0_test_LE(x1, x2, x3, x4) → Cond_515_0_test_LE(x1, x3, x4)
Filtered duplicate args:
515_0_test_LE(x1, x2) → 515_0_test_LE(x2)
Cond_515_0_test_LE(x1, x2, x3) → Cond_515_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
515_0_test_LE(x0) → 515_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
515_0_TEST_LE(x0) → COND_515_0_TEST_LE(>(x0, 0), x0)
COND_515_0_TEST_LE(TRUE, x0) → 515_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 515_0_TEST_LE(x0[0])≥NonInfC∧515_0_TEST_LE(x0[0])≥COND_515_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_515_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 515_0_TEST_LE(x0[0])≥NonInfC∧515_0_TEST_LE(x0[0])≥COND_515_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_515_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_515_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_515_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_515_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_515_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_515_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_515_0_TEST_LE(TRUE, x0[1])≥515_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(515_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(515_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(515_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(515_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(515_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(515_0_TEST_LE(x1)) = [2]x1
POL(COND_515_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_515_0_TEST_LE(TRUE, x0[1]) → 515_0_TEST_LE(+(x0[1], -1))
515_0_TEST_LE(x0[0]) → COND_515_0_TEST_LE(>(x0[0], 0), x0[0])
515_0_TEST_LE(x0[0]) → COND_515_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
479_0_test_LE(EOS(STATIC_479), i137, i137) → 484_0_test_LE(EOS(STATIC_484), i137, i137)
484_0_test_LE(EOS(STATIC_484), i137, i137) → 488_0_test_Inc(EOS(STATIC_488), i137) | >(i137, 0)
488_0_test_Inc(EOS(STATIC_488), i137) → 493_0_test_JMP(EOS(STATIC_493), +(i137, -1)) | >(i137, 0)
493_0_test_JMP(EOS(STATIC_493), i140) → 498_0_test_Load(EOS(STATIC_498), i140)
498_0_test_Load(EOS(STATIC_498), i140) → 477_0_test_Load(EOS(STATIC_477), i140)
477_0_test_Load(EOS(STATIC_477), i132) → 479_0_test_LE(EOS(STATIC_479), i132, i132)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
479_0_test_LE(EOS(STATIC_479), x0, x0) → 479_0_test_LE(EOS(STATIC_479), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
479_0_test_LE(x1, x2, x3) → 479_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_479_0_test_LE(x1, x2, x3, x4) → Cond_479_0_test_LE(x1, x3, x4)
Filtered duplicate args:
479_0_test_LE(x1, x2) → 479_0_test_LE(x2)
Cond_479_0_test_LE(x1, x2, x3) → Cond_479_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
479_0_test_LE(x0) → 479_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
479_0_TEST_LE(x0) → COND_479_0_TEST_LE(>(x0, 0), x0)
COND_479_0_TEST_LE(TRUE, x0) → 479_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 479_0_TEST_LE(x0[0])≥NonInfC∧479_0_TEST_LE(x0[0])≥COND_479_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_479_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 479_0_TEST_LE(x0[0])≥NonInfC∧479_0_TEST_LE(x0[0])≥COND_479_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_479_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_479_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_479_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_479_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_479_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_479_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_479_0_TEST_LE(TRUE, x0[1])≥479_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(479_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(479_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(479_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(479_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(479_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(479_0_TEST_LE(x1)) = [2]x1
POL(COND_479_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_479_0_TEST_LE(TRUE, x0[1]) → 479_0_TEST_LE(+(x0[1], -1))
479_0_TEST_LE(x0[0]) → COND_479_0_TEST_LE(>(x0[0], 0), x0[0])
479_0_TEST_LE(x0[0]) → COND_479_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
446_0_test_LE(EOS(STATIC_446), i126, i126) → 449_0_test_LE(EOS(STATIC_449), i126, i126)
449_0_test_LE(EOS(STATIC_449), i126, i126) → 453_0_test_Inc(EOS(STATIC_453), i126) | >(i126, 0)
453_0_test_Inc(EOS(STATIC_453), i126) → 457_0_test_JMP(EOS(STATIC_457), +(i126, -1)) | >(i126, 0)
457_0_test_JMP(EOS(STATIC_457), i128) → 463_0_test_Load(EOS(STATIC_463), i128)
463_0_test_Load(EOS(STATIC_463), i128) → 443_0_test_Load(EOS(STATIC_443), i128)
443_0_test_Load(EOS(STATIC_443), i122) → 446_0_test_LE(EOS(STATIC_446), i122, i122)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
446_0_test_LE(EOS(STATIC_446), x0, x0) → 446_0_test_LE(EOS(STATIC_446), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
446_0_test_LE(x1, x2, x3) → 446_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_446_0_test_LE(x1, x2, x3, x4) → Cond_446_0_test_LE(x1, x3, x4)
Filtered duplicate args:
446_0_test_LE(x1, x2) → 446_0_test_LE(x2)
Cond_446_0_test_LE(x1, x2, x3) → Cond_446_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
446_0_test_LE(x0) → 446_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
446_0_TEST_LE(x0) → COND_446_0_TEST_LE(>(x0, 0), x0)
COND_446_0_TEST_LE(TRUE, x0) → 446_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 446_0_TEST_LE(x0[0])≥NonInfC∧446_0_TEST_LE(x0[0])≥COND_446_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_446_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 446_0_TEST_LE(x0[0])≥NonInfC∧446_0_TEST_LE(x0[0])≥COND_446_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_446_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_446_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_446_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_446_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_446_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_446_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_446_0_TEST_LE(TRUE, x0[1])≥446_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(446_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(446_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(446_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(446_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(446_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(446_0_TEST_LE(x1)) = [2]x1
POL(COND_446_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_446_0_TEST_LE(TRUE, x0[1]) → 446_0_TEST_LE(+(x0[1], -1))
446_0_TEST_LE(x0[0]) → COND_446_0_TEST_LE(>(x0[0], 0), x0[0])
446_0_TEST_LE(x0[0]) → COND_446_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
410_0_test_LE(EOS(STATIC_410), i112, i112) → 414_0_test_LE(EOS(STATIC_414), i112, i112)
414_0_test_LE(EOS(STATIC_414), i112, i112) → 418_0_test_Inc(EOS(STATIC_418), i112) | >(i112, 0)
418_0_test_Inc(EOS(STATIC_418), i112) → 421_0_test_JMP(EOS(STATIC_421), +(i112, -1)) | >(i112, 0)
421_0_test_JMP(EOS(STATIC_421), i115) → 428_0_test_Load(EOS(STATIC_428), i115)
428_0_test_Load(EOS(STATIC_428), i115) → 407_0_test_Load(EOS(STATIC_407), i115)
407_0_test_Load(EOS(STATIC_407), i109) → 410_0_test_LE(EOS(STATIC_410), i109, i109)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
410_0_test_LE(EOS(STATIC_410), x0, x0) → 410_0_test_LE(EOS(STATIC_410), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
410_0_test_LE(x1, x2, x3) → 410_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_410_0_test_LE(x1, x2, x3, x4) → Cond_410_0_test_LE(x1, x3, x4)
Filtered duplicate args:
410_0_test_LE(x1, x2) → 410_0_test_LE(x2)
Cond_410_0_test_LE(x1, x2, x3) → Cond_410_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
410_0_test_LE(x0) → 410_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
410_0_TEST_LE(x0) → COND_410_0_TEST_LE(>(x0, 0), x0)
COND_410_0_TEST_LE(TRUE, x0) → 410_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 410_0_TEST_LE(x0[0])≥NonInfC∧410_0_TEST_LE(x0[0])≥COND_410_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_410_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 410_0_TEST_LE(x0[0])≥NonInfC∧410_0_TEST_LE(x0[0])≥COND_410_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_410_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_410_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_410_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_410_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_410_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_410_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_410_0_TEST_LE(TRUE, x0[1])≥410_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(410_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(410_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(410_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(410_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(410_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(410_0_TEST_LE(x1)) = [2]x1
POL(COND_410_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_410_0_TEST_LE(TRUE, x0[1]) → 410_0_TEST_LE(+(x0[1], -1))
410_0_TEST_LE(x0[0]) → COND_410_0_TEST_LE(>(x0[0], 0), x0[0])
410_0_TEST_LE(x0[0]) → COND_410_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
376_0_test_LE(EOS(STATIC_376), i102, i102) → 380_0_test_LE(EOS(STATIC_380), i102, i102)
380_0_test_LE(EOS(STATIC_380), i102, i102) → 384_0_test_Inc(EOS(STATIC_384), i102) | >(i102, 0)
384_0_test_Inc(EOS(STATIC_384), i102) → 388_0_test_JMP(EOS(STATIC_388), +(i102, -1)) | >(i102, 0)
388_0_test_JMP(EOS(STATIC_388), i106) → 393_0_test_Load(EOS(STATIC_393), i106)
393_0_test_Load(EOS(STATIC_393), i106) → 373_0_test_Load(EOS(STATIC_373), i106)
373_0_test_Load(EOS(STATIC_373), i98) → 376_0_test_LE(EOS(STATIC_376), i98, i98)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
376_0_test_LE(EOS(STATIC_376), x0, x0) → 376_0_test_LE(EOS(STATIC_376), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
376_0_test_LE(x1, x2, x3) → 376_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_376_0_test_LE(x1, x2, x3, x4) → Cond_376_0_test_LE(x1, x3, x4)
Filtered duplicate args:
376_0_test_LE(x1, x2) → 376_0_test_LE(x2)
Cond_376_0_test_LE(x1, x2, x3) → Cond_376_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
376_0_test_LE(x0) → 376_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
376_0_TEST_LE(x0) → COND_376_0_TEST_LE(>(x0, 0), x0)
COND_376_0_TEST_LE(TRUE, x0) → 376_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 376_0_TEST_LE(x0[0])≥NonInfC∧376_0_TEST_LE(x0[0])≥COND_376_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_376_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 376_0_TEST_LE(x0[0])≥NonInfC∧376_0_TEST_LE(x0[0])≥COND_376_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_376_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_376_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_376_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_376_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_376_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_376_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_376_0_TEST_LE(TRUE, x0[1])≥376_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(376_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(376_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(376_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(376_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(376_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(376_0_TEST_LE(x1)) = [2]x1
POL(COND_376_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_376_0_TEST_LE(TRUE, x0[1]) → 376_0_TEST_LE(+(x0[1], -1))
376_0_TEST_LE(x0[0]) → COND_376_0_TEST_LE(>(x0[0], 0), x0[0])
376_0_TEST_LE(x0[0]) → COND_376_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
341_0_test_LE(EOS(STATIC_341), i91, i91) → 345_0_test_LE(EOS(STATIC_345), i91, i91)
345_0_test_LE(EOS(STATIC_345), i91, i91) → 349_0_test_Inc(EOS(STATIC_349), i91) | >(i91, 0)
349_0_test_Inc(EOS(STATIC_349), i91) → 353_0_test_JMP(EOS(STATIC_353), +(i91, -1)) | >(i91, 0)
353_0_test_JMP(EOS(STATIC_353), i94) → 358_0_test_Load(EOS(STATIC_358), i94)
358_0_test_Load(EOS(STATIC_358), i94) → 338_0_test_Load(EOS(STATIC_338), i94)
338_0_test_Load(EOS(STATIC_338), i86) → 341_0_test_LE(EOS(STATIC_341), i86, i86)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
341_0_test_LE(EOS(STATIC_341), x0, x0) → 341_0_test_LE(EOS(STATIC_341), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
341_0_test_LE(x1, x2, x3) → 341_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_341_0_test_LE(x1, x2, x3, x4) → Cond_341_0_test_LE(x1, x3, x4)
Filtered duplicate args:
341_0_test_LE(x1, x2) → 341_0_test_LE(x2)
Cond_341_0_test_LE(x1, x2, x3) → Cond_341_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
341_0_test_LE(x0) → 341_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
341_0_TEST_LE(x0) → COND_341_0_TEST_LE(>(x0, 0), x0)
COND_341_0_TEST_LE(TRUE, x0) → 341_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 341_0_TEST_LE(x0[0])≥NonInfC∧341_0_TEST_LE(x0[0])≥COND_341_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_341_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 341_0_TEST_LE(x0[0])≥NonInfC∧341_0_TEST_LE(x0[0])≥COND_341_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_341_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_341_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_341_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_341_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_341_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_341_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_341_0_TEST_LE(TRUE, x0[1])≥341_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(341_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(341_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(341_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(341_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(341_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(341_0_TEST_LE(x1)) = [2]x1
POL(COND_341_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_341_0_TEST_LE(TRUE, x0[1]) → 341_0_TEST_LE(+(x0[1], -1))
341_0_TEST_LE(x0[0]) → COND_341_0_TEST_LE(>(x0[0], 0), x0[0])
341_0_TEST_LE(x0[0]) → COND_341_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
306_0_test_LE(EOS(STATIC_306), i78, i78) → 310_0_test_LE(EOS(STATIC_310), i78, i78)
310_0_test_LE(EOS(STATIC_310), i78, i78) → 314_0_test_Inc(EOS(STATIC_314), i78) | >(i78, 0)
314_0_test_Inc(EOS(STATIC_314), i78) → 318_0_test_JMP(EOS(STATIC_318), +(i78, -1)) | >(i78, 0)
318_0_test_JMP(EOS(STATIC_318), i80) → 323_0_test_Load(EOS(STATIC_323), i80)
323_0_test_Load(EOS(STATIC_323), i80) → 303_0_test_Load(EOS(STATIC_303), i80)
303_0_test_Load(EOS(STATIC_303), i74) → 306_0_test_LE(EOS(STATIC_306), i74, i74)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
306_0_test_LE(EOS(STATIC_306), x0, x0) → 306_0_test_LE(EOS(STATIC_306), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
306_0_test_LE(x1, x2, x3) → 306_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_306_0_test_LE(x1, x2, x3, x4) → Cond_306_0_test_LE(x1, x3, x4)
Filtered duplicate args:
306_0_test_LE(x1, x2) → 306_0_test_LE(x2)
Cond_306_0_test_LE(x1, x2, x3) → Cond_306_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
306_0_test_LE(x0) → 306_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
306_0_TEST_LE(x0) → COND_306_0_TEST_LE(>(x0, 0), x0)
COND_306_0_TEST_LE(TRUE, x0) → 306_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 306_0_TEST_LE(x0[0])≥NonInfC∧306_0_TEST_LE(x0[0])≥COND_306_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_306_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 306_0_TEST_LE(x0[0])≥NonInfC∧306_0_TEST_LE(x0[0])≥COND_306_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_306_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_306_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_306_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_306_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_306_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_306_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_306_0_TEST_LE(TRUE, x0[1])≥306_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(306_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(306_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(306_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(306_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(306_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(306_0_TEST_LE(x1)) = [2]x1
POL(COND_306_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_306_0_TEST_LE(TRUE, x0[1]) → 306_0_TEST_LE(+(x0[1], -1))
306_0_TEST_LE(x0[0]) → COND_306_0_TEST_LE(>(x0[0], 0), x0[0])
306_0_TEST_LE(x0[0]) → COND_306_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
270_0_test_LE(EOS(STATIC_270), i68, i68) → 274_0_test_LE(EOS(STATIC_274), i68, i68)
274_0_test_LE(EOS(STATIC_274), i68, i68) → 278_0_test_Inc(EOS(STATIC_278), i68) | >(i68, 0)
278_0_test_Inc(EOS(STATIC_278), i68) → 282_0_test_JMP(EOS(STATIC_282), +(i68, -1)) | >(i68, 0)
282_0_test_JMP(EOS(STATIC_282), i69) → 288_0_test_Load(EOS(STATIC_288), i69)
288_0_test_Load(EOS(STATIC_288), i69) → 267_0_test_Load(EOS(STATIC_267), i69)
267_0_test_Load(EOS(STATIC_267), i62) → 270_0_test_LE(EOS(STATIC_270), i62, i62)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
270_0_test_LE(EOS(STATIC_270), x0, x0) → 270_0_test_LE(EOS(STATIC_270), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
270_0_test_LE(x1, x2, x3) → 270_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_270_0_test_LE(x1, x2, x3, x4) → Cond_270_0_test_LE(x1, x3, x4)
Filtered duplicate args:
270_0_test_LE(x1, x2) → 270_0_test_LE(x2)
Cond_270_0_test_LE(x1, x2, x3) → Cond_270_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
270_0_test_LE(x0) → 270_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
270_0_TEST_LE(x0) → COND_270_0_TEST_LE(>(x0, 0), x0)
COND_270_0_TEST_LE(TRUE, x0) → 270_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 270_0_TEST_LE(x0[0])≥NonInfC∧270_0_TEST_LE(x0[0])≥COND_270_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_270_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 270_0_TEST_LE(x0[0])≥NonInfC∧270_0_TEST_LE(x0[0])≥COND_270_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_270_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_270_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_270_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_270_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_270_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_270_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_270_0_TEST_LE(TRUE, x0[1])≥270_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(270_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(270_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(270_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(270_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(270_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(270_0_TEST_LE(x1)) = [2]x1
POL(COND_270_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_270_0_TEST_LE(TRUE, x0[1]) → 270_0_TEST_LE(+(x0[1], -1))
270_0_TEST_LE(x0[0]) → COND_270_0_TEST_LE(>(x0[0], 0), x0[0])
270_0_TEST_LE(x0[0]) → COND_270_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
235_0_test_LE(EOS(STATIC_235), i55, i55) → 238_0_test_LE(EOS(STATIC_238), i55, i55)
238_0_test_LE(EOS(STATIC_238), i55, i55) → 243_0_test_Inc(EOS(STATIC_243), i55) | >(i55, 0)
243_0_test_Inc(EOS(STATIC_243), i55) → 247_0_test_JMP(EOS(STATIC_247), +(i55, -1)) | >(i55, 0)
247_0_test_JMP(EOS(STATIC_247), i58) → 252_0_test_Load(EOS(STATIC_252), i58)
252_0_test_Load(EOS(STATIC_252), i58) → 232_0_test_Load(EOS(STATIC_232), i58)
232_0_test_Load(EOS(STATIC_232), i49) → 235_0_test_LE(EOS(STATIC_235), i49, i49)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
235_0_test_LE(EOS(STATIC_235), x0, x0) → 235_0_test_LE(EOS(STATIC_235), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
235_0_test_LE(x1, x2, x3) → 235_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_235_0_test_LE(x1, x2, x3, x4) → Cond_235_0_test_LE(x1, x3, x4)
Filtered duplicate args:
235_0_test_LE(x1, x2) → 235_0_test_LE(x2)
Cond_235_0_test_LE(x1, x2, x3) → Cond_235_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
235_0_test_LE(x0) → 235_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
235_0_TEST_LE(x0) → COND_235_0_TEST_LE(>(x0, 0), x0)
COND_235_0_TEST_LE(TRUE, x0) → 235_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 235_0_TEST_LE(x0[0])≥NonInfC∧235_0_TEST_LE(x0[0])≥COND_235_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_235_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 235_0_TEST_LE(x0[0])≥NonInfC∧235_0_TEST_LE(x0[0])≥COND_235_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_235_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_235_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_235_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_235_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_235_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_235_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_235_0_TEST_LE(TRUE, x0[1])≥235_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(235_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(235_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(235_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(235_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(235_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(235_0_TEST_LE(x1)) = [2]x1
POL(COND_235_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_235_0_TEST_LE(TRUE, x0[1]) → 235_0_TEST_LE(+(x0[1], -1))
235_0_TEST_LE(x0[0]) → COND_235_0_TEST_LE(>(x0[0], 0), x0[0])
235_0_TEST_LE(x0[0]) → COND_235_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
194_0_test_LE(EOS(STATIC_194), i44, i44) → 198_0_test_LE(EOS(STATIC_198), i44, i44)
198_0_test_LE(EOS(STATIC_198), i44, i44) → 202_0_test_Inc(EOS(STATIC_202), i44) | >(i44, 0)
202_0_test_Inc(EOS(STATIC_202), i44) → 207_0_test_JMP(EOS(STATIC_207), +(i44, -1)) | >(i44, 0)
207_0_test_JMP(EOS(STATIC_207), i45) → 215_0_test_Load(EOS(STATIC_215), i45)
215_0_test_Load(EOS(STATIC_215), i45) → 191_0_test_Load(EOS(STATIC_191), i45)
191_0_test_Load(EOS(STATIC_191), i38) → 194_0_test_LE(EOS(STATIC_194), i38, i38)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
194_0_test_LE(EOS(STATIC_194), x0, x0) → 194_0_test_LE(EOS(STATIC_194), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
194_0_test_LE(x1, x2, x3) → 194_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_194_0_test_LE(x1, x2, x3, x4) → Cond_194_0_test_LE(x1, x3, x4)
Filtered duplicate args:
194_0_test_LE(x1, x2) → 194_0_test_LE(x2)
Cond_194_0_test_LE(x1, x2, x3) → Cond_194_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
194_0_test_LE(x0) → 194_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
194_0_TEST_LE(x0) → COND_194_0_TEST_LE(>(x0, 0), x0)
COND_194_0_TEST_LE(TRUE, x0) → 194_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 194_0_TEST_LE(x0[0])≥NonInfC∧194_0_TEST_LE(x0[0])≥COND_194_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_194_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 194_0_TEST_LE(x0[0])≥NonInfC∧194_0_TEST_LE(x0[0])≥COND_194_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_194_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_194_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_194_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_194_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_194_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_194_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_194_0_TEST_LE(TRUE, x0[1])≥194_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(194_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(194_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(194_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(194_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(194_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(194_0_TEST_LE(x1)) = [2]x1
POL(COND_194_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_194_0_TEST_LE(TRUE, x0[1]) → 194_0_TEST_LE(+(x0[1], -1))
194_0_TEST_LE(x0[0]) → COND_194_0_TEST_LE(>(x0[0], 0), x0[0])
194_0_TEST_LE(x0[0]) → COND_194_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 6 rules for P and 0 rules for R.
P rules:
157_0_test_LE(EOS(STATIC_157), i31, i31) → 161_0_test_LE(EOS(STATIC_161), i31, i31)
161_0_test_LE(EOS(STATIC_161), i31, i31) → 165_0_test_Inc(EOS(STATIC_165), i31) | >(i31, 0)
165_0_test_Inc(EOS(STATIC_165), i31) → 169_0_test_JMP(EOS(STATIC_169), +(i31, -1)) | >(i31, 0)
169_0_test_JMP(EOS(STATIC_169), i33) → 175_0_test_Load(EOS(STATIC_175), i33)
175_0_test_Load(EOS(STATIC_175), i33) → 153_0_test_Load(EOS(STATIC_153), i33)
153_0_test_Load(EOS(STATIC_153), i24) → 157_0_test_LE(EOS(STATIC_157), i24, i24)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
157_0_test_LE(EOS(STATIC_157), x0, x0) → 157_0_test_LE(EOS(STATIC_157), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
157_0_test_LE(x1, x2, x3) → 157_0_test_LE(x2, x3)
EOS(x1) → EOS
Cond_157_0_test_LE(x1, x2, x3, x4) → Cond_157_0_test_LE(x1, x3, x4)
Filtered duplicate args:
157_0_test_LE(x1, x2) → 157_0_test_LE(x2)
Cond_157_0_test_LE(x1, x2, x3) → Cond_157_0_test_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
157_0_test_LE(x0) → 157_0_test_LE(+(x0, -1)) | >(x0, 0)
R rules:
Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.
P rules:
157_0_TEST_LE(x0) → COND_157_0_TEST_LE(>(x0, 0), x0)
COND_157_0_TEST_LE(TRUE, x0) → 157_0_TEST_LE(+(x0, -1))
R rules:
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 157_0_TEST_LE(x0[0])≥NonInfC∧157_0_TEST_LE(x0[0])≥COND_157_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_157_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 157_0_TEST_LE(x0[0])≥NonInfC∧157_0_TEST_LE(x0[0])≥COND_157_0_TEST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_157_0_TEST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_157_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_157_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_157_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_157_0_TEST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(7) (COND_157_0_TEST_LE(TRUE, x0[1])≥NonInfC∧COND_157_0_TEST_LE(TRUE, x0[1])≥157_0_TEST_LE(+(x0[1], -1))∧(UIncreasing(157_0_TEST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(157_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(157_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(157_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(157_0_TEST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(157_0_TEST_LE(x1)) = [2]x1
POL(COND_157_0_TEST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_157_0_TEST_LE(TRUE, x0[1]) → 157_0_TEST_LE(+(x0[1], -1))
157_0_TEST_LE(x0[0]) → COND_157_0_TEST_LE(>(x0[0], 0), x0[0])
157_0_TEST_LE(x0[0]) → COND_157_0_TEST_LE(>(x0[0], 0), x0[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
Generated 27 rules for P and 134 rules for R.
P rules:
70_0_main_ConstantStackPush(EOS(STATIC_70), i4, i4) → 74_0_main_Cmp(EOS(STATIC_74), i4, i4, 0)
74_0_main_Cmp(EOS(STATIC_74), i9, i9, matching1) → 79_0_main_Cmp(EOS(STATIC_79), i9, i9, 0) | =(matching1, 0)
79_0_main_Cmp(EOS(STATIC_79), i9, i9, matching1) → 82_0_main_LE(EOS(STATIC_82), i9, 1) | &&(>(i9, 0), =(matching1, 0))
82_0_main_LE(EOS(STATIC_82), i9, matching1) → 84_0_main_Load(EOS(STATIC_84), i9) | &&(>(1, 0), =(matching1, 1))
84_0_main_Load(EOS(STATIC_84), i9) → 86_0_main_TypeCast(EOS(STATIC_86), i9, i9)
86_0_main_TypeCast(EOS(STATIC_86), i9, i9) → 87_0_main_Store(EOS(STATIC_87), i9, i10) | =(i10, i9)
87_0_main_Store(EOS(STATIC_87), i9, i10) → 89_0_main_Load(EOS(STATIC_89), i9, i10)
89_0_main_Load(EOS(STATIC_89), i9, i10) → 91_0_main_ConstantStackPush(EOS(STATIC_91), i9, i10, i10)
91_0_main_ConstantStackPush(EOS(STATIC_91), i9, i10, i10) → 92_0_main_GE(EOS(STATIC_92), i9, i10, i10, 100)
92_0_main_GE(EOS(STATIC_92), i9, i14, i14, matching1) → 93_0_main_GE(EOS(STATIC_93), i9, i14, i14, 100) | =(matching1, 100)
92_0_main_GE(EOS(STATIC_92), i9, i15, i15, matching1) → 94_0_main_GE(EOS(STATIC_94), i9, i15, i15, 100) | =(matching1, 100)
93_0_main_GE(EOS(STATIC_93), i9, i14, i14, matching1) → 95_0_main_Load(EOS(STATIC_95), i9, i14) | &&(<(i14, 100), =(matching1, 100))
95_0_main_Load(EOS(STATIC_95), i9, i14) → 99_0_main_InvokeMethod(EOS(STATIC_99), i9, i14, i14)
99_0_main_InvokeMethod(EOS(STATIC_99), i9, i14, i14) → 103_1_main_InvokeMethod(103_0_test_Load(EOS(STATIC_103), i14), i9, i14, i14)
103_1_main_InvokeMethod(555_0_test_Return(EOS(STATIC_555)), i9, i167, i167) → 576_0_test_Return(EOS(STATIC_576), i9, i167, i167)
576_0_test_Return(EOS(STATIC_576), i9, i167, i167) → 577_0_main_Inc(EOS(STATIC_577), i9, i167)
577_0_main_Inc(EOS(STATIC_577), i9, i167) → 580_0_main_JMP(EOS(STATIC_580), i9, +(i167, 1)) | >(i167, 0)
580_0_main_JMP(EOS(STATIC_580), i9, i172) → 583_0_main_Load(EOS(STATIC_583), i9, i172)
583_0_main_Load(EOS(STATIC_583), i9, i172) → 89_0_main_Load(EOS(STATIC_89), i9, i172)
94_0_main_GE(EOS(STATIC_94), i9, i15, i15, matching1) → 97_0_main_Load(EOS(STATIC_97), i9) | &&(>=(i15, 100), =(matching1, 100))
97_0_main_Load(EOS(STATIC_97), i9) → 101_0_main_ConstantStackPush(EOS(STATIC_101), i9)
101_0_main_ConstantStackPush(EOS(STATIC_101), i9) → 106_0_main_IntArithmetic(EOS(STATIC_106), i9, 1)
106_0_main_IntArithmetic(EOS(STATIC_106), i9, matching1) → 116_0_main_Store(EOS(STATIC_116), -(i9, 1)) | &&(>(i9, 0), =(matching1, 1))
116_0_main_Store(EOS(STATIC_116), i18) → 120_0_main_JMP(EOS(STATIC_120), i18)
120_0_main_JMP(EOS(STATIC_120), i18) → 129_0_main_Load(EOS(STATIC_129), i18)
129_0_main_Load(EOS(STATIC_129), i18) → 68_0_main_Load(EOS(STATIC_68), i18)
68_0_main_Load(EOS(STATIC_68), i4) → 70_0_main_ConstantStackPush(EOS(STATIC_70), i4, i4)
R rules:
103_0_test_Load(EOS(STATIC_103), i14) → 114_0_test_Load(EOS(STATIC_114), i14)
114_0_test_Load(EOS(STATIC_114), i14) → 122_0_test_Load(EOS(STATIC_122), i14)
122_0_test_Load(EOS(STATIC_122), i14) → 132_0_test_Store(EOS(STATIC_132), i14, i14)
132_0_test_Store(EOS(STATIC_132), i14, i14) → 134_0_test_Load(EOS(STATIC_134), i14, i14)
134_0_test_Load(EOS(STATIC_134), i14, i14) → 153_0_test_Load(EOS(STATIC_153), i14, i14)
153_0_test_Load(EOS(STATIC_153), i14, i24) → 157_0_test_LE(EOS(STATIC_157), i14, i24, i24)
157_0_test_LE(EOS(STATIC_157), i14, matching1, matching2) → 160_0_test_LE(EOS(STATIC_160), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
157_0_test_LE(EOS(STATIC_157), i14, i31, i31) → 161_0_test_LE(EOS(STATIC_161), i14, i31, i31)
160_0_test_LE(EOS(STATIC_160), i14, matching1, matching2) → 163_0_test_Load(EOS(STATIC_163), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
161_0_test_LE(EOS(STATIC_161), i14, i31, i31) → 165_0_test_Inc(EOS(STATIC_165), i14, i31) | >(i31, 0)
163_0_test_Load(EOS(STATIC_163), i14) → 167_0_test_Store(EOS(STATIC_167), i14, i14)
165_0_test_Inc(EOS(STATIC_165), i14, i31) → 169_0_test_JMP(EOS(STATIC_169), i14, +(i31, -1)) | >(i31, 0)
167_0_test_Store(EOS(STATIC_167), i14, i14) → 171_0_test_Load(EOS(STATIC_171), i14, i14)
169_0_test_JMP(EOS(STATIC_169), i14, i33) → 175_0_test_Load(EOS(STATIC_175), i14, i33)
171_0_test_Load(EOS(STATIC_171), i14, i14) → 191_0_test_Load(EOS(STATIC_191), i14, i14)
175_0_test_Load(EOS(STATIC_175), i14, i33) → 153_0_test_Load(EOS(STATIC_153), i14, i33)
191_0_test_Load(EOS(STATIC_191), i14, i38) → 194_0_test_LE(EOS(STATIC_194), i14, i38, i38)
194_0_test_LE(EOS(STATIC_194), i14, matching1, matching2) → 197_0_test_LE(EOS(STATIC_197), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
194_0_test_LE(EOS(STATIC_194), i14, i44, i44) → 198_0_test_LE(EOS(STATIC_198), i14, i44, i44)
197_0_test_LE(EOS(STATIC_197), i14, matching1, matching2) → 200_0_test_Load(EOS(STATIC_200), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
198_0_test_LE(EOS(STATIC_198), i14, i44, i44) → 202_0_test_Inc(EOS(STATIC_202), i14, i44) | >(i44, 0)
200_0_test_Load(EOS(STATIC_200), i14) → 204_0_test_Store(EOS(STATIC_204), i14, i14)
202_0_test_Inc(EOS(STATIC_202), i14, i44) → 207_0_test_JMP(EOS(STATIC_207), i14, +(i44, -1)) | >(i44, 0)
204_0_test_Store(EOS(STATIC_204), i14, i14) → 209_0_test_Load(EOS(STATIC_209), i14, i14)
207_0_test_JMP(EOS(STATIC_207), i14, i45) → 215_0_test_Load(EOS(STATIC_215), i14, i45)
209_0_test_Load(EOS(STATIC_209), i14, i14) → 232_0_test_Load(EOS(STATIC_232), i14, i14)
215_0_test_Load(EOS(STATIC_215), i14, i45) → 191_0_test_Load(EOS(STATIC_191), i14, i45)
232_0_test_Load(EOS(STATIC_232), i14, i49) → 235_0_test_LE(EOS(STATIC_235), i14, i49, i49)
235_0_test_LE(EOS(STATIC_235), i14, matching1, matching2) → 237_0_test_LE(EOS(STATIC_237), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
235_0_test_LE(EOS(STATIC_235), i14, i55, i55) → 238_0_test_LE(EOS(STATIC_238), i14, i55, i55)
237_0_test_LE(EOS(STATIC_237), i14, matching1, matching2) → 241_0_test_Load(EOS(STATIC_241), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
238_0_test_LE(EOS(STATIC_238), i14, i55, i55) → 243_0_test_Inc(EOS(STATIC_243), i14, i55) | >(i55, 0)
241_0_test_Load(EOS(STATIC_241), i14) → 245_0_test_Store(EOS(STATIC_245), i14, i14)
243_0_test_Inc(EOS(STATIC_243), i14, i55) → 247_0_test_JMP(EOS(STATIC_247), i14, +(i55, -1)) | >(i55, 0)
245_0_test_Store(EOS(STATIC_245), i14, i14) → 249_0_test_Load(EOS(STATIC_249), i14, i14)
247_0_test_JMP(EOS(STATIC_247), i14, i58) → 252_0_test_Load(EOS(STATIC_252), i14, i58)
249_0_test_Load(EOS(STATIC_249), i14, i14) → 267_0_test_Load(EOS(STATIC_267), i14, i14)
252_0_test_Load(EOS(STATIC_252), i14, i58) → 232_0_test_Load(EOS(STATIC_232), i14, i58)
267_0_test_Load(EOS(STATIC_267), i14, i62) → 270_0_test_LE(EOS(STATIC_270), i14, i62, i62)
270_0_test_LE(EOS(STATIC_270), i14, matching1, matching2) → 273_0_test_LE(EOS(STATIC_273), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
270_0_test_LE(EOS(STATIC_270), i14, i68, i68) → 274_0_test_LE(EOS(STATIC_274), i14, i68, i68)
273_0_test_LE(EOS(STATIC_273), i14, matching1, matching2) → 276_0_test_Load(EOS(STATIC_276), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
274_0_test_LE(EOS(STATIC_274), i14, i68, i68) → 278_0_test_Inc(EOS(STATIC_278), i14, i68) | >(i68, 0)
276_0_test_Load(EOS(STATIC_276), i14) → 280_0_test_Store(EOS(STATIC_280), i14, i14)
278_0_test_Inc(EOS(STATIC_278), i14, i68) → 282_0_test_JMP(EOS(STATIC_282), i14, +(i68, -1)) | >(i68, 0)
280_0_test_Store(EOS(STATIC_280), i14, i14) → 284_0_test_Load(EOS(STATIC_284), i14, i14)
282_0_test_JMP(EOS(STATIC_282), i14, i69) → 288_0_test_Load(EOS(STATIC_288), i14, i69)
284_0_test_Load(EOS(STATIC_284), i14, i14) → 303_0_test_Load(EOS(STATIC_303), i14, i14)
288_0_test_Load(EOS(STATIC_288), i14, i69) → 267_0_test_Load(EOS(STATIC_267), i14, i69)
303_0_test_Load(EOS(STATIC_303), i14, i74) → 306_0_test_LE(EOS(STATIC_306), i14, i74, i74)
306_0_test_LE(EOS(STATIC_306), i14, matching1, matching2) → 308_0_test_LE(EOS(STATIC_308), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
306_0_test_LE(EOS(STATIC_306), i14, i78, i78) → 310_0_test_LE(EOS(STATIC_310), i14, i78, i78)
308_0_test_LE(EOS(STATIC_308), i14, matching1, matching2) → 312_0_test_Load(EOS(STATIC_312), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
310_0_test_LE(EOS(STATIC_310), i14, i78, i78) → 314_0_test_Inc(EOS(STATIC_314), i14, i78) | >(i78, 0)
312_0_test_Load(EOS(STATIC_312), i14) → 316_0_test_Store(EOS(STATIC_316), i14, i14)
314_0_test_Inc(EOS(STATIC_314), i14, i78) → 318_0_test_JMP(EOS(STATIC_318), i14, +(i78, -1)) | >(i78, 0)
316_0_test_Store(EOS(STATIC_316), i14, i14) → 320_0_test_Load(EOS(STATIC_320), i14, i14)
318_0_test_JMP(EOS(STATIC_318), i14, i80) → 323_0_test_Load(EOS(STATIC_323), i14, i80)
320_0_test_Load(EOS(STATIC_320), i14, i14) → 338_0_test_Load(EOS(STATIC_338), i14, i14)
323_0_test_Load(EOS(STATIC_323), i14, i80) → 303_0_test_Load(EOS(STATIC_303), i14, i80)
338_0_test_Load(EOS(STATIC_338), i14, i86) → 341_0_test_LE(EOS(STATIC_341), i14, i86, i86)
341_0_test_LE(EOS(STATIC_341), i14, matching1, matching2) → 344_0_test_LE(EOS(STATIC_344), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
341_0_test_LE(EOS(STATIC_341), i14, i91, i91) → 345_0_test_LE(EOS(STATIC_345), i14, i91, i91)
344_0_test_LE(EOS(STATIC_344), i14, matching1, matching2) → 347_0_test_Load(EOS(STATIC_347), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
345_0_test_LE(EOS(STATIC_345), i14, i91, i91) → 349_0_test_Inc(EOS(STATIC_349), i14, i91) | >(i91, 0)
347_0_test_Load(EOS(STATIC_347), i14) → 351_0_test_Store(EOS(STATIC_351), i14, i14)
349_0_test_Inc(EOS(STATIC_349), i14, i91) → 353_0_test_JMP(EOS(STATIC_353), i14, +(i91, -1)) | >(i91, 0)
351_0_test_Store(EOS(STATIC_351), i14, i14) → 355_0_test_Load(EOS(STATIC_355), i14, i14)
353_0_test_JMP(EOS(STATIC_353), i14, i94) → 358_0_test_Load(EOS(STATIC_358), i14, i94)
355_0_test_Load(EOS(STATIC_355), i14, i14) → 373_0_test_Load(EOS(STATIC_373), i14, i14)
358_0_test_Load(EOS(STATIC_358), i14, i94) → 338_0_test_Load(EOS(STATIC_338), i14, i94)
373_0_test_Load(EOS(STATIC_373), i14, i98) → 376_0_test_LE(EOS(STATIC_376), i14, i98, i98)
376_0_test_LE(EOS(STATIC_376), i14, matching1, matching2) → 379_0_test_LE(EOS(STATIC_379), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
376_0_test_LE(EOS(STATIC_376), i14, i102, i102) → 380_0_test_LE(EOS(STATIC_380), i14, i102, i102)
379_0_test_LE(EOS(STATIC_379), i14, matching1, matching2) → 382_0_test_Load(EOS(STATIC_382), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
380_0_test_LE(EOS(STATIC_380), i14, i102, i102) → 384_0_test_Inc(EOS(STATIC_384), i14, i102) | >(i102, 0)
382_0_test_Load(EOS(STATIC_382), i14) → 386_0_test_Store(EOS(STATIC_386), i14, i14)
384_0_test_Inc(EOS(STATIC_384), i14, i102) → 388_0_test_JMP(EOS(STATIC_388), i14, +(i102, -1)) | >(i102, 0)
386_0_test_Store(EOS(STATIC_386), i14, i14) → 390_0_test_Load(EOS(STATIC_390), i14, i14)
388_0_test_JMP(EOS(STATIC_388), i14, i106) → 393_0_test_Load(EOS(STATIC_393), i14, i106)
390_0_test_Load(EOS(STATIC_390), i14, i14) → 407_0_test_Load(EOS(STATIC_407), i14, i14)
393_0_test_Load(EOS(STATIC_393), i14, i106) → 373_0_test_Load(EOS(STATIC_373), i14, i106)
407_0_test_Load(EOS(STATIC_407), i14, i109) → 410_0_test_LE(EOS(STATIC_410), i14, i109, i109)
410_0_test_LE(EOS(STATIC_410), i14, matching1, matching2) → 412_0_test_LE(EOS(STATIC_412), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
410_0_test_LE(EOS(STATIC_410), i14, i112, i112) → 414_0_test_LE(EOS(STATIC_414), i14, i112, i112)
412_0_test_LE(EOS(STATIC_412), i14, matching1, matching2) → 416_0_test_Load(EOS(STATIC_416), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
414_0_test_LE(EOS(STATIC_414), i14, i112, i112) → 418_0_test_Inc(EOS(STATIC_418), i14, i112) | >(i112, 0)
416_0_test_Load(EOS(STATIC_416), i14) → 420_0_test_Store(EOS(STATIC_420), i14, i14)
418_0_test_Inc(EOS(STATIC_418), i14, i112) → 421_0_test_JMP(EOS(STATIC_421), i14, +(i112, -1)) | >(i112, 0)
420_0_test_Store(EOS(STATIC_420), i14, i14) → 424_0_test_Load(EOS(STATIC_424), i14, i14)
421_0_test_JMP(EOS(STATIC_421), i14, i115) → 428_0_test_Load(EOS(STATIC_428), i14, i115)
424_0_test_Load(EOS(STATIC_424), i14, i14) → 443_0_test_Load(EOS(STATIC_443), i14, i14)
428_0_test_Load(EOS(STATIC_428), i14, i115) → 407_0_test_Load(EOS(STATIC_407), i14, i115)
443_0_test_Load(EOS(STATIC_443), i14, i122) → 446_0_test_LE(EOS(STATIC_446), i14, i122, i122)
446_0_test_LE(EOS(STATIC_446), i14, matching1, matching2) → 448_0_test_LE(EOS(STATIC_448), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
446_0_test_LE(EOS(STATIC_446), i14, i126, i126) → 449_0_test_LE(EOS(STATIC_449), i14, i126, i126)
448_0_test_LE(EOS(STATIC_448), i14, matching1, matching2) → 451_0_test_Load(EOS(STATIC_451), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
449_0_test_LE(EOS(STATIC_449), i14, i126, i126) → 453_0_test_Inc(EOS(STATIC_453), i14, i126) | >(i126, 0)
451_0_test_Load(EOS(STATIC_451), i14) → 455_0_test_Store(EOS(STATIC_455), i14, i14)
453_0_test_Inc(EOS(STATIC_453), i14, i126) → 457_0_test_JMP(EOS(STATIC_457), i14, +(i126, -1)) | >(i126, 0)
455_0_test_Store(EOS(STATIC_455), i14, i14) → 459_0_test_Load(EOS(STATIC_459), i14, i14)
457_0_test_JMP(EOS(STATIC_457), i14, i128) → 463_0_test_Load(EOS(STATIC_463), i14, i128)
459_0_test_Load(EOS(STATIC_459), i14, i14) → 477_0_test_Load(EOS(STATIC_477), i14, i14)
463_0_test_Load(EOS(STATIC_463), i14, i128) → 443_0_test_Load(EOS(STATIC_443), i14, i128)
477_0_test_Load(EOS(STATIC_477), i14, i132) → 479_0_test_LE(EOS(STATIC_479), i14, i132, i132)
479_0_test_LE(EOS(STATIC_479), i14, matching1, matching2) → 483_0_test_LE(EOS(STATIC_483), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
479_0_test_LE(EOS(STATIC_479), i14, i137, i137) → 484_0_test_LE(EOS(STATIC_484), i14, i137, i137)
483_0_test_LE(EOS(STATIC_483), i14, matching1, matching2) → 485_0_test_Load(EOS(STATIC_485), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
484_0_test_LE(EOS(STATIC_484), i14, i137, i137) → 488_0_test_Inc(EOS(STATIC_488), i14, i137) | >(i137, 0)
485_0_test_Load(EOS(STATIC_485), i14) → 491_0_test_Store(EOS(STATIC_491), i14, i14)
488_0_test_Inc(EOS(STATIC_488), i14, i137) → 493_0_test_JMP(EOS(STATIC_493), i14, +(i137, -1)) | >(i137, 0)
491_0_test_Store(EOS(STATIC_491), i14, i14) → 495_0_test_Load(EOS(STATIC_495), i14, i14)
493_0_test_JMP(EOS(STATIC_493), i14, i140) → 498_0_test_Load(EOS(STATIC_498), i14, i140)
495_0_test_Load(EOS(STATIC_495), i14, i14) → 512_0_test_Load(EOS(STATIC_512), i14, i14)
498_0_test_Load(EOS(STATIC_498), i14, i140) → 477_0_test_Load(EOS(STATIC_477), i14, i140)
512_0_test_Load(EOS(STATIC_512), i14, i144) → 515_0_test_LE(EOS(STATIC_515), i14, i144, i144)
515_0_test_LE(EOS(STATIC_515), i14, matching1, matching2) → 517_0_test_LE(EOS(STATIC_517), i14, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
515_0_test_LE(EOS(STATIC_515), i14, i150, i150) → 518_0_test_LE(EOS(STATIC_518), i14, i150, i150)
517_0_test_LE(EOS(STATIC_517), i14, matching1, matching2) → 520_0_test_Load(EOS(STATIC_520), i14) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
518_0_test_LE(EOS(STATIC_518), i14, i150, i150) → 522_0_test_Inc(EOS(STATIC_522), i14, i150) | >(i150, 0)
520_0_test_Load(EOS(STATIC_520), i14) → 524_0_test_Store(EOS(STATIC_524), i14)
522_0_test_Inc(EOS(STATIC_522), i14, i150) → 526_0_test_JMP(EOS(STATIC_526), i14, +(i150, -1)) | >(i150, 0)
524_0_test_Store(EOS(STATIC_524), i14) → 529_0_test_Load(EOS(STATIC_529), i14)
526_0_test_JMP(EOS(STATIC_526), i14, i153) → 533_0_test_Load(EOS(STATIC_533), i14, i153)
529_0_test_Load(EOS(STATIC_529), i14) → 546_0_test_Load(EOS(STATIC_546), i14)
533_0_test_Load(EOS(STATIC_533), i14, i153) → 512_0_test_Load(EOS(STATIC_512), i14, i153)
546_0_test_Load(EOS(STATIC_546), i158) → 549_0_test_LE(EOS(STATIC_549), i158, i158)
549_0_test_LE(EOS(STATIC_549), matching1, matching2) → 552_0_test_LE(EOS(STATIC_552), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
549_0_test_LE(EOS(STATIC_549), i161, i161) → 553_0_test_LE(EOS(STATIC_553), i161, i161)
552_0_test_LE(EOS(STATIC_552), matching1, matching2) → 555_0_test_Return(EOS(STATIC_555)) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
553_0_test_LE(EOS(STATIC_553), i161, i161) → 557_0_test_Inc(EOS(STATIC_557), i161) | >(i161, 0)
557_0_test_Inc(EOS(STATIC_557), i161) → 563_0_test_JMP(EOS(STATIC_563), +(i161, -1)) | >(i161, 0)
563_0_test_JMP(EOS(STATIC_563), i163) → 574_0_test_Load(EOS(STATIC_574), i163)
574_0_test_Load(EOS(STATIC_574), i163) → 546_0_test_Load(EOS(STATIC_546), i163)
Combined rules. Obtained 3 conditional rules for P and 25 conditional rules for R.
P rules:
92_0_main_GE(EOS(STATIC_92), x0, x1, x1, 100) → 103_1_main_InvokeMethod(103_0_test_Load(EOS(STATIC_103), x1), x0, x1, x1) | <(x1, 100)
103_1_main_InvokeMethod(555_0_test_Return(EOS(STATIC_555)), x0, x1, x1) → 92_0_main_GE(EOS(STATIC_92), x0, +(x1, 1), +(x1, 1), 100) | >(x1, 0)
92_0_main_GE(EOS(STATIC_92), x0, x1, x1, 100) → 92_0_main_GE(EOS(STATIC_92), -(x0, 1), -(x0, 1), -(x0, 1), 100) | &&(>(+(x1, 1), 100), >(x0, 1))
R rules:
103_0_test_Load(EOS(STATIC_103), x0) → 157_0_test_LE(EOS(STATIC_157), x0, x0, x0)
157_0_test_LE(EOS(STATIC_157), x0, x1, x1) → 157_0_test_LE(EOS(STATIC_157), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
157_0_test_LE(EOS(STATIC_157), x0, 0, 0) → 194_0_test_LE(EOS(STATIC_194), x0, x0, x0)
194_0_test_LE(EOS(STATIC_194), x0, x1, x1) → 194_0_test_LE(EOS(STATIC_194), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
194_0_test_LE(EOS(STATIC_194), x0, 0, 0) → 235_0_test_LE(EOS(STATIC_235), x0, x0, x0)
235_0_test_LE(EOS(STATIC_235), x0, x1, x1) → 235_0_test_LE(EOS(STATIC_235), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
235_0_test_LE(EOS(STATIC_235), x0, 0, 0) → 270_0_test_LE(EOS(STATIC_270), x0, x0, x0)
270_0_test_LE(EOS(STATIC_270), x0, x1, x1) → 270_0_test_LE(EOS(STATIC_270), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
270_0_test_LE(EOS(STATIC_270), x0, 0, 0) → 306_0_test_LE(EOS(STATIC_306), x0, x0, x0)
306_0_test_LE(EOS(STATIC_306), x0, x1, x1) → 306_0_test_LE(EOS(STATIC_306), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
306_0_test_LE(EOS(STATIC_306), x0, 0, 0) → 341_0_test_LE(EOS(STATIC_341), x0, x0, x0)
341_0_test_LE(EOS(STATIC_341), x0, x1, x1) → 341_0_test_LE(EOS(STATIC_341), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
341_0_test_LE(EOS(STATIC_341), x0, 0, 0) → 376_0_test_LE(EOS(STATIC_376), x0, x0, x0)
376_0_test_LE(EOS(STATIC_376), x0, x1, x1) → 376_0_test_LE(EOS(STATIC_376), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
376_0_test_LE(EOS(STATIC_376), x0, 0, 0) → 410_0_test_LE(EOS(STATIC_410), x0, x0, x0)
410_0_test_LE(EOS(STATIC_410), x0, x1, x1) → 410_0_test_LE(EOS(STATIC_410), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
410_0_test_LE(EOS(STATIC_410), x0, 0, 0) → 446_0_test_LE(EOS(STATIC_446), x0, x0, x0)
446_0_test_LE(EOS(STATIC_446), x0, x1, x1) → 446_0_test_LE(EOS(STATIC_446), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
446_0_test_LE(EOS(STATIC_446), x0, 0, 0) → 479_0_test_LE(EOS(STATIC_479), x0, x0, x0)
479_0_test_LE(EOS(STATIC_479), x0, x1, x1) → 479_0_test_LE(EOS(STATIC_479), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
479_0_test_LE(EOS(STATIC_479), x0, 0, 0) → 515_0_test_LE(EOS(STATIC_515), x0, x0, x0)
515_0_test_LE(EOS(STATIC_515), x0, x1, x1) → 515_0_test_LE(EOS(STATIC_515), x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
515_0_test_LE(EOS(STATIC_515), x0, 0, 0) → 549_0_test_LE(EOS(STATIC_549), x0, x0)
549_0_test_LE(EOS(STATIC_549), 0, 0) → 555_0_test_Return(EOS(STATIC_555))
549_0_test_LE(EOS(STATIC_549), x0, x0) → 549_0_test_LE(EOS(STATIC_549), +(x0, -1), +(x0, -1)) | >(x0, 0)
Filtered ground terms:
92_0_main_GE(x1, x2, x3, x4, x5) → 92_0_main_GE(x2, x3, x4)
Cond_92_0_main_GE1(x1, x2, x3, x4, x5, x6) → Cond_92_0_main_GE1(x1, x3, x4, x5)
Cond_103_1_main_InvokeMethod(x1, x2, x3, x4, x5) → Cond_103_1_main_InvokeMethod(x1, x3, x4, x5)
555_0_test_Return(x1) → 555_0_test_Return
103_0_test_Load(x1, x2) → 103_0_test_Load(x2)
Cond_92_0_main_GE(x1, x2, x3, x4, x5, x6) → Cond_92_0_main_GE(x1, x3, x4, x5)
549_0_test_LE(x1, x2, x3) → 549_0_test_LE(x2, x3)
Cond_549_0_test_LE(x1, x2, x3, x4) → Cond_549_0_test_LE(x1, x3, x4)
515_0_test_LE(x1, x2, x3, x4) → 515_0_test_LE(x2, x3, x4)
Cond_515_0_test_LE(x1, x2, x3, x4, x5) → Cond_515_0_test_LE(x1, x3, x4, x5)
479_0_test_LE(x1, x2, x3, x4) → 479_0_test_LE(x2, x3, x4)
Cond_479_0_test_LE(x1, x2, x3, x4, x5) → Cond_479_0_test_LE(x1, x3, x4, x5)
446_0_test_LE(x1, x2, x3, x4) → 446_0_test_LE(x2, x3, x4)
Cond_446_0_test_LE(x1, x2, x3, x4, x5) → Cond_446_0_test_LE(x1, x3, x4, x5)
410_0_test_LE(x1, x2, x3, x4) → 410_0_test_LE(x2, x3, x4)
Cond_410_0_test_LE(x1, x2, x3, x4, x5) → Cond_410_0_test_LE(x1, x3, x4, x5)
376_0_test_LE(x1, x2, x3, x4) → 376_0_test_LE(x2, x3, x4)
Cond_376_0_test_LE(x1, x2, x3, x4, x5) → Cond_376_0_test_LE(x1, x3, x4, x5)
341_0_test_LE(x1, x2, x3, x4) → 341_0_test_LE(x2, x3, x4)
Cond_341_0_test_LE(x1, x2, x3, x4, x5) → Cond_341_0_test_LE(x1, x3, x4, x5)
306_0_test_LE(x1, x2, x3, x4) → 306_0_test_LE(x2, x3, x4)
Cond_306_0_test_LE(x1, x2, x3, x4, x5) → Cond_306_0_test_LE(x1, x3, x4, x5)
270_0_test_LE(x1, x2, x3, x4) → 270_0_test_LE(x2, x3, x4)
Cond_270_0_test_LE(x1, x2, x3, x4, x5) → Cond_270_0_test_LE(x1, x3, x4, x5)
235_0_test_LE(x1, x2, x3, x4) → 235_0_test_LE(x2, x3, x4)
Cond_235_0_test_LE(x1, x2, x3, x4, x5) → Cond_235_0_test_LE(x1, x3, x4, x5)
194_0_test_LE(x1, x2, x3, x4) → 194_0_test_LE(x2, x3, x4)
Cond_194_0_test_LE(x1, x2, x3, x4, x5) → Cond_194_0_test_LE(x1, x3, x4, x5)
157_0_test_LE(x1, x2, x3, x4) → 157_0_test_LE(x2, x3, x4)
Cond_157_0_test_LE(x1, x2, x3, x4, x5) → Cond_157_0_test_LE(x1, x3, x4, x5)
Filtered duplicate args:
92_0_main_GE(x1, x2, x3) → 92_0_main_GE(x1, x3)
Cond_92_0_main_GE(x1, x2, x3, x4) → Cond_92_0_main_GE(x1, x2, x4)
103_1_main_InvokeMethod(x1, x2, x3, x4) → 103_1_main_InvokeMethod(x1, x2, x4)
Cond_103_1_main_InvokeMethod(x1, x2, x3, x4) → Cond_103_1_main_InvokeMethod(x1, x2, x4)
Cond_92_0_main_GE1(x1, x2, x3, x4) → Cond_92_0_main_GE1(x1, x2, x4)
Cond_157_0_test_LE(x1, x2, x3, x4) → Cond_157_0_test_LE(x1, x2, x4)
Cond_194_0_test_LE(x1, x2, x3, x4) → Cond_194_0_test_LE(x1, x2, x4)
Cond_235_0_test_LE(x1, x2, x3, x4) → Cond_235_0_test_LE(x1, x2, x4)
Cond_270_0_test_LE(x1, x2, x3, x4) → Cond_270_0_test_LE(x1, x2, x4)
Cond_306_0_test_LE(x1, x2, x3, x4) → Cond_306_0_test_LE(x1, x2, x4)
Cond_341_0_test_LE(x1, x2, x3, x4) → Cond_341_0_test_LE(x1, x2, x4)
Cond_376_0_test_LE(x1, x2, x3, x4) → Cond_376_0_test_LE(x1, x2, x4)
Cond_410_0_test_LE(x1, x2, x3, x4) → Cond_410_0_test_LE(x1, x2, x4)
Cond_446_0_test_LE(x1, x2, x3, x4) → Cond_446_0_test_LE(x1, x2, x4)
Cond_479_0_test_LE(x1, x2, x3, x4) → Cond_479_0_test_LE(x1, x2, x4)
Cond_515_0_test_LE(x1, x2, x3, x4) → Cond_515_0_test_LE(x1, x2, x4)
549_0_test_LE(x1, x2) → 549_0_test_LE(x2)
Cond_549_0_test_LE(x1, x2, x3) → Cond_549_0_test_LE(x1, x3)
Filtered unneeded arguments:
Cond_92_0_main_GE1(x1, x2, x3) → Cond_92_0_main_GE1(x1, x2)
Combined rules. Obtained 3 conditional rules for P and 25 conditional rules for R.
P rules:
92_0_main_GE(x0, x1) → 103_1_main_InvokeMethod(103_0_test_Load(x1), x0, x1) | <(x1, 100)
103_1_main_InvokeMethod(555_0_test_Return, x0, x1) → 92_0_main_GE(x0, +(x1, 1)) | >(x1, 0)
92_0_main_GE(x0, x1) → 92_0_main_GE(-(x0, 1), -(x0, 1)) | &&(>(x1, 99), >(x0, 1))
R rules:
103_0_test_Load(x0) → 157_0_test_LE(x0, x0, x0)
157_0_test_LE(x0, x1, x1) → 157_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
157_0_test_LE(x0, 0, 0) → 194_0_test_LE(x0, x0, x0)
194_0_test_LE(x0, x1, x1) → 194_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
194_0_test_LE(x0, 0, 0) → 235_0_test_LE(x0, x0, x0)
235_0_test_LE(x0, x1, x1) → 235_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
235_0_test_LE(x0, 0, 0) → 270_0_test_LE(x0, x0, x0)
270_0_test_LE(x0, x1, x1) → 270_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
270_0_test_LE(x0, 0, 0) → 306_0_test_LE(x0, x0, x0)
306_0_test_LE(x0, x1, x1) → 306_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
306_0_test_LE(x0, 0, 0) → 341_0_test_LE(x0, x0, x0)
341_0_test_LE(x0, x1, x1) → 341_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
341_0_test_LE(x0, 0, 0) → 376_0_test_LE(x0, x0, x0)
376_0_test_LE(x0, x1, x1) → 376_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
376_0_test_LE(x0, 0, 0) → 410_0_test_LE(x0, x0, x0)
410_0_test_LE(x0, x1, x1) → 410_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
410_0_test_LE(x0, 0, 0) → 446_0_test_LE(x0, x0, x0)
446_0_test_LE(x0, x1, x1) → 446_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
446_0_test_LE(x0, 0, 0) → 479_0_test_LE(x0, x0, x0)
479_0_test_LE(x0, x1, x1) → 479_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
479_0_test_LE(x0, 0, 0) → 515_0_test_LE(x0, x0, x0)
515_0_test_LE(x0, x1, x1) → 515_0_test_LE(x0, +(x1, -1), +(x1, -1)) | >(x1, 0)
515_0_test_LE(x0, 0, 0) → 549_0_test_LE(x0)
549_0_test_LE(0) → 555_0_test_Return
549_0_test_LE(x0) → 549_0_test_LE(+(x0, -1)) | >(x0, 0)
Finished conversion. Obtained 6 rules for P and 37 rules for R. System has predefined symbols.
P rules:
92_0_MAIN_GE(x0, x1) → COND_92_0_MAIN_GE(<(x1, 100), x0, x1)
COND_92_0_MAIN_GE(TRUE, x0, x1) → 103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1), x0, x1)
103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0, x1) → COND_103_1_MAIN_INVOKEMETHOD(>(x1, 0), 555_0_test_Return, x0, x1)
COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0, x1) → 92_0_MAIN_GE(x0, +(x1, 1))
92_0_MAIN_GE(x0, x1) → COND_92_0_MAIN_GE1(&&(>(x1, 99), >(x0, 1)), x0, x1)
COND_92_0_MAIN_GE1(TRUE, x0, x1) → 92_0_MAIN_GE(-(x0, 1), -(x0, 1))
R rules:
103_0_test_Load(x0) → 157_0_test_LE(x0, x0, x0)
157_0_test_LE(x0, x1, x1) → Cond_157_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_157_0_test_LE(TRUE, x0, x1, x1) → 157_0_test_LE(x0, +(x1, -1), +(x1, -1))
157_0_test_LE(x0, 0, 0) → 194_0_test_LE(x0, x0, x0)
194_0_test_LE(x0, x1, x1) → Cond_194_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_194_0_test_LE(TRUE, x0, x1, x1) → 194_0_test_LE(x0, +(x1, -1), +(x1, -1))
194_0_test_LE(x0, 0, 0) → 235_0_test_LE(x0, x0, x0)
235_0_test_LE(x0, x1, x1) → Cond_235_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_235_0_test_LE(TRUE, x0, x1, x1) → 235_0_test_LE(x0, +(x1, -1), +(x1, -1))
235_0_test_LE(x0, 0, 0) → 270_0_test_LE(x0, x0, x0)
270_0_test_LE(x0, x1, x1) → Cond_270_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_270_0_test_LE(TRUE, x0, x1, x1) → 270_0_test_LE(x0, +(x1, -1), +(x1, -1))
270_0_test_LE(x0, 0, 0) → 306_0_test_LE(x0, x0, x0)
306_0_test_LE(x0, x1, x1) → Cond_306_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_306_0_test_LE(TRUE, x0, x1, x1) → 306_0_test_LE(x0, +(x1, -1), +(x1, -1))
306_0_test_LE(x0, 0, 0) → 341_0_test_LE(x0, x0, x0)
341_0_test_LE(x0, x1, x1) → Cond_341_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_341_0_test_LE(TRUE, x0, x1, x1) → 341_0_test_LE(x0, +(x1, -1), +(x1, -1))
341_0_test_LE(x0, 0, 0) → 376_0_test_LE(x0, x0, x0)
376_0_test_LE(x0, x1, x1) → Cond_376_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_376_0_test_LE(TRUE, x0, x1, x1) → 376_0_test_LE(x0, +(x1, -1), +(x1, -1))
376_0_test_LE(x0, 0, 0) → 410_0_test_LE(x0, x0, x0)
410_0_test_LE(x0, x1, x1) → Cond_410_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_410_0_test_LE(TRUE, x0, x1, x1) → 410_0_test_LE(x0, +(x1, -1), +(x1, -1))
410_0_test_LE(x0, 0, 0) → 446_0_test_LE(x0, x0, x0)
446_0_test_LE(x0, x1, x1) → Cond_446_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_446_0_test_LE(TRUE, x0, x1, x1) → 446_0_test_LE(x0, +(x1, -1), +(x1, -1))
446_0_test_LE(x0, 0, 0) → 479_0_test_LE(x0, x0, x0)
479_0_test_LE(x0, x1, x1) → Cond_479_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_479_0_test_LE(TRUE, x0, x1, x1) → 479_0_test_LE(x0, +(x1, -1), +(x1, -1))
479_0_test_LE(x0, 0, 0) → 515_0_test_LE(x0, x0, x0)
515_0_test_LE(x0, x1, x1) → Cond_515_0_test_LE(>(x1, 0), x0, x1, x1)
Cond_515_0_test_LE(TRUE, x0, x1, x1) → 515_0_test_LE(x0, +(x1, -1), +(x1, -1))
515_0_test_LE(x0, 0, 0) → 549_0_test_LE(x0)
549_0_test_LE(0) → 555_0_test_Return
549_0_test_LE(x0) → Cond_549_0_test_LE(>(x0, 0), x0)
Cond_549_0_test_LE(TRUE, x0) → 549_0_test_LE(+(x0, -1))
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(3) -> (4), if (x0[3] →* x0[4]∧x1[3] + 1 →* x1[4])
(4) -> (5), if (x1[4] > 99 && x0[4] > 1 ∧x0[4] →* x0[5]∧x1[4] →* x1[5])
(5) -> (0), if (x0[5] - 1 →* x0[0]∧x0[5] - 1 →* x1[0])
(5) -> (4), if (x0[5] - 1 →* x0[4]∧x0[5] - 1 →* x1[4])
(1) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 92_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧92_0_MAIN_GE(x0[0], x1[0])≥COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(2) (<(x1[0], 100)=TRUE ⇒ 92_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧92_0_MAIN_GE(x0[0], x1[0])≥COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(3) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [bni_87]x0[0] ≥ 0∧[(-1)bso_88] ≥ 0)
(4) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [bni_87]x0[0] ≥ 0∧[(-1)bso_88] ≥ 0)
(5) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_87 + (-1)Bound*bni_87] + [bni_87]x0[0] ≥ 0∧[(-1)bso_88] ≥ 0)
(6) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_87] = 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 = 0∧[(-1)bso_88] ≥ 0)
(7) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_87] = 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 = 0∧[(-1)bso_88] ≥ 0)
(8) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[bni_87] = 0∧[(-1)bni_87 + (-1)Bound*bni_87] ≥ 0∧0 = 0∧[(-1)bso_88] ≥ 0)
(9) (COND_92_0_MAIN_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_92_0_MAIN_GE(TRUE, x0[1], x1[1])≥103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])∧(UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥))
(10) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧[(-1)bso_90] ≥ 0)
(11) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧[(-1)bso_90] ≥ 0)
(12) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧[(-1)bso_90] ≥ 0)
(13) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_89] = 0∧0 = 0∧0 = 0∧[(-1)bso_90] ≥ 0)
(14) (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥NonInfC∧103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥))
(15) (>(x1[2], 0)=TRUE ⇒ 103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥NonInfC∧103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥))
(16) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [bni_91]x0[2] ≥ 0∧[(-1)bso_92] ≥ 0)
(17) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [bni_91]x0[2] ≥ 0∧[(-1)bso_92] ≥ 0)
(18) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_91 + (-1)Bound*bni_91] + [bni_91]x0[2] ≥ 0∧[(-1)bso_92] ≥ 0)
(19) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[bni_91] = 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 = 0∧[(-1)bso_92] ≥ 0)
(20) (x1[2] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[bni_91] = 0∧[(-1)bni_91 + (-1)Bound*bni_91] ≥ 0∧0 = 0∧[(-1)bso_92] ≥ 0)
(21) (COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3])≥NonInfC∧COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3])≥92_0_MAIN_GE(x0[3], +(x1[3], 1))∧(UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥))
(22) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧[(-1)bso_94] ≥ 0)
(23) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧[(-1)bso_94] ≥ 0)
(24) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧[(-1)bso_94] ≥ 0)
(25) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_93] = 0∧0 = 0∧0 = 0∧[(-1)bso_94] ≥ 0)
(26) (&&(>(x1[4], 99), >(x0[4], 1))=TRUE∧x0[4]=x0[5]∧x1[4]=x1[5] ⇒ 92_0_MAIN_GE(x0[4], x1[4])≥NonInfC∧92_0_MAIN_GE(x0[4], x1[4])≥COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])∧(UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥))
(27) (>(x1[4], 99)=TRUE∧>(x0[4], 1)=TRUE ⇒ 92_0_MAIN_GE(x0[4], x1[4])≥NonInfC∧92_0_MAIN_GE(x0[4], x1[4])≥COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])∧(UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥))
(28) (x1[4] + [-100] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(29) (x1[4] + [-100] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(30) (x1[4] + [-100] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(31) (x1[4] ≥ 0∧x0[4] + [-2] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[(-1)bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(32) (x1[4] ≥ 0∧x0[4] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])), ≥)∧[bni_95 + (-1)Bound*bni_95] + [bni_95]x0[4] ≥ 0∧[(-1)bso_96] ≥ 0)
(33) (COND_92_0_MAIN_GE1(TRUE, x0[5], x1[5])≥NonInfC∧COND_92_0_MAIN_GE1(TRUE, x0[5], x1[5])≥92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))∧(UIncreasing(92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥))
(34) ((UIncreasing(92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧[1 + (-1)bso_98] ≥ 0)
(35) ((UIncreasing(92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧[1 + (-1)bso_98] ≥ 0)
(36) ((UIncreasing(92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧[1 + (-1)bso_98] ≥ 0)
(37) ((UIncreasing(92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))), ≥)∧[bni_97] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_98] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(103_0_test_Load(x1)) = [1]
POL(157_0_test_LE(x1, x2, x3)) = [1]
POL(Cond_157_0_test_LE(x1, x2, x3, x4)) = [1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(194_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + x2
POL(Cond_194_0_test_LE(x1, x2, x3, x4)) = [1] + x4 + [-1]x3
POL(235_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_235_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(270_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_270_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(306_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_306_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(341_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_341_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(376_0_test_LE(x1, x2, x3)) = [1]
POL(Cond_376_0_test_LE(x1, x2, x3, x4)) = [1]
POL(410_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_410_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(446_0_test_LE(x1, x2, x3)) = [1]
POL(Cond_446_0_test_LE(x1, x2, x3, x4)) = [1]
POL(479_0_test_LE(x1, x2, x3)) = [1] + x3 + [-1]x2
POL(Cond_479_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3
POL(515_0_test_LE(x1, x2, x3)) = [1]
POL(Cond_515_0_test_LE(x1, x2, x3, x4)) = [1]
POL(549_0_test_LE(x1)) = [1]
POL(555_0_test_Return) = [1]
POL(Cond_549_0_test_LE(x1, x2)) = [1]
POL(92_0_MAIN_GE(x1, x2)) = [-1] + x1
POL(COND_92_0_MAIN_GE(x1, x2, x3)) = [-1] + x2
POL(<(x1, x2)) = [-1]
POL(100) = [100]
POL(103_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1]x1 + x2
POL(COND_103_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + x3
POL(1) = [1]
POL(COND_92_0_MAIN_GE1(x1, x2, x3)) = [-1] + x2
POL(&&(x1, x2)) = [-1]
POL(99) = [99]
POL(-(x1, x2)) = x1 + [-1]x2
COND_92_0_MAIN_GE1(TRUE, x0[5], x1[5]) → 92_0_MAIN_GE(-(x0[5], 1), -(x0[5], 1))
92_0_MAIN_GE(x0[4], x1[4]) → COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])
92_0_MAIN_GE(x0[0], x1[0]) → COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
COND_92_0_MAIN_GE(TRUE, x0[1], x1[1]) → 103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])
103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2]) → COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])
COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3]) → 92_0_MAIN_GE(x0[3], +(x1[3], 1))
92_0_MAIN_GE(x0[4], x1[4]) → COND_92_0_MAIN_GE1(&&(>(x1[4], 99), >(x0[4], 1)), x0[4], x1[4])
103_0_test_Load(x0)1 ↔ 157_0_test_LE(x0, x0, x0)1
157_0_test_LE(x0, 0, 0)1 ↔ 194_0_test_LE(x0, x0, x0)1
Cond_157_0_test_LE(TRUE, x0, x1, x1)1 ↔ 157_0_test_LE(x0, +(x1, -1), +(x1, -1))1
157_0_test_LE(x0, x1, x1)1 ↔ Cond_157_0_test_LE(>(x1, 0), x0, x1, x1)1
194_0_test_LE(x0, 0, 0)1 ↔ 235_0_test_LE(x0, x0, x0)1
Cond_194_0_test_LE(TRUE, x0, x1, x1)1 ↔ 194_0_test_LE(x0, +(x1, -1), +(x1, -1))1
194_0_test_LE(x0, x1, x1)1 ↔ Cond_194_0_test_LE(>(x1, 0), x0, x1, x1)1
235_0_test_LE(x0, 0, 0)1 ↔ 270_0_test_LE(x0, x0, x0)1
Cond_235_0_test_LE(TRUE, x0, x1, x1)1 ↔ 235_0_test_LE(x0, +(x1, -1), +(x1, -1))1
235_0_test_LE(x0, x1, x1)1 ↔ Cond_235_0_test_LE(>(x1, 0), x0, x1, x1)1
270_0_test_LE(x0, 0, 0)1 ↔ 306_0_test_LE(x0, x0, x0)1
Cond_270_0_test_LE(TRUE, x0, x1, x1)1 ↔ 270_0_test_LE(x0, +(x1, -1), +(x1, -1))1
270_0_test_LE(x0, x1, x1)1 ↔ Cond_270_0_test_LE(>(x1, 0), x0, x1, x1)1
306_0_test_LE(x0, 0, 0)1 ↔ 341_0_test_LE(x0, x0, x0)1
Cond_306_0_test_LE(TRUE, x0, x1, x1)1 ↔ 306_0_test_LE(x0, +(x1, -1), +(x1, -1))1
306_0_test_LE(x0, x1, x1)1 ↔ Cond_306_0_test_LE(>(x1, 0), x0, x1, x1)1
341_0_test_LE(x0, 0, 0)1 ↔ 376_0_test_LE(x0, x0, x0)1
Cond_341_0_test_LE(TRUE, x0, x1, x1)1 ↔ 341_0_test_LE(x0, +(x1, -1), +(x1, -1))1
341_0_test_LE(x0, x1, x1)1 ↔ Cond_341_0_test_LE(>(x1, 0), x0, x1, x1)1
376_0_test_LE(x0, 0, 0)1 ↔ 410_0_test_LE(x0, x0, x0)1
Cond_376_0_test_LE(TRUE, x0, x1, x1)1 ↔ 376_0_test_LE(x0, +(x1, -1), +(x1, -1))1
376_0_test_LE(x0, x1, x1)1 ↔ Cond_376_0_test_LE(>(x1, 0), x0, x1, x1)1
410_0_test_LE(x0, 0, 0)1 ↔ 446_0_test_LE(x0, x0, x0)1
Cond_410_0_test_LE(TRUE, x0, x1, x1)1 ↔ 410_0_test_LE(x0, +(x1, -1), +(x1, -1))1
410_0_test_LE(x0, x1, x1)1 ↔ Cond_410_0_test_LE(>(x1, 0), x0, x1, x1)1
446_0_test_LE(x0, 0, 0)1 ↔ 479_0_test_LE(x0, x0, x0)1
Cond_446_0_test_LE(TRUE, x0, x1, x1)1 ↔ 446_0_test_LE(x0, +(x1, -1), +(x1, -1))1
446_0_test_LE(x0, x1, x1)1 ↔ Cond_446_0_test_LE(>(x1, 0), x0, x1, x1)1
479_0_test_LE(x0, 0, 0)1 ↔ 515_0_test_LE(x0, x0, x0)1
Cond_479_0_test_LE(TRUE, x0, x1, x1)1 ↔ 479_0_test_LE(x0, +(x1, -1), +(x1, -1))1
479_0_test_LE(x0, x1, x1)1 ↔ Cond_479_0_test_LE(>(x1, 0), x0, x1, x1)1
515_0_test_LE(x0, 0, 0)1 ↔ 549_0_test_LE(x0)1
Cond_515_0_test_LE(TRUE, x0, x1, x1)1 ↔ 515_0_test_LE(x0, +(x1, -1), +(x1, -1))1
515_0_test_LE(x0, x1, x1)1 ↔ Cond_515_0_test_LE(>(x1, 0), x0, x1, x1)1
549_0_test_LE(0)1 ↔ 555_0_test_Return1
549_0_test_LE(x0)1 ↔ Cond_549_0_test_LE(>(x0, 0), x0)1
Cond_549_0_test_LE(TRUE, x0)1 ↔ 549_0_test_LE(+(x0, -1))1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer, Boolean
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(3) -> (4), if (x0[3] →* x0[4]∧x1[3] + 1 →* x1[4])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(1) (COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3])≥NonInfC∧COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3])≥92_0_MAIN_GE(x0[3], +(x1[3], 1))∧(UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥))
(2) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧[(-1)bso_37] ≥ 0)
(3) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧[(-1)bso_37] ≥ 0)
(4) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧[(-1)bso_37] ≥ 0)
(5) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_36] = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
(6) (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥NonInfC∧103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥))
(7) (>(x1[2], 0)=TRUE ⇒ 103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥NonInfC∧103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥))
(8) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(2)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)
(9) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(2)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)
(10) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(2)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)
(11) (x1[2] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)
(12) (COND_92_0_MAIN_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_92_0_MAIN_GE(TRUE, x0[1], x1[1])≥103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])∧(UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥))
(13) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)
(14) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)
(15) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧[(-1)bso_41] ≥ 0)
(16) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_40] = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
(17) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 92_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧92_0_MAIN_GE(x0[0], x1[0])≥COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(18) (<(x1[0], 100)=TRUE ⇒ 92_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧92_0_MAIN_GE(x0[0], x1[0])≥COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(19) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(20) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(21) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(22) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_42 + (-1)Bound*bni_42] + [bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
(23) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(2)bni_42 + (-1)Bound*bni_42] + [(-1)bni_42]x1[0] ≥ 0∧[(-1)bso_43] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(103_0_test_Load(x1)) = [-1] + [-1]x1
POL(157_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(Cond_157_0_test_LE(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(194_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2
POL(Cond_194_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x3 + [-1]x2
POL(235_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x1
POL(Cond_235_0_test_LE(x1, x2, x3, x4)) = [2] + [-1]x4 + [-1]x3 + [-1]x2
POL(270_0_test_LE(x1, x2, x3)) = [2] + x3 + [-1]x2 + x1
POL(Cond_270_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [-1]x2
POL(306_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + [2]x1
POL(Cond_306_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3 + [-1]x2
POL(341_0_test_LE(x1, x2, x3)) = x3 + [-1]x2 + x1
POL(Cond_341_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x4 + x3 + [-1]x2
POL(376_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_376_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3 + [-1]x2
POL(410_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [2]x1
POL(Cond_410_0_test_LE(x1, x2, x3, x4)) = [2]x4 + [-1]x3 + [-1]x2
POL(446_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + x1
POL(Cond_446_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2
POL(479_0_test_LE(x1, x2, x3)) = [-1] + x3 + x2 + x1
POL(Cond_479_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [-1]x2
POL(515_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + [-1]x2
POL(Cond_515_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3 + [-1]x2
POL(549_0_test_LE(x1)) = [1] + x1
POL(555_0_test_Return) = [-1]
POL(Cond_549_0_test_LE(x1, x2)) = [-1] + [-1]x2
POL(COND_103_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [1] + [-1]x4
POL(92_0_MAIN_GE(x1, x2)) = [2] + [-1]x2
POL(1) = [1]
POL(103_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [2] + [-1]x3
POL(COND_92_0_MAIN_GE(x1, x2, x3)) = [2] + [-1]x3
POL(<(x1, x2)) = [1]
POL(100) = [100]
103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2]) → COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])
92_0_MAIN_GE(x0[0], x1[0]) → COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3]) → 92_0_MAIN_GE(x0[3], +(x1[3], 1))
COND_92_0_MAIN_GE(TRUE, x0[1], x1[1]) → 103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])
92_0_MAIN_GE(x0[0], x1[0]) → COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(5) -> (0), if (x0[5] - 1 →* x0[0]∧x0[5] - 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(3) -> (0), if (x0[3] →* x0[0]∧x1[3] + 1 →* x1[0])
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])
(1) (COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3])≥NonInfC∧COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3])≥92_0_MAIN_GE(x0[3], +(x1[3], 1))∧(UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥))
(2) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧[1 + (-1)bso_36] ≥ 0)
(3) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧[1 + (-1)bso_36] ≥ 0)
(4) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧[1 + (-1)bso_36] ≥ 0)
(5) ((UIncreasing(92_0_MAIN_GE(x0[3], +(x1[3], 1))), ≥)∧[bni_35] = 0∧0 = 0∧[1 + (-1)bso_36] ≥ 0)
(6) (>(x1[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3] ⇒ 103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥NonInfC∧103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥))
(7) (>(x1[2], 0)=TRUE ⇒ 103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥NonInfC∧103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2])≥COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])∧(UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥))
(8) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(9) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(10) (x1[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-1)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(11) (x1[2] ≥ 0 ⇒ (UIncreasing(COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])), ≥)∧[(-2)bni_37 + (-1)Bound*bni_37] + [(-1)bni_37]x1[2] ≥ 0∧[(-1)bso_38] ≥ 0)
(12) (COND_92_0_MAIN_GE(TRUE, x0[1], x1[1])≥NonInfC∧COND_92_0_MAIN_GE(TRUE, x0[1], x1[1])≥103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])∧(UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥))
(13) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)
(14) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)
(15) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧[(-1)bso_40] ≥ 0)
(16) ((UIncreasing(103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])), ≥)∧[bni_39] = 0∧0 = 0∧[(-1)bso_40] ≥ 0)
(17) (<(x1[0], 100)=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1] ⇒ 92_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧92_0_MAIN_GE(x0[0], x1[0])≥COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(18) (<(x1[0], 100)=TRUE ⇒ 92_0_MAIN_GE(x0[0], x1[0])≥NonInfC∧92_0_MAIN_GE(x0[0], x1[0])≥COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])∧(UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥))
(19) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(20) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(21) ([99] + [-1]x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(22) ([99] + x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
(23) ([99] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [(-1)bni_41]x1[0] ≥ 0∧[(-1)bso_42] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(103_0_test_Load(x1)) = [-1]
POL(157_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_157_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(194_0_test_LE(x1, x2, x3)) = [-1] + x3 + [-1]x2
POL(Cond_194_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + x3
POL(235_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_235_0_test_LE(x1, x2, x3, x4)) = [1] + [-1]x3
POL(270_0_test_LE(x1, x2, x3)) = [-1] + [2]x3 + [-1]x2 + [2]x1
POL(Cond_270_0_test_LE(x1, x2, x3, x4)) = [2] + [-1]x4 + [2]x3
POL(306_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_306_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3
POL(341_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_341_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x3
POL(376_0_test_LE(x1, x2, x3)) = [1] + [-1]x3 + [-1]x1
POL(Cond_376_0_test_LE(x1, x2, x3, x4)) = [-1] + x4 + [-1]x3
POL(410_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_410_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3
POL(446_0_test_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_446_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3
POL(479_0_test_LE(x1, x2, x3)) = [-1]x3 + [-1]x2 + x1
POL(Cond_479_0_test_LE(x1, x2, x3, x4)) = [2] + [2]x4 + [-1]x3
POL(515_0_test_LE(x1, x2, x3)) = [2] + [-1]x3 + [-1]x2 + [-1]x1
POL(Cond_515_0_test_LE(x1, x2, x3, x4)) = [-1] + [-1]x3
POL(549_0_test_LE(x1)) = [2] + [-1]x1
POL(555_0_test_Return) = [-1]
POL(Cond_549_0_test_LE(x1, x2)) = [-1] + [-1]x2
POL(COND_103_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x4
POL(92_0_MAIN_GE(x1, x2)) = [-1] + [-1]x2
POL(1) = [1]
POL(103_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3
POL(COND_92_0_MAIN_GE(x1, x2, x3)) = [-1] + [-1]x3
POL(<(x1, x2)) = [-1]
POL(100) = [100]
COND_103_1_MAIN_INVOKEMETHOD(TRUE, 555_0_test_Return, x0[3], x1[3]) → 92_0_MAIN_GE(x0[3], +(x1[3], 1))
92_0_MAIN_GE(x0[0], x1[0]) → COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
103_1_MAIN_INVOKEMETHOD(555_0_test_Return, x0[2], x1[2]) → COND_103_1_MAIN_INVOKEMETHOD(>(x1[2], 0), 555_0_test_Return, x0[2], x1[2])
COND_92_0_MAIN_GE(TRUE, x0[1], x1[1]) → 103_1_MAIN_INVOKEMETHOD(103_0_test_Load(x1[1]), x0[1], x1[1])
92_0_MAIN_GE(x0[0], x1[0]) → COND_92_0_MAIN_GE(<(x1[0], 100), x0[0], x1[0])
515_0_test_LE(x0, 0, 0)1 ↔ 549_0_test_LE(x0)1
549_0_test_LE(0)1 → 555_0_test_Return1
549_0_test_LE(x0)1 → Cond_549_0_test_LE(>(x0, 0), x0)1
549_0_test_LE(+(x0, -1))1 → Cond_549_0_test_LE(TRUE, x0)1
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(0) -> (1), if (x1[0] < 100 ∧x0[0] →* x0[1]∧x1[0] →* x1[1])
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
!= | ~ | Neq: (Integer, Integer) -> Boolean |
* | ~ | Mul: (Integer, Integer) -> Integer |
>= | ~ | Ge: (Integer, Integer) -> Boolean |
-1 | ~ | UnaryMinus: (Integer) -> Integer |
| | ~ | Bwor: (Integer, Integer) -> Integer |
/ | ~ | Div: (Integer, Integer) -> Integer |
= | ~ | Eq: (Integer, Integer) -> Boolean |
~ | Bwxor: (Integer, Integer) -> Integer | |
|| | ~ | Lor: (Boolean, Boolean) -> Boolean |
! | ~ | Lnot: (Boolean) -> Boolean |
< | ~ | Lt: (Integer, Integer) -> Boolean |
- | ~ | Sub: (Integer, Integer) -> Integer |
<= | ~ | Le: (Integer, Integer) -> Boolean |
> | ~ | Gt: (Integer, Integer) -> Boolean |
~ | ~ | Bwnot: (Integer) -> Integer |
% | ~ | Mod: (Integer, Integer) -> Integer |
& | ~ | Bwand: (Integer, Integer) -> Integer |
+ | ~ | Add: (Integer, Integer) -> Integer |
&& | ~ | Land: (Boolean, Boolean) -> Boolean |
Integer
(1) -> (2), if (103_0_test_Load(x1[1]) →* 555_0_test_Return∧x0[1] →* x0[2]∧x1[1] →* x1[2])
(2) -> (3), if (x1[2] > 0 ∧x0[2] →* x0[3]∧x1[2] →* x1[3])