[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 10 from proof rg2-lem1-term-unfair (previous step)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 11:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, G1(pm, s2, s3) ∧ ¬ R1(pm, s3, s0) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL S = s0] ∥nf false ::- [PL □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ (□ R2(pm, S', S'') → ◇ last)] ] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s1) ∧ ¬ n2 < n ∧ ¬ R2(pm, s3, s4) ∧ [:S | Boolvar ::- [PL S = s1] ∥nf false ::- [PL N = n ∧ S = s4 ∧ □ ¬ N' < N'']] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s5) ∧ ¬ n2 < n0 ∧ ¬ R2(pm, s3, s6) ∧ [:S | Boolvar ::- [PL S = s5] ∥nf false ::- [PL N = n0 ∧ S = s6 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s7) ∧ ¬ n2 < n1 ∧ ¬ R2(pm, s3, s8) ∧ [:S | Boolvar ::- [PL S = s7] ∥nf false ::- [PL N = n1 ∧ S = s8 ∧ □ ¬ N' < N'' ∧ ◇ last]] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s10) ∧ ¬ R1(pm, s2, s9) ∧ ¬ n2 < n3 ∧ [:S | Boolvar ::- [PL S = s9] ∥nf false ::- [PL S = s10 ∧ N = n3 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s12) ∧ ¬ R1(pm, s2, s11) ∧ ¬ n2 < n4 ∧ [:S | Boolvar ::- [PL S = s11] ∥nf false ::- [PL S = s12 ∧ N = n4 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ n2 = n5 + 1 ∧ G1(pm, s2, s3) ∧ ¬ R1(pm, s3, s13) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N = n5 ∧ S = s13 ∧ 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)] ] ∨ n2 = n6 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s14) ∧ ¬ n6 + 1 < n7 ∧ ¬ R2(pm, s3, s15) ∧ [:S | Boolvar ::- [PL N = n6 ∧ S = s14 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n7 ∧ S = s15 ∧ □ ¬ N' < N'']] ∨ n2 = n8 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s16) ∧ ¬ n8 + 1 < n9 ∧ ¬ R2(pm, s3, s17) ∧ [:S | Boolvar ::- [PL N = n8 ∧ S = s16 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n9 ∧ S = s17 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ n2 = n10 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s18) ∧ ¬ n10 + 1 < n11 ∧ ¬ R2(pm, s3, s19) ∧ [:S | Boolvar ::- [PL N = n10 ∧ S = s18 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n11 ∧ S = s19 ∧ □ ¬ N' < N'' ∧ ◇ last]] ∨ n2 = n12 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s21) ∧ ¬ R1(pm, s2, s20) ∧ ¬ n12 + 1 < n13 ∧ [:S | Boolvar ::- [PL N = n12 ∧ S = s20 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL S = s21 ∧ N = n13 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ n2 = n14 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s23) ∧ ¬ R1(pm, s2, s22) ∧ ¬ n14 + 1 < n15 ∧ [:S | Boolvar ::- [PL N = n14 ∧ S = s22 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL S = s23 ∧ N = n15 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ n2 = n16 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s24) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N = n16 ∧ S = s24 ∧ 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)] ] ∨ n2 = n17 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s25) ∧ G2(pm, s2, s3) ∧ ¬ n17 + 1 < n18 ∧ ¬ R2(pm, s3, s26) ∧ [:S | Boolvar ::- [PL N = n17 ∧ S = s25 ∧ 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 = n18 ∧ S = s26 ∧ □ ¬ N' < N''] ] ∨ n2 = n19 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s27) ∧ G2(pm, s2, s3) ∧ ¬ n19 + 1 < n20 ∧ ¬ R2(pm, s3, s28) ∧ [:S | Boolvar ::- [PL N = n19 ∧ S = s27 ∧ 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 = n20 ∧ S = s28 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ n2 = n21 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s29) ∧ G2(pm, s2, s3) ∧ ¬ n21 + 1 < n22 ∧ ¬ R2(pm, s3, s30) ∧ [:S | Boolvar ::- [PL N = n21 ∧ S = s29 ∧ 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 = n22 ∧ S = s30 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ n2 = n23 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s31) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s32) ∧ ¬ n23 + 1 < n24 ∧ [:S | Boolvar ::- [PL N = n23 ∧ S = s31 ∧ 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 = s32 ∧ N = n24 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ n2 = n25 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s33) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s34) ∧ ¬ n25 + 1 < n26 ∧ [:S | Boolvar ::- [PL N = n25 ∧ S = s33 ∧ 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 = s34 ∧ N = n26 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ n2 < n27 ∧ ¬ R2(pm, s3, s35) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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 = n27 ∧ S = s35 ∧ □ ¬ N' < N''] ] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ ¬ n2 < n28 ∧ ¬ R2(pm, s2, s36) ∧ ¬ R1(pm, s3, s37) ∧ [:S | Boolvar ::- [PL S = s37] ∥nf false ::- [PL N = n28 ∧ S = s36 ∧ □ ¬ N' < N'']] ∨ G2(pm, s2, s2) ∧ n2 = n30 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n30 + 1 < n29 ∧ ¬ R2(pm, s2, s38) ∧ ¬ R1(pm, s3, s39) ∧ [:S | Boolvar ::- [PL N = n30 ∧ S = s39 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n29 ∧ S = s38 ∧ □ ¬ N' < N'']] ∨ G2(pm, s2, s2) ∧ n2 = n32 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s41) ∧ ¬ n32 + 1 < n31 ∧ ¬ R2(pm, s2, s40) ∧ [:S | Boolvar ::- [PL N = n32 ∧ S = s41 ∧ 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 = n31 ∧ S = s40 ∧ □ ¬ N' < N''] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ n2 < n33 ∧ ¬ R2(pm, s3, s42) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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 = n33 ∧ S = s42 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ ¬ n2 < n34 ∧ ¬ R2(pm, s2, s43) ∧ ¬ R1(pm, s3, s44) ∧ [:S | Boolvar ::- [PL S = s44] ∥nf false ::- [PL N = n34 ∧ S = s43 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]] ∨ G2(pm, s2, s2) ∧ n2 = n36 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n36 + 1 < n35 ∧ ¬ R2(pm, s2, s45) ∧ ¬ R1(pm, s3, s46) ∧ [:S | Boolvar ::- [PL N = n36 ∧ S = s46 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n35 ∧ S = s45 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ G2(pm, s2, s2) ∧ n2 = n38 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s48) ∧ ¬ n38 + 1 < n37 ∧ ¬ R2(pm, s2, s47) ∧ [:S | Boolvar ::- [PL N = n38 ∧ S = s48 ∧ 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 = n37 ∧ S = s47 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ n2 < n39 ∧ ¬ R2(pm, s3, s49) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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 = n39 ∧ S = s49 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ G1(pm, s2, s3) ∧ ¬ n2 < n40 ∧ ¬ R2(pm, s2, s50) ∧ ¬ R1(pm, s3, s51) ∧ [:S | Boolvar ::- [PL S = s51] ∥nf false ::- [PL N = n40 ∧ S = s50 ∧ □ ¬ N' < N'' ∧ ◇ last]] ∨ G2(pm, s2, s2) ∧ n2 = n42 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n42 + 1 < n41 ∧ ¬ R2(pm, s2, s52) ∧ ¬ R1(pm, s3, s53) ∧ [:S | Boolvar ::- [PL N = n42 ∧ S = s53 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n41 ∧ S = s52 ∧ □ ¬ N' < N'' ∧ ◇ last]] ∨ G2(pm, s2, s2) ∧ n2 = n44 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s55) ∧ ¬ n44 + 1 < n43 ∧ ¬ R2(pm, s2, s54) ∧ [:S | Boolvar ::- [PL N = n44 ∧ S = s55 ∧ 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 = n43 ∧ S = s54 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s56) ∧ ¬ n2 < n45 ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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 = s56 ∧ N = n45 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s57) ∧ G1(pm, s2, s3) ∧ ¬ n2 < n46 ∧ ¬ R1(pm, s3, s58) ∧ [:S | Boolvar ::- [PL S = s58] ∥nf false ::- [PL S = s57 ∧ N = n46 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s59) ∧ n2 = n48 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n48 + 1 < n47 ∧ ¬ R1(pm, s3, s60) ∧ [:S | Boolvar ::- [PL N = n48 ∧ S = s60 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL S = s59 ∧ N = n47 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s61) ∧ n2 = n50 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s62) ∧ ¬ n50 + 1 < n49 ∧ [:S | Boolvar ::- [PL N = n50 ∧ S = s62 ∧ 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 = s61 ∧ N = n49 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s63) ∧ ¬ n2 < n51 ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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 = s63 ∧ N = n51 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s64) ∧ G1(pm, s2, s3) ∧ ¬ n2 < n52 ∧ ¬ R1(pm, s3, s65) ∧ [:S | Boolvar ::- [PL S = s65] ∥nf false ::- [PL S = s64 ∧ N = n52 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s66) ∧ n2 = n54 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n54 + 1 < n53 ∧ ¬ R1(pm, s3, s67) ∧ [:S | Boolvar ::- [PL N = n54 ∧ S = s67 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL S = s66 ∧ N = n53 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s68) ∧ n2 = n56 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s69) ∧ ¬ n56 + 1 < n55 ∧ [:S | Boolvar ::- [PL N = n56 ∧ S = s69 ∧ 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 = s68 ∧ N = n55 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ], INDHYP-nat(n2) ∧ INDHYP-nat0(n2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s), Pre2(pm, s), I(pm, s2), R1(pm, s3, S), R2(pm, s3, S), N ≤ n2, I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ⊦ ◇ 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%l: ⊦ m + n < m + n0 ↔ n < n0; from specification nat-basic2%le-ls-simp: ⊦ m ≤ n → (n < m ↔ false); from specification nat%succ: ⊦ m +1 = m + 1; from specification nat-basic2%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat