Proof step 11 from proof rg2-lem1-term-unfair (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 12:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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)] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G1(pm, s2, s3), ¬ R1(pm, s3, s0), ¬ boolvar1 ⊦ ◇ last

• Proof step 16:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s1] ∥nf false ::- [PL N = n ∧ S = s4 ∧ □ ¬ N' < N'']], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s1), ¬ n2 < n, ¬ R2(pm, s3, s4) ⊦ ◇ last

• Proof step 18:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s5] ∥nf false ::- [PL N = n0 ∧ S = s6 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s5), ¬ n2 < n0, ¬ R2(pm, s3, s6) ⊦ ◇ last

• Proof step 20:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s7] ∥nf false ::- [PL N = n1 ∧ S = s8 ∧ □ ¬ N' < N'' ∧ ◇ last]], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s7), ¬ n2 < n1, ¬ R2(pm, s3, s8) ⊦ ◇ last

• Proof step 22:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s10), ¬ R1(pm, s2, s9), ¬ n2 < n3 ⊦ ◇ last

• Proof step 26:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s12), ¬ R1(pm, s2, s11), ¬ n2 < n4 ⊦ ◇ last

• Proof step 30:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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)] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n5 + 1, G1(pm, s2, s3), ¬ R1(pm, s3, s13), ¬ boolvar1 ⊦ ◇ last

• Proof step 34:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL N = n6 ∧ S = s14 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n7 ∧ S = s15 ∧ □ ¬ N' < N'']], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n6 + 1, G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s14), ¬ n6 + 1 < n7, ¬ R2(pm, s3, s15) ⊦ ◇ last

• Proof step 36:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n8 + 1, G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s16), ¬ n8 + 1 < n9, ¬ R2(pm, s3, s17) ⊦ ◇ last

• Proof step 38:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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]], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n10 + 1, G1(pm, s2, s2), G2(pm, s2, s3), ¬ R1(pm, s2, s18), ¬ n10 + 1 < n11, ¬ R2(pm, s3, s19) ⊦ ◇ last

• Proof step 40:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n12 + 1, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s21), ¬ R1(pm, s2, s20), ¬ n12 + 1 < n13 ⊦ ◇ last

• Proof step 44:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n14 + 1, G1(pm, s2, s2), G2(pm, s2, s3), R2(pm, s3, s23), ¬ R1(pm, s2, s22), ¬ n14 + 1 < n15 ⊦ ◇ last

• Proof step 48:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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)] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n16 + 1, G1(pm, s2, s3), R1(pm, s3, s24), ¬ boolvar1 ⊦ ◇ last

• Proof step 102:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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''] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n17 + 1, G1(pm, s2, s2), R1(pm, s2, s25), G2(pm, s2, s3), ¬ n17 + 1 < n18, ¬ R2(pm, s3, s26) ⊦ ◇ last

• Proof step 106:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n19 + 1, G1(pm, s2, s2), R1(pm, s2, s27), G2(pm, s2, s3), ¬ n19 + 1 < n20, ¬ R2(pm, s3, s28) ⊦ ◇ last

• Proof step 110:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n21 + 1, G1(pm, s2, s2), R1(pm, s2, s29), G2(pm, s2, s3), ¬ n21 + 1 < n22, ¬ R2(pm, s3, s30) ⊦ ◇ last

• Proof step 114:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n23 + 1, G1(pm, s2, s2), R1(pm, s2, s31), G2(pm, s2, s3), R2(pm, s3, s32), ¬ n23 + 1 < n24 ⊦ ◇ last

• Proof step 130:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), n2 = n25 + 1, G1(pm, s2, s2), R1(pm, s2, s33), G2(pm, s2, s3), R2(pm, s3, s34), ¬ n25 + 1 < n26 ⊦ ◇ last

• Proof step 146:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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''] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), ¬ boolvar, G2(pm, s2, s3), ¬ n2 < n27, ¬ R2(pm, s3, s35), ¬ boolvar1 ⊦ ◇ last

• Proof step 150:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s37] ∥nf false ::- [PL N = n28 ∧ S = s36 ∧ □ ¬ N' < N'']], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), G1(pm, s2, s3), ¬ n2 < n28, ¬ R2(pm, s2, s36), ¬ R1(pm, s3, s37) ⊦ ◇ last

• Proof step 152:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL N = n30 ∧ S = s39 ∧ N' = N'' + 1 until ¬ R1(pm, S', S'')] ∥nf false ::- [PL N = n29 ∧ S = s38 ∧ □ ¬ N' < N'']], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), n2 = n30 + 1, G1(pm, s2, s3), ¬ n30 + 1 < n29, ¬ R2(pm, s2, s38), ¬ R1(pm, s3, s39) ⊦ ◇ last

• Proof step 154:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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''] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), n2 = n32 + 1, G1(pm, s2, s3), R1(pm, s3, s41), ¬ n32 + 1 < n31, ¬ R2(pm, s2, s40) ⊦ ◇ last

• Proof step 158:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), ¬ boolvar, G2(pm, s2, s3), ¬ n2 < n33, ¬ R2(pm, s3, s42), ¬ boolvar1 ⊦ ◇ last

• Proof step 162:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s44] ∥nf false ::- [PL N = n34 ∧ S = s43 ∧ □ ¬ N' < N'' ∧ ¬ □ R2(pm, S', S'')]], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), G1(pm, s2, s3), ¬ n2 < n34, ¬ R2(pm, s2, s43), ¬ R1(pm, s3, s44) ⊦ ◇ last

• Proof step 164:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), n2 = n36 + 1, G1(pm, s2, s3), ¬ n36 + 1 < n35, ¬ R2(pm, s2, s45), ¬ R1(pm, s3, s46) ⊦ ◇ last

• Proof step 166:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), n2 = n38 + 1, G1(pm, s2, s3), R1(pm, s3, s48), ¬ n38 + 1 < n37, ¬ R2(pm, s2, s47) ⊦ ◇ last

• Proof step 170:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), ¬ boolvar, G2(pm, s2, s3), ¬ n2 < n39, ¬ R2(pm, s3, s49), ¬ boolvar1 ⊦ ◇ last

• Proof step 174:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL S = s51] ∥nf false ::- [PL N = n40 ∧ S = s50 ∧ □ ¬ N' < N'' ∧ ◇ last]], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), G1(pm, s2, s3), ¬ n2 < n40, ¬ R2(pm, s2, s50), ¬ R1(pm, s3, s51) ⊦ ◇ last

• Proof step 176:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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]], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), n2 = n42 + 1, G1(pm, s2, s3), ¬ n42 + 1 < n41, ¬ R2(pm, s2, s52), ¬ R1(pm, s3, s53) ⊦ ◇ last

• Proof step 178:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), n2 = n44 + 1, G1(pm, s2, s3), R1(pm, s3, s55), ¬ n44 + 1 < n43, ¬ R2(pm, s2, s54) ⊦ ◇ last

• Proof step 182:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), ¬ boolvar, G2(pm, s2, s3), R2(pm, s3, s56), ¬ n2 < n45, ¬ boolvar1 ⊦ ◇ last

• Proof step 186:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), R2(pm, s2, s57), G1(pm, s2, s3), ¬ n2 < n46, ¬ R1(pm, s3, s58) ⊦ ◇ last

• Proof step 190:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), R2(pm, s2, s59), n2 = n48 + 1, G1(pm, s2, s3), ¬ n48 + 1 < n47, ¬ R1(pm, s3, s60) ⊦ ◇ last

• Proof step 194:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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'')] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), R2(pm, s2, s61), n2 = n50 + 1, G1(pm, s2, s3), R1(pm, s3, s62), ¬ n50 + 1 < n49 ⊦ ◇ last

• Proof step 210:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), ¬ boolvar, G2(pm, s2, s3), R2(pm, s3, s63), ¬ n2 < n51, ¬ boolvar1 ⊦ ◇ last

• Proof step 214:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), R2(pm, s2, s64), G1(pm, s2, s3), ¬ n2 < n52, ¬ R1(pm, s3, s65) ⊦ ◇ last

• Proof step 218:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), R2(pm, s2, s66), n2 = n54 + 1, G1(pm, s2, s3), ¬ n54 + 1 < n53, ¬ R1(pm, s3, s67) ⊦ ◇ last

• Proof step 222:

  □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [: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] ], □ (N = N' ∧ ¬ N' < N''), boolvar ∨ n2 = N + 1 ∧ N = N'' + 1 until Boolvar, 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), G2(pm, s2, s2), R2(pm, s2, s68), n2 = n56 + 1, G1(pm, s2, s3), R1(pm, s3, s69), ¬ n56 + 1 < n55 ⊦ ◇ last

Rule argument

Additional information