LTS Termination Proof

by T2Cert

Input

Integer Transition System

Transitions: (pre-variables and post-variables)

0	0	1:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + a_1 ≤ 0 ∧ −1 − a_1 ≤ 0 ∧ −1 + ret_returnOne2_post ≤ 0 ∧ 1 − ret_returnOne2_post ≤ 0 ∧ a_post − ret_returnOne2_post ≤ 0 ∧ − a_post + ret_returnOne2_post ≤ 0 ∧ a_0 − a_post ≤ 0 ∧ − a_0 + a_post ≤ 0 ∧ ret_returnOne2_0 − ret_returnOne2_post ≤ 0 ∧ − ret_returnOne2_0 + ret_returnOne2_post ≤ 0
2	1	0:		− ret_returnOne2_post + ret_returnOne2_post ≤ 0 ∧ ret_returnOne2_post − ret_returnOne2_post ≤ 0 ∧ − ret_returnOne2_0 + ret_returnOne2_0 ≤ 0 ∧ ret_returnOne2_0 − ret_returnOne2_0 ≤ 0 ∧ − a_post + a_post ≤ 0 ∧ a_post − a_post ≤ 0 ∧ − a_1 + a_1 ≤ 0 ∧ a_1 − a_1 ≤ 0 ∧ − a_0 + a_0 ≤ 0 ∧ a_0 − a_0 ≤ 0

The following invariants are asserted.

0:	TRUE
1:	−1 + a_post ≤ 0 ∧ −1 + ret_returnOne2_post ≤ 0 ∧ 1 − ret_returnOne2_post ≤ 0 ∧ 1 + a_1 ≤ 0 ∧ −1 − a_1 ≤ 0 ∧ −1 + a_0 ≤ 0 ∧ −1 + ret_returnOne2_0 ≤ 0 ∧ 1 − ret_returnOne2_0 ≤ 0
2:	TRUE

The invariants are proved as follows.

nodes (location) invariant:

0	(0)	TRUE
1	(1)	−1 + a_post ≤ 0 ∧ −1 + ret_returnOne2_post ≤ 0 ∧ 1 − ret_returnOne2_post ≤ 0 ∧ 1 + a_1 ≤ 0 ∧ −1 − a_1 ≤ 0 ∧ −1 + a_0 ≤ 0 ∧ −1 + ret_returnOne2_0 ≤ 0 ∧ 1 − ret_returnOne2_0 ≤ 0
2	(2)	TRUE

We consider the following cutpoint-transitions:

and for every transition t, a duplicate t is considered.

We remove transitions 0, 1 using the following ranking functions, which are bounded by −8.

There exist no SCC in the program graph.

T2Cert