LTS Termination Proof

by T2Cert

Input

• Initial Location: 10
• Transitions: (pre-variables and post-variables)

  0	0	1:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x6 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
  0	2	3:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x18 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − x19 ≤ 0 ∧ 1 − arg2 + x19 ≤ 0 ∧ − x20 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0
  1	4	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 + x26 ≤ 0 ∧ 1 − x26 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − x34 ≤ 0 ∧ 2 − arg4P ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ 3 − arg1 + arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg3 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0
  1	5	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 + x36 ≤ 0 ∧ 1 − x36 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − x44 ≤ 0 ∧ 2 − arg4P ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 4 − arg2P ≤ 0 ∧ 4 − arg3P ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg3 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0
  0	6	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ −1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
  0	7	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x52 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − x50 ≤ 0 ∧ 1 − arg2 + x50 ≤ 0 ∧ − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg3P + x50 ≤ 0 ∧ −1 + arg3P − x50 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
  1	8	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 + x54 ≤ 0 ∧ 1 − x54 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg3 ≤ 0 ∧ 1 − arg3P + x54 ≤ 0 ∧ −1 + arg3P − x54 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
  6	9	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2 ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg2 + arg3 ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 0 ∧ arg2 − arg4P ≤ 0 ∧ − arg2 + arg4P ≤ 0 ∧ 1 + arg3 − arg5P ≤ 0 ∧ −1 − arg3 + arg5P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
  7	10	6:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg2 − arg3 ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 0 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ − arg2P + arg4 ≤ 0 ∧ arg2P − arg4 ≤ 0 ∧ − arg3P + arg5 ≤ 0 ∧ arg3P − arg5 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0
  7	11	7:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg2 − arg3 ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
  5	12	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 1 − arg1 + arg6P ≤ 0 ∧ 1 − arg2 + arg7P ≤ 0 ∧ 1 − arg3 + arg7P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg6P ≤ 0 ∧ − arg7P ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3P ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0
  5	13	8:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 1 − arg1 + arg6P ≤ 0 ∧ 1 − arg2 + arg7P ≤ 0 ∧ 1 − arg3 + arg7P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg6P ≤ 0 ∧ − arg7P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ −1 + arg3P ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0
  8	14	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg1P − arg2 ≤ 0 ∧ arg1P − arg7 ≤ 0 ∧ 1 − arg1 + arg2P ≤ 0 ∧ arg2P − arg6 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg6 ≤ 0 ∧ − arg7 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ −1 + arg3 ≤ 0 ∧ − arg3P + arg4 ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0
  9	15	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 + arg1P − arg2 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ 2 − arg1 + arg2P ≤ 0 ∧ 3 + arg2P − arg2 ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 3 − arg2 + arg3P ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0
  9	16	5:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 + arg1P − arg2 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ 2 − arg1 + arg2P ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0
  9	17	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 + arg1P − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ 2 + arg2P − arg2 ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0
  9	18	9:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 + arg1P − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ 2 + arg2P − arg2 ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0
  10	19	0:		0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

The invariants are proved as follows.

IMPACT Invariant Proof

• nodes (location) invariant:

  0		(0)		TRUE
  1		(1)		4 − arg1P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − x6 ≤ 0
  3		(3)		1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − x18 ≤ 0 ∧ 1 − x19 ≤ 0 ∧ − x20 ≤ 0
  5		(5)		− arg1P ≤ 0 ∧ − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ − x6 ≤ 0
  6		(6)		TRUE
  7		(7)		− arg3P ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ − arg3 ≤ 0
  8		(8)		1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg6P ≤ 0 ∧ − arg7P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg6 ≤ 0 ∧ − arg7 ≤ 0 ∧ − x6 ≤ 0
  9		(9)		− arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − x6 ≤ 0
  10		(10)		TRUE

• initial node: 10
• cover edges:
• transition edges:

  0	0 1
  0	2 3
  0	6 6
  0	7 6
  1	4 5
  1	5 5
  1	8 6
  5	12 8
  5	13 8
  6	9 7
  7	10 6
  7	11 7
  8	14 9
  9	15 5
  9	16 5
  9	17 9
  9	18 9
  10	19 0

2 Switch to Cooperation Termination Proof

3 Transition Removal

We remove transitions 0, 2, 4, 5, 6, 7, 8, 19 using the following ranking functions, which are bounded by −23.

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

5* 23 5: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

5 21 5_var_snapshot: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

6* 30 6: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

7 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

6 28 6_var_snapshot: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

8 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

7* 37 7: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

9 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

7 35 7_var_snapshot: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

10 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

9* 44 9: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

11 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

9 42 9_var_snapshot: − x6 + x6 ≤ 0 ∧ x6 − x6 ≤ 0 ∧ − x54 + x54 ≤ 0 ∧ x54 − x54 ≤ 0 ∧ − x52 + x52 ≤ 0 ∧ x52 − x52 ≤ 0 ∧ − x50 + x50 ≤ 0 ∧ x50 − x50 ≤ 0 ∧ − x44 + x44 ≤ 0 ∧ x44 − x44 ≤ 0 ∧ − x36 + x36 ≤ 0 ∧ x36 − x36 ≤ 0 ∧ − x34 + x34 ≤ 0 ∧ x34 − x34 ≤ 0 ∧ − x26 + x26 ≤ 0 ∧ x26 − x26 ≤ 0 ∧ − x20 + x20 ≤ 0 ∧ x20 − x20 ≤ 0 ∧ − x19 + x19 ≤ 0 ∧ x19 − x19 ≤ 0 ∧ − x18 + x18 ≤ 0 ∧ x18 − x18 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

12 SCC Decomposition

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

12.1 SCC Subproblem 1/2

Here we consider the SCC { 5, 8, 9, 5_var_snapshot, 5*, 9_var_snapshot, 9* }.

12.1.1 Transition Removal

We remove transitions 21, 23, 42, 44, 12, 13, 14, 15, 16, 17, 18 using the following ranking functions, which are bounded by −1.

12.1.2 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

12.1.2.1 Cut-Point Subproblem 1/2

12.1.2.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

12.1.2.2 Cut-Point Subproblem 2/2

12.1.2.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

12.2 SCC Subproblem 2/2

Here we consider the SCC { 6, 7, 6_var_snapshot, 6*, 7_var_snapshot, 7* }.

12.2.1 Transition Removal

We remove transitions 9, 10 using the following ranking functions, which are bounded by 9.

12.2.2 Transition Removal

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

12.2.3 Transition Removal

We remove transitions 28, 35, 37 using the following ranking functions, which are bounded by −1.

12.2.4 Splitting Cut-Point Transitions

We consider 2 subproblems corresponding to sets of cut-point transitions as follows.

12.2.4.1 Cut-Point Subproblem 1/2

12.2.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

12.2.4.2 Cut-Point Subproblem 2/2

12.2.4.2.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert

• version: 1.0