LTS Termination Proof

by AProVE

Input

• Initial Location: f795_0_main_GE, f1421_0_sort_GE, f1445_0_aux_LT, f1_0_main_Load, f1611_0_aux_InvokeMethod, __init
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f795_0_main_GE:		x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x8 = _arg8 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ x8 = _arg8P ∧ 0 = _arg8P ∧ 0 = _arg7P ∧ 0 = _arg6P ∧ 0 = _arg5P ∧ 0 = _arg4P ∧ 0 = _arg3P ∧ 0 = _arg2 ∧ 0 ≤ _arg2P − 1 ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ _arg2P ≤ _arg1 ∧ _arg1P ≤ _arg1
  f1_0_main_Load	2	f795_0_main_GE:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x7 ∧ x8 = _x8 ∧ x1 = _x9 ∧ x2 = _x10 ∧ x3 = _x13 ∧ x4 = _x14 ∧ x5 = _x15 ∧ x6 = _x16 ∧ x7 = _x17 ∧ x8 = _x18 ∧ _x9 ≤ _x ∧ −1 ≤ _x19 − 1 ∧ _x10 ≤ _x ∧ 0 ≤ _x − 1 ∧ 0 ≤ _x9 − 1 ∧ 0 ≤ _x10 − 1 ∧ 1 = _x1 ∧ 0 = _x13 ∧ 0 = _x14 ∧ 1 = _x15 ∧ 1 = _x16 ∧ 1 = _x17 ∧ 0 = _x18
  f1_0_main_Load	3	f795_0_main_GE:		x1 = _x20 ∧ x2 = _x21 ∧ x3 = _x22 ∧ x4 = _x23 ∧ x5 = _x24 ∧ x6 = _x25 ∧ x7 = _x26 ∧ x8 = _x27 ∧ x1 = _x28 ∧ x2 = _x29 ∧ x3 = _x30 ∧ x4 = _x31 ∧ x5 = _x32 ∧ x6 = _x33 ∧ x7 = _x34 ∧ x8 = _x35 ∧ −1 ≤ _x36 − 1 ∧ 1 ≤ _x21 − 1 ∧ 0 ≤ _x36⋅_x37 ∧ −1 ≤ _x37 − 1 ∧ _x28 ≤ _x20 ∧ _x29 ≤ _x20 ∧ 0 ≤ _x20 − 1 ∧ 0 ≤ _x28 − 1 ∧ 0 ≤ _x29 − 1 ∧ 0 = _x30 ∧ _x36⋅_x37 = _x31 ∧ _x21 = _x32 ∧ 2 = _x33 ∧ _x21 = _x34 ∧ _x36⋅_x37 = _x35
  f795_0_main_GE	4	f795_0_main_GE:		x1 = _x38 ∧ x2 = _x39 ∧ x3 = _x40 ∧ x4 = _x41 ∧ x5 = _x42 ∧ x6 = _x43 ∧ x7 = _x44 ∧ x8 = _x45 ∧ x1 = _x46 ∧ x2 = _x47 ∧ x3 = _x48 ∧ x4 = _x49 ∧ x5 = _x50 ∧ x6 = _x51 ∧ x7 = _x52 ∧ x8 = _x53 ∧ _x41 = _x53 ∧ _x42 = _x52 ∧ _x43 = _x51 ∧ _x42 = _x50 ∧ _x41 = _x49 ∧ _x40 + 1 = _x48 ∧ _x41 = _x45 ∧ _x42 = _x44 ∧ 0 ≤ _x47 − 1 ∧ 0 ≤ _x46 − 1 ∧ 0 ≤ _x39 − 1 ∧ 0 ≤ _x38 − 1 ∧ _x47 ≤ _x39 ∧ _x47 ≤ _x38 ∧ _x46 ≤ _x39 ∧ _x46 ≤ _x38 ∧ −1 ≤ _x41 − 1 ∧ _x42 ≤ _x43 ∧ −1 ≤ _x42 − 1 ∧ _x40 ≤ _x41 − 1
  f795_0_main_GE	5	f795_0_main_GE:		x1 = _x54 ∧ x2 = _x55 ∧ x3 = _x56 ∧ x4 = _x57 ∧ x5 = _x58 ∧ x6 = _x59 ∧ x7 = _x60 ∧ x8 = _x61 ∧ x1 = _x62 ∧ x2 = _x63 ∧ x3 = _x64 ∧ x4 = _x65 ∧ x5 = _x66 ∧ x6 = _x67 ∧ x7 = _x70 ∧ x8 = _x71 ∧ _x57 = _x71 ∧ _x58 = _x70 ∧ _x59 + 1 = _x67 ∧ _x58 = _x66 ∧ _x57 = _x65 ∧ _x56 + 1 = _x64 ∧ _x57 = _x61 ∧ _x58 = _x60 ∧ 0 ≤ _x63 − 1 ∧ 0 ≤ _x62 − 1 ∧ 0 ≤ _x55 − 1 ∧ 0 ≤ _x54 − 1 ∧ _x63 ≤ _x55 ∧ _x63 ≤ _x54 ∧ _x62 ≤ _x55 ∧ _x62 ≤ _x54 ∧ −1 ≤ _x57 − 1 ∧ _x59 ≤ _x58 − 1 ∧ −1 ≤ _x59 − 1 ∧ −1 ≤ _x58 − 1 ∧ _x56 ≤ _x57 − 1
  f795_0_main_GE	6	f1421_0_sort_GE:		x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ x6 = _x79 ∧ x7 = _x80 ∧ x8 = _x81 ∧ x1 = _x82 ∧ x2 = _x83 ∧ x3 = _x84 ∧ x4 = _x85 ∧ x5 = _x86 ∧ x6 = _x87 ∧ x7 = _x88 ∧ x8 = _x89 ∧ _x75 = _x86 ∧ _x75 = _x85 ∧ 1 = _x84 ∧ _x75 = _x81 ∧ _x76 = _x80 ∧ 0 ≤ _x83 − 1 ∧ 0 ≤ _x82 − 1 ∧ 0 ≤ _x73 − 1 ∧ 0 ≤ _x72 − 1 ∧ _x83 ≤ _x73 ∧ _x83 ≤ _x72 ∧ _x82 ≤ _x73 ∧ _x82 ≤ _x72 ∧ _x75 ≤ _x74 ∧ −1 ≤ _x75 − 1
  f1421_0_sort_GE	7	f1421_0_sort_GE:		x1 = _x90 ∧ x2 = _x91 ∧ x3 = _x92 ∧ x4 = _x93 ∧ x5 = _x94 ∧ x6 = _x95 ∧ x7 = _x96 ∧ x8 = _x97 ∧ x1 = _x98 ∧ x2 = _x99 ∧ x3 = _x100 ∧ x4 = _x101 ∧ x5 = _x102 ∧ x6 = _x103 ∧ x7 = _x104 ∧ x8 = _x105 ∧ _x94 = _x102 ∧ _x93 = _x101 ∧ _x92 + 1 = _x100 ∧ 0 ≤ _x99 − 1 ∧ 0 ≤ _x98 − 1 ∧ 0 ≤ _x91 − 1 ∧ 0 ≤ _x90 − 1 ∧ _x99 ≤ _x91 ∧ _x99 ≤ _x90 ∧ _x98 ≤ _x91 ∧ _x98 ≤ _x90 ∧ _x92 ≤ _x93 − 1 ∧ 0 ≤ _x92 − 1 ∧ 1 ≤ _x93 − 1 ∧ 1 ≤ _x93 − _x92
  f1421_0_sort_GE	8	f1421_0_sort_GE:		x1 = _x106 ∧ x2 = _x107 ∧ x3 = _x108 ∧ x4 = _x109 ∧ x5 = _x110 ∧ x6 = _x111 ∧ x7 = _x112 ∧ x8 = _x113 ∧ x1 = _x114 ∧ x2 = _x115 ∧ x3 = _x116 ∧ x4 = _x117 ∧ x5 = _x118 ∧ x6 = _x119 ∧ x7 = _x120 ∧ x8 = _x121 ∧ _x109 = _x117 ∧ _x108 + 1 = _x116 ∧ 0 ≤ _x115 − 1 ∧ 0 ≤ _x114 − 1 ∧ 0 ≤ _x107 − 1 ∧ 0 ≤ _x106 − 1 ∧ _x115 ≤ _x107 ∧ _x115 ≤ _x106 ∧ _x114 ≤ _x107 ∧ _x114 ≤ _x106 ∧ _x108 ≤ _x109 − 1 ∧ 0 ≤ _x108 − 1 ∧ 1 ≤ _x109 − 1 ∧ 1 ≤ _x109 − _x108
  f1421_0_sort_GE	9	f1445_0_aux_LT:		x1 = _x122 ∧ x2 = _x123 ∧ x3 = _x124 ∧ x4 = _x125 ∧ x5 = _x126 ∧ x6 = _x127 ∧ x7 = _x128 ∧ x8 = _x129 ∧ x1 = _x130 ∧ x2 = _x131 ∧ x3 = _x132 ∧ x4 = _x133 ∧ x5 = _x134 ∧ x6 = _x135 ∧ x7 = _x136 ∧ x8 = _x137 ∧ _x126 = _x135 ∧ _x125 − _x124 = _x134 ∧ 0 = _x133 ∧ 0 = _x131 ∧ 0 = _x130 ∧ 0 ≤ _x132 − 1 ∧ 0 ≤ _x123 − 1 ∧ 0 ≤ _x122 − 1 ∧ _x132 ≤ _x123 ∧ _x132 ≤ _x122 ∧ _x124 ≤ _x125 − 1 ∧ 0 ≤ _x124 − 1 ∧ 1 ≤ _x125 − 1 ∧ 1 ≤ _x125 − _x124
  f1445_0_aux_LT	10	f1611_0_aux_InvokeMethod:		x1 = _x138 ∧ x2 = _x139 ∧ x3 = _x140 ∧ x4 = _x141 ∧ x5 = _x142 ∧ x6 = _x143 ∧ x7 = _x144 ∧ x8 = _x145 ∧ x1 = _x146 ∧ x2 = _x147 ∧ x3 = _x148 ∧ x4 = _x149 ∧ x5 = _x150 ∧ x6 = _x151 ∧ x7 = _x152 ∧ x8 = _x153 ∧ −1 ≤ _x139 − 1 ∧ _x139 + 1 ≤ _x143 − 1 ∧ _x139 ≤ _x142 − 1 ∧ _x154 ≤ _x155 ∧ _x149 ≤ _x140 ∧ 0 ≤ _x140 − 1 ∧ 0 ≤ _x149 − 1 ∧ _x139 = _x141 ∧ _x138 = _x146 ∧ _x139 + 1 = _x147 ∧ _x142 = _x148 ∧ _x143 = _x151
  f1445_0_aux_LT	11	f1611_0_aux_InvokeMethod:		x1 = _x156 ∧ x2 = _x157 ∧ x3 = _x158 ∧ x4 = _x159 ∧ x5 = _x160 ∧ x6 = _x161 ∧ x7 = _x162 ∧ x8 = _x163 ∧ x1 = _x164 ∧ x2 = _x165 ∧ x3 = _x166 ∧ x4 = _x167 ∧ x5 = _x168 ∧ x6 = _x169 ∧ x7 = _x170 ∧ x8 = _x171 ∧ −1 ≤ _x157 − 1 ∧ _x157 + 1 ≤ _x161 − 1 ∧ _x157 ≤ _x160 − 1 ∧ _x172 ≤ _x173 − 1 ∧ _x167 ≤ _x158 ∧ 0 ≤ _x158 − 1 ∧ 0 ≤ _x167 − 1 ∧ _x157 = _x159 ∧ _x156 = _x164 ∧ _x157 + 1 = _x165 ∧ _x160 = _x166 ∧ _x161 = _x169
  f1611_0_aux_InvokeMethod	12	f1445_0_aux_LT:		x1 = _x174 ∧ x2 = _x175 ∧ x3 = _x176 ∧ x4 = _x177 ∧ x5 = _x178 ∧ x6 = _x179 ∧ x7 = _x180 ∧ x8 = _x181 ∧ x1 = _x182 ∧ x2 = _x183 ∧ x3 = _x184 ∧ x4 = _x185 ∧ x5 = _x186 ∧ x6 = _x187 ∧ x7 = _x188 ∧ x8 = _x189 ∧ _x179 = _x187 ∧ _x176 = _x186 ∧ _x175 = _x185 ∧ _x175 = _x183 ∧ _x175 = _x182 ∧ 0 ≤ _x184 − 1 ∧ 0 ≤ _x177 − 1 ∧ _x184 ≤ _x177 ∧ _x174 ≤ _x176 ∧ _x175 ≤ _x176 ∧ 0 ≤ _x175 − 1 ∧ 0 ≤ _x176 − 1
  __init	13	f1_0_main_Load:		x1 = _x190 ∧ x2 = _x191 ∧ x3 = _x192 ∧ x4 = _x193 ∧ x5 = _x194 ∧ x6 = _x195 ∧ x7 = _x196 ∧ x8 = _x197 ∧ x1 = _x198 ∧ x2 = _x199 ∧ x3 = _x200 ∧ x4 = _x201 ∧ x5 = _x202 ∧ x6 = _x203 ∧ x7 = _x204 ∧ x8 = _x205 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

We consider subproblems for each of the 3 SCC(s) of the program graph.

2.1 SCC Subproblem 1/3

Here we consider the SCC { f795_0_main_GE }.

2.1.1 Transition Removal

We remove transitions 4, 5 using the following ranking functions, which are bounded by 0.

2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/3

Here we consider the SCC { f1421_0_sort_GE }.

2.2.1 Transition Removal

We remove transition 8 using the following ranking functions, which are bounded by 0.

2.2.2 Transition Removal

We remove transition 7 using the following ranking functions, which are bounded by 0.

2.2.3 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/3

Here we consider the SCC { f1445_0_aux_LT, f1611_0_aux_InvokeMethod }.

2.3.1 Transition Removal

We remove transitions 10, 12, 11 using the following ranking functions, which are bounded by 0.

2.3.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE

• version: AProVE Commit ID: unknown
• strategy: Statistics for single proof: 100.00 % (11 real / 0 unknown / 0 assumptions / 11 total proof steps)