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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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

Rule argument

Additional information

Used simplifier rules: r1-trans: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s, s0) ∧ R1(pm, s0, s1) ∧ I(pm, s) → R1(pm, s, s1);%pre2-i: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ Pre2(pm, s) → I(pm, s);%pre1-r1: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R1(pm, s, s0) ∧ Pre1(pm, s) → Pre1(pm, s0);%pre1-i: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ Pre1(pm, s) → I(pm, s);%i-r2-i: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ R2(pm, s, s0) ∧ I(pm, s) → I(pm, s0);%g2-r1: ⊦ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ G2(pm, s, s0) ∧ I(pm, s) → R1(pm, s, s0);