Proof step 63 from proof rg2-lem1-term-unfair (previous step)

User applied rule step

And obtained the following new goals

• Proof step 64:

  □ (N = N' ∧ ¬ N' < N''), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), boolvar ∨ n2 = N0 +1 ∧ N0 = N0'' +1 until Boolvar0, ( ( ( ( ( ( ( ( (((n1 = n16 ∧ (true ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s2)) ∧ ¬ n3 < N) ∧ ¬ R2(pm, s3, S)) ∧ □ ¬ N' < N'' ∨ ( ( (((n1 = n16 ∧ (true ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s2)) ∧ ¬ n3 < N) ∧ ¬ R2(pm, s3, S)) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')) ∨ false ∨ ( ( (((n1 = n16 ∧ (true ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s2)) ∧ ¬ n3 < N) ∧ ¬ R2(pm, s3, S)) ∧ □ ¬ N' < N'' ∧ ◇ last) ∨ ( false ∨ ( ( ((n1 = n16 ∧ (true ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, S)) ∧ ¬ R1(pm, s2, s2)) ∧ ¬ n3 < N) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')) ∨ false ∨ ( ( ((n1 = n16 ∧ (true ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, S)) ∧ ¬ R1(pm, s2, s2)) ∧ ¬ n3 < N) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last) ∨ (∃ s0. (¬ false ∧ (n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ R1(pm, s3, s0)) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s0 ∧ true] ∥nf false ::- [PL □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ]) ∨ ( ( (∃ s0, n, s1. ( ( (((n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s0 ∧ true] ∥nf false ::- [PL (N = n ∧ S = s1) ∧ □ ¬ N' < N'']]) ∨ (∃ s0, n, s1. ( ( (((n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s0 ∧ true] ∥nf false ::- [PL (N = n ∧ S = s1) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]])) ∨ (∃ s0, n, s1. ( ( (((n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s0 ∧ true] ∥nf false ::- [PL (N = n ∧ S = s1) ∧ □ ¬ N' < N'' ∧ ◇ last]])) ∨ ( (∃ s0. false) ∨ (∃ s0, s1, n. ( ( ((n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s0 ∧ true] ∥nf false ::- [PL (S = s1 ∧ N = n) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ])) ∨ (∃ s0, s1, n. ( ( ((n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s0 ∧ true] ∥nf false ::- [PL (S = s1 ∧ N = n) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ])) ∨ (((false ∨ false) ∨ false ∨ false) ∨ (false ∨ false) ∨ false ∨ false) ∨ (¬ false ∧ false) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL true ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ]) ∨ ( (∃ n, s0. (¬ false ∧ (n1 = n16 ∧ n3 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ R1(pm, s3, s0)) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ]) ∨ ( ( (∃ n, s0, n0, s1. ( ( ( ((n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n0) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (N = n0 ∧ S = s1) ∧ □ ¬ N' < N''] ]) ∨ (∃ n, s0, n0, s1. ( ( ( ((n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n0) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (N = n0 ∧ S = s1) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ])) ∨ (∃ n, s0, n0, s1. ( ( ( ((n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n0) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (N = n0 ∧ S = s1) ∧ □ ¬ N' < N'' ∧ ◇ last] ])) ∨ ( (∃ n, s0. false) ∨ (∃ n, s0, s1, n0. ( ( ( (n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n0) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (S = s1 ∧ N = n0) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ])) ∨ (∃ n, s0, s1, n0. ( ( ((n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2))) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ n3 < n0) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (S = s1 ∧ N = n0) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ])) ∨ (∃ n, s0. (¬ false ∧ n1 = n16 ∧ n3 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, s0)) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ]) ∨ ( ( (∃ n, s0, n0, s1. ( ( ( (n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ n3 < n0) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n0 ∧ S = s1) ∧ □ ¬ N' < N''] ]) ∨ (∃ n, s0, n0, s1. ( ( ( (n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ n3 < n0) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n0 ∧ S = s1) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ])) ∨ (∃ n, s0, n0, s1. ( ( ((n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ n3 < n0) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n0 ∧ S = s1) ∧ □ ¬ N' < N'' ∧ ◇ last] ])) ∨ ( (∃ n, s0. false) ∨ (∃ n, s0, s1, n0. ( ( (n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ n3 < n0) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (S = s1 ∧ N = n0) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ])) ∨ (∃ n, s0, s1, n0. ( ( (n1 = n16 ∧ n1 = n + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ n3 < n0) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n ∧ S = s0) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (S = s1 ∧ N = n0) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ])) ∨ ( ( ( ( ( ( (((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n1) ∧ ¬ R2(pm, s2, s2)) ∧ ¬ R1(pm, s3, S) ∨ false) ∨ ( ( (((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = N + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n1) ∧ ¬ R2(pm, s2, s2)) ∧ ¬ R1(pm, s3, S)) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∨ ( ( ((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = N + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, S)) ∧ ¬ n1 < n1) ∧ ¬ R2(pm, s2, s2)) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))) ∨ (∃ n, s0. (¬(boolvar ∨ boolvar0) ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N''] ]) ∨ ( (∃ n, s0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s1 ∧ true] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'']]) ∨ (∃ n, s0. false)) ∨ (∃ n, s0, n0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N''] ]) ∨ (∃ n, s0, n0, s1. ( ( ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, s1)) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N''] ])) ∨ (∃ n, s0. (¬(boolvar ∨ boolvar0) ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ]) ∨ ( (∃ n, s0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s1 ∧ true] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]]) ∨ (∃ n, s0. false)) ∨ (∃ n, s0, n0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ]) ∨ (∃ n, s0, n0, s1. ( ( ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, s1)) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ])) ∨ ( ( ((((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n1) ∧ ¬ R2(pm, s2, s2)) ∧ ¬ R1(pm, s3, S) ∨ false) ∨ ( ( (((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = N + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n1) ∧ ¬ R2(pm, s2, s2)) ∧ ¬ R1(pm, s3, S)) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∨ ( ( ((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = N + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, S)) ∧ ¬ n1 < n1) ∧ ¬ R2(pm, s2, s2)) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))) ∨ (∃ n, s0. (¬(boolvar ∨ boolvar0) ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ◇ last] ]) ∨ ( (∃ n, s0, s1. ( ((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s1 ∧ true] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ◇ last]]) ∨ (∃ n, s0. false)) ∨ (∃ n, s0, n0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ◇ last] ]) ∨ (∃ n, s0, n0, s1. ( ( ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, s1)) ∧ ¬ n1 < n) ∧ ¬ R2(pm, s2, s0)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ◇ last] ])) ∨ ( ( ((false ∨ false) ∨ false ∨ false) ∨ (¬(boolvar ∨ boolvar0) ∧ false) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL true ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ]) ∨ (∃ s0, n. (¬(boolvar ∨ boolvar0) ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s0)) ∧ ¬ n3 < n) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ]) ∨ ( (∃ s0, n, s1. ( ((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s1 ∧ true] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ]) ∨ (∃ s0, n. false)) ∨ (∃ s0, n, n0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ]) ∨ (∃ s0, n, n0, s1. ( ( ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, s1)) ∧ ¬ n1 < n) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ (□ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))) ∧ ¬ □ R2(pm, S', S'')] ])) ∨ ( ( ((((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s2)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n1) ∧ ¬ R1(pm, s3, S) ∨ false) ∨ ( ( (((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = N + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n1) ∧ ¬ R1(pm, s3, S)) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∨ ( ( ((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s2)) ∧ n1 = n16 ∧ n3 = N + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, S)) ∧ ¬ n1 < n1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))) ∨ (∃ s0, n. (¬(boolvar ∨ boolvar0) ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s0)) ∧ ¬ n3 < n) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ]) ∨ ( (∃ s0, n, s1. ( ((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ n1 = n16 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL S = s1 ∧ true] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ]) ∨ (∃ s0, n. false)) ∨ (∃ s0, n, n0, s1. ( ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3))) ∧ ¬ n1 < n) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ]) ∨ (∃ s0, n, n0, s1. ( ( ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ n1 = n16 ∧ n3 = n0 + 1 ∧ (false ⊃ Post1(pm, s, s2);G1(pm, s2, s3)) ∧ R1(pm, s3, s1)) ∧ ¬ n1 < n) ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL (N = n0 ∧ S = s1) ∧ N' = N'' + 1 until ¬ R1(pm, S', S'') ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL (S = s0 ∧ N = n) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ]), (INDHYP-nat(n16 + 1) ∧ INDHYP-nat0(n16 + 1)) ∧ INDHYP-nat1(n2), n1 = n16 + 1, Pre2(pm, s), Pre1(pm, s), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), I(pm, s2), ¬ false, boolvar3 → n1 = n3 ∧ s2 = s3 ∧ (boolvar ↔ boolvar1) ∧ (boolvar0 ↔ boolvar2) ∧ n2 = n4, R1(pm, s3, S), R2(pm, s3, S), n1 = n3, ¬ n3 < N ⊦ ◇ last

Rule argument

Additional information