[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-lem2-term-unfair (previous step)

□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N0 +1 ∧ N0 = N0'' +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)) ∧ ¬ n3 < 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)) ∧ ¬ n3 < 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)) ∧ ¬ n3 < 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)) ∧ ¬ n3 < 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)) ∧ ¬ n3 < N) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last) ∨ ( ( ( ((((true ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s2)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ n3 < N) ∧ ¬ R2(pm, s3, S)) ∧ □ ¬ N' < N'' ∨ ( ((((true ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s2)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ n3 < N) ∧ ¬ R2(pm, s3, S)) ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')) ∨ false ∨ ( ((((true ⊃ Post1(pm, s, s2);G1(pm, s2, s2)) ∧ R1(pm, s2, s2)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ n3 < N) ∧ ¬ R2(pm, s3, S)) ∧ □ ¬ N' < N'' ∧ ◇ last) ∨ ( false ∨ ((((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)) ∧ ¬ n3 < 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)) ∧ R1(pm, s2, s2)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, S)) ∧ ¬ n3 < N) ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last) ∨ ( (∃ n, s0. (¬ false ∧ (n3 = 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 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 = 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 | 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 = 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 | 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 = 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 | 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 = 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 | 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 = 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 | 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 ∧ n3 = 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 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 = 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 | 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 = 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 | 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 = 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 | 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 = 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 | 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 = 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 | 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)) ∧ 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 last ∨ ( (((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ 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 last ∧ 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)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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)) ∧ n3 = 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 last] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'']]) ∨ (∃ n, s0, n0, s1. ( ( ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n3 = 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 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 ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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)) ∧ n3 = 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 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)) ∧ n3 = 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 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)) ∧ 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 last ∨ ( (((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ 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 last ∧ 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)) ∧ ¬ n3 < n) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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)) ∧ n3 = 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 last] ∥nf false ::- [PL (N = n ∧ S = s0) ∧ □ ¬ N' < N'' ∧ ◇ last]]) ∨ (∃ n, s0, n0, s1. ( (((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ n3 = 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 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 ∧ false) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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 ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s0)) ∧ ¬ n3 < n) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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)) ∧ n3 = 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 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)) ∧ n3 = 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 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)) ∧ n3 = 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)) ∧ n3 = 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 ∧ ((false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s0)) ∧ ¬ n3 < n) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL 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)) ∧ n3 = 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 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)) ∧ n3 = 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 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(n1) ∧ INDHYP-nat0(n2), 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 = n3 ∧ (boolvar ↔ boolvar0) ∧ n2 = n4, n1 = n3, ¬ n3 < 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 = N0 + 1 ∧ N0 = N0'' + 1 until Boolvar, n3 = n + 1 ∧ G1(pm, s2, s3) ∧ ¬ R1(pm, s3, s0) ∧ ¬ boolvar1 ∧ [:S | 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)] ] ∨ n3 = n0 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s1) ∧ ¬ n0 + 1 < n1 ∧ ¬ R2(pm, s3, s4) ∧ [:S | Boolvar ::- [PL N = n0 ∧ S = s1 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL N = n1 ∧ S = s4 ∧ □ ¬ N' < N'']] ∨ n3 = n5 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s5) ∧ ¬ n5 + 1 < n6 ∧ ¬ R2(pm, s3, s6) ∧ [:S | Boolvar ::- [PL N = n5 ∧ S = s5 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL N = n6 ∧ S = s6 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]] ∨ n3 = n7 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ ¬ R1(pm, s2, s7) ∧ ¬ n7 + 1 < n8 ∧ ¬ R2(pm, s3, s8) ∧ [:S | Boolvar ::- [PL N = n7 ∧ S = s7 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL N = n8 ∧ S = s8 ∧ □ ¬ N' < N'' ∧ ◇ last]] ∨ n3 = n9 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s10) ∧ ¬ R1(pm, s2, s9) ∧ ¬ n9 + 1 < n10 ∧ [:S | Boolvar ::- [PL N = n9 ∧ S = s9 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL S = s10 ∧ N = n10 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ n3 = n11 + 1 ∧ G1(pm, s2, s2) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s12) ∧ ¬ R1(pm, s2, s11) ∧ ¬ n11 + 1 < n12 ∧ [:S | Boolvar ::- [PL N = n11 ∧ S = s11 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL S = s12 ∧ N = n12 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ n3 = n13 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s13) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N = n13 ∧ S = s13 ∧ 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)] ] ∨ n3 = n14 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s14) ∧ G2(pm, s2, s3) ∧ ¬ n14 + 1 < n15 ∧ ¬ R2(pm, s3, s15) ∧ [:S | Boolvar ::- [PL N = n14 ∧ S = s14 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n15 ∧ S = s15 ∧ □ ¬ N' < N''] ] ∨ n3 = n16 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s16) ∧ G2(pm, s2, s3) ∧ ¬ n16 + 1 < n17 ∧ ¬ R2(pm, s3, s17) ∧ [:S | Boolvar ::- [PL N = n16 ∧ S = s16 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n17 ∧ S = s17 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ n3 = n18 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s18) ∧ G2(pm, s2, s3) ∧ ¬ n18 + 1 < n19 ∧ ¬ R2(pm, s3, s19) ∧ [:S | Boolvar ::- [PL N = n18 ∧ S = s18 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n19 ∧ S = s19 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ n3 = n20 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s20) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s21) ∧ ¬ n20 + 1 < n21 ∧ [:S | Boolvar ::- [PL N = n20 ∧ S = s20 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s21 ∧ N = n21 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ n3 = n22 + 1 ∧ G1(pm, s2, s2) ∧ R1(pm, s2, s22) ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s23) ∧ ¬ n22 + 1 < n23 ∧ [:S | Boolvar ::- [PL N = n22 ∧ S = s22 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s23 ∧ N = n23 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ n3 < n24 ∧ ¬ R2(pm, s3, s24) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n24 ∧ S = s24 ∧ □ ¬ N' < N''] ] ∨ G2(pm, s2, s2) ∧ n3 = n26 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n26 + 1 < n25 ∧ ¬ R2(pm, s2, s25) ∧ ¬ R1(pm, s3, s26) ∧ [:S | Boolvar ::- [PL N = n26 ∧ S = s26 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL N = n25 ∧ S = s25 ∧ □ ¬ N' < N'']] ∨ G2(pm, s2, s2) ∧ n3 = n28 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s28) ∧ ¬ n28 + 1 < n27 ∧ ¬ R2(pm, s2, s27) ∧ [:S | Boolvar ::- [PL N = n28 ∧ S = s28 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n27 ∧ S = s27 ∧ □ ¬ N' < N''] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ n3 < n29 ∧ ¬ R2(pm, s3, s29) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n29 ∧ S = s29 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ G2(pm, s2, s2) ∧ n3 = n31 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n31 + 1 < n30 ∧ ¬ R2(pm, s2, s30) ∧ ¬ R1(pm, s3, s31) ∧ [:S | Boolvar ::- [PL N = n31 ∧ S = s31 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL N = n30 ∧ S = s30 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]] ∨ G2(pm, s2, s2) ∧ n3 = n33 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s33) ∧ ¬ n33 + 1 < n32 ∧ ¬ R2(pm, s2, s32) ∧ [:S | Boolvar ::- [PL N = n33 ∧ S = s33 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n32 ∧ S = s32 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ ¬ n3 < n34 ∧ ¬ R2(pm, s3, s34) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n34 ∧ S = s34 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ n3 = n36 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n36 + 1 < n35 ∧ ¬ R2(pm, s2, s35) ∧ ¬ R1(pm, s3, s36) ∧ [:S | Boolvar ::- [PL N = n36 ∧ S = s36 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL N = n35 ∧ S = s35 ∧ □ ¬ N' < N'' ∧ ◇ last]] ∨ G2(pm, s2, s2) ∧ n3 = n38 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s38) ∧ ¬ n38 + 1 < n37 ∧ ¬ R2(pm, s2, s37) ∧ [:S | Boolvar ::- [PL N = n38 ∧ S = s38 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL N = n37 ∧ S = s37 ∧ □ ¬ N' < N'' ∧ ◇ last] ] ∨ ¬ boolvar ∧ G2(pm, s2, s3) ∧ R2(pm, s3, s39) ∧ ¬ n3 < n39 ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s39 ∧ N = n39 ∧ □ ¬ 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, s40) ∧ n3 = n41 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n41 + 1 < n40 ∧ ¬ R1(pm, s3, s41) ∧ [:S | Boolvar ::- [PL N = n41 ∧ S = s41 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL S = s40 ∧ N = n40 ∧ □ ¬ 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, s42) ∧ n3 = n43 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s43) ∧ ¬ n43 + 1 < n42 ∧ [:S | Boolvar ::- [PL N = n43 ∧ S = s43 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s42 ∧ N = n42 ∧ □ ¬ 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, s44) ∧ ¬ n3 < n44 ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s44 ∧ N = n44 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s45) ∧ n3 = n46 + 1 ∧ G1(pm, s2, s3) ∧ ¬ n46 + 1 < n45 ∧ ¬ R1(pm, s3, s46) ∧ [:S | Boolvar ::- [PL N = n46 ∧ S = s46 ∧ N' = N'' + 1 until last] ∥nf false ::- [PL S = s45 ∧ N = n45 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ] ∨ G2(pm, s2, s2) ∧ R2(pm, s2, s47) ∧ n3 = n48 + 1 ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s48) ∧ ¬ n48 + 1 < n47 ∧ [:S | Boolvar ::- [PL N = n48 ∧ S = s48 ∧ N' = N'' + 1 until last ∧ R1(pm, S', S'') -+-> (last ⊃ Post1(pm, s, S);G1(pm, S, S'))] ∥nf false ::- [PL S = s47 ∧ N = n47 ∧ □ ¬ N' < N'' ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last] ], INDHYP-nat(n3) ∧ 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 ≤ n3, I(pm, s), boolvar1 → s2 = s3 ∧ (boolvar ↔ boolvar0) ∧ n2 = n4 ⊦ ◇ 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