[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 9 from proof no-progress-left-aux (previous step)

(P(pm, s2) ∨ false) ∨ n = N + 1 ∧ N = N'' + 1 until (P(pm, S) ∨ last), ( ( (∃ s0. (¬ false ∧ (G1(pm, s2, s3) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s3, s0)) ∧ ¬ boolvar ∧ [:S | [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]]) ∨ (∃ s0, s1. ((((G1(pm, s2, s2) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s2, s0)) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ [PL S = s1 ∧ true]]) ∨ (∃ s0, s1. (((G1(pm, s2, s2) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s2, s0)) ∧ [:S | [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ [PL S = s1 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]])) ∨ (∃ s0. (¬ false ∧ (G1(pm, s2, s3) ∧ R1(pm, s3, s0)) ∧ ¬ P(pm, s2)) ∧ ¬ boolvar ∧ [:S | [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ]) ∨ (∃ s0, s1. ((((G1(pm, s2, s2) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3))) ∧ ¬ P(pm, s2)) ∧ ¬ R2(pm, s3, s1)) ∧ [:S | [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL S = s1 ∧ true]]) ∨ (∃ s0, s1. (((G1(pm, s2, s2) ∧ R1(pm, s2, s0)) ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s1)) ∧ ¬ P(pm, s2)) ∧ [:S | [PL S = s0 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL S = s1 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ])) ∨ ( ( (((((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ G1(pm, s2, s3)) ∧ ¬ R2(pm, s2, s2)) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s3, S)) ∧ □ (¬ P(pm, S) ∧ ¬ last) ∨ ((((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, S)) ∧ ¬ R2(pm, s2, s2)) ∧ ¬ P(pm, s2)) ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')) ∨ (∃ s0. (¬ false ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ boolvar ∧ [:S | [PL □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL S = s0 ∧ true]]) ∨ (∃ s0, s1. (((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ G1(pm, s2, s3)) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ [PL S = s0 ∧ true]]) ∨ (∃ s0, s1. ((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s1)) ∧ ¬ R2(pm, s2, s0)) ∧ ¬ P(pm, s2)) ∧ [:S | [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL S = s0 ∧ true]])) ∨ ( (((((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s2)) ∧ G1(pm, s2, s3)) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s3, S)) ∧ □ (¬ P(pm, S) ∧ ¬ last) ∨ ((((true ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s2)) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, S)) ∧ ¬ P(pm, s2)) ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')) ∨ (∃ s0. (¬ false ∧ (false ⊃ Post2(pm, s, s2);G2(pm, s2, s3)) ∧ R2(pm, s3, s0)) ∧ ¬ boolvar ∧ [:S | [PL □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL S = s0 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ]) ∨ (∃ s0, s1. (((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ G1(pm, s2, s3)) ∧ ¬ P(pm, s2)) ∧ ¬ R1(pm, s3, s1)) ∧ [:S | [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last)] ∥ [PL S = s0 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]]) ∨ (∃ s0, s1. ((((false ⊃ Post2(pm, s, s2);G2(pm, s2, s2)) ∧ R2(pm, s2, s0)) ∧ G1(pm, s2, s3) ∧ R1(pm, s3, s1)) ∧ ¬ P(pm, s2)) ∧ [:S | [PL S = s1 ∧ □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL S = s0 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))] ]), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), \A ∀ N, R1, pm, S, R2, P, G1, Post2, s, G2, Pre1, Post1, I, Pre2. N < m → □ (R1(pm, S', S'') ∧ R2(pm, S', S'')) ∧ [:S | [PL □ (¬ P(pm, S) ∧ ¬ last) ∧ R1(pm, S', S'') -+-> G1(pm, S, S')] ∥ [PL R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]] ∧ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ stable(pm, I, R1) ∧ stable(pm, I, R2) ∧ I(pm, S) ∧ Pre1(pm, s) ∧ Pre2(pm, s) ∧ P-restr(pm, P, I, R1) → ¬ N = N'' +1 until (P(pm, S) ∨ last), m = n, RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), stable(pm, I, R1), stable(pm, I, R2), I(pm, s2), Pre1(pm, s), Pre2(pm, s), P-restr(pm, P, I, R1), ¬ P(pm, s2), ¬ false, boolvar → s2 = s3 ∧ n = n0, R1(pm, s3, S), R2(pm, s3, S) ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information