[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 11 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, 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

User applied rule case distinction

And obtained the following new goals

Rule argument

pos: left 4

Additional information