[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 46 from proof rg2-lem2-term-unfair (previous step)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 47:
□ (N = N' ∧ ¬ N' < N''), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), boolvar ∨ n3 = N0 + 1 ∧ N0 = N0'' + 1 until Boolvar0, ¬ boolvar ∧ ¬ boolvar0 ∧ G2(pm, s2, s3) ∧ ¬ n13 + 1 < n ∧ ¬ R2(pm, s3, s0) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n13 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n ∧ S = s0 ∧ □ ¬ N' < N''] ] ∨ ¬ boolvar ∧ ¬ boolvar0 ∧ G2(pm, s2, s3) ∧ ¬ n13 + 1 < n0 ∧ ¬ R2(pm, s3, s1) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n13 ∧ N' = N'' + 1 until last ∧ 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'')] ] ∨ ¬ boolvar ∧ ¬ boolvar0 ∧ G2(pm, s2, s3) ∧ ¬ n13 + 1 < n1 ∧ ¬ R2(pm, s3, s4) ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n13 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n1 ∧ S = s4 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ ¬ boolvar ∧ ¬ boolvar0 ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s5) ∧ ¬ n13 + 1 < n4 ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n13 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s5 ∧ N = n4 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ ¬ boolvar ∧ ¬ boolvar0 ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s6) ∧ ¬ n13 + 1 < n6 ∧ ¬ boolvar3 ∧ [:S | Boolvar0 ∨ Boolvar ::- [PL N = n13 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s6 ∧ N = n6 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ], (INDHYP-nat(n13 + 1) ∧ INDHYP-nat0(n2)) ∧ INDHYP-nat1(n3), Pre2(pm, s), Pre1(pm, s), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), N ≤ n13 + 1, I(pm, s), boolvar3 → s2 = s3 ∧ (boolvar ↔ boolvar1) ∧ (boolvar0 ↔ boolvar2) ∧ n3 = n5 ⊦ ◇ last

Rule argument

Additional information

Used simplifier rules: pre2-i: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ Pre2(pm, s) → I(pm, s);%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%eq: ⊦ m = m + n ↔ n = 0; from specification nat-basic2%succ: ⊦ m +1 = m + 1; from specification nat-basic2%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat