[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 6 from proof not-pre1-term-unfair (previous step)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 7:
□ (R1(pm, S', S'') ∧ R2(pm, S', S'')), boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, ¬ boolvar ∧ G2(pm, s1, s2) ∧ ¬ R2(pm, s2, s0) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s0]] ∨ ¬ boolvar ∧ G2(pm, s1, s2) ∧ ¬ R2(pm, s2, s3) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s3 ∧ ¬ □ R2(pm, S', S'')]] ∨ ¬ boolvar ∧ G2(pm, s1, s2) ∧ ¬ R2(pm, s2, s4) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s4 ∧ ◇ last]] ∨ ¬ boolvar ∧ G2(pm, s1, s2) ∧ R2(pm, s2, s5) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s5 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ ¬ boolvar ∧ G2(pm, s1, s2) ∧ R2(pm, s2, s6) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s6 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ◇ last]], INDHYP-nat(n), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s1), Pre2(pm, s), R1(pm, s2, S), R2(pm, s2, S), I(pm, s1), I(pm, s), boolvar1 → s1 = s2 ∧ (boolvar ↔ boolvar0) ∧ n = n0 ⊦ ◇ 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);%pre1-i: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ Pre1(pm, s) → I(pm, s);%succ: ⊦ m +1 = m + 1; from specification nat-basic2