[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 14 from proof fair-always-right-relyinv (previous step)

□ (CRelyto(n + 1, Act', CS', Act'', CS'') ∧ CInv(n0, Act', CS') ∧ CInv(n0, Act'', CS'')), [:Act, CS | [PL (CRely(n + 1, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuar(n + 1, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ∥ [PL ◇ (¬ CRelyto(n, Act', CS', Act'', CS'') ∨ ¬(CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) ∧ (CRelyto(n, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuarto(n, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ], n0 ≠ 0, Init(cs), RG-restr (n0, λ n0, act, cs, act0, cs0. CRely(n + 1, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs, act0, cs0. CGuar(n + 1, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs. CInit(n + 1, act, cs) ∧ CInv(n0, act, cs), λ n, act, cs, act0, cs0. CInv(n, act0, cs0), CInv, λ n0, act, cs, act0, cs0. CRelyto(n, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs, act0, cs0. CGuarto(n, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs. CInitto(n, act, cs) ∧ CInv(n0, act, cs), λ n, act, cs, act0, cs0. CInv(n, act0, cs0)), CInv(n0, Act, CS), n < n0, ∀ n. Idle(n, cs) ⊦ CInit(n + 1, λ n. false, cs) ∧ CInv(n0, λ n. false, cs) ∧ CInitto(n, λ n. false, cs) ∧ CInv(n0, λ n. false, cs) ∧ □ ( (CRely(n + 1, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) ∧ CRelyto(n, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) ∧ [:Act, CS | [PL (CRely(n + 1, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuar(n + 1, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ∥ [PL ◇ ¬(CRelyto(n, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) ∧ (CRelyto(n, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuarto(n, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ]

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 15:
□ (CRelyto(n + 1, Act', CS', Act'', CS'') ∧ CInv(n0, Act', CS') ∧ CInv(n0, Act'', CS'')), [:Act, CS | [PL (CRely(n + 1, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuar(n + 1, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ∥ [PL ◇ (¬ CRelyto(n, Act', CS', Act'', CS'') ∨ ¬(CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) ∧ (CRelyto(n, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuarto(n, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ], n0 ≠ 0, Init(cs), RG-restr (n0, λ n0, act, cs, act0, cs0. CRely(n + 1, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs, act0, cs0. CGuar(n + 1, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs. CInit(n + 1, act, cs) ∧ CInv(n0, act, cs), λ n, act, cs, act0, cs0. CInv(n, act0, cs0), CInv, λ n0, act, cs, act0, cs0. CRelyto(n, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs, act0, cs0. CGuarto(n, act, cs, act0, cs0) ∧ (CInv(n0, act, cs) → CInv(n0, act0, cs0)), λ n0, act, cs. CInitto(n, act, cs) ∧ CInv(n0, act, cs), λ n, act, cs, act0, cs0. CInv(n, act0, cs0)), CInv(n0, Act, CS), n < n0, ∀ n. Idle(n, cs) ⊦ CInit(n + 1, λ n. false, cs) ∧ CInitto(n, λ n. false, cs) ∧ CInv(n0, λ n. false, cs) ∧ [:Act, CS | [PL (CRely(n + 1, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuar(n + 1, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ∥ [PL ◇ (¬ CRelyto(n, Act', CS', Act'', CS'') ∨ ¬(CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) ∧ (CRelyto(n, Act', CS', Act'', CS'') ∧ (CInv(n0, Act', CS') → CInv(n0, Act'', CS''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuarto(n, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ]

Rule argument

Additional information

Used simplifier rules: CRelytosucc-CRely: ⊦ CRelyto(m + 1, act, cs, act0, cs0) → (¬ CRely(m + 1, act, cs, act0, cs0) ↔ false);%CRelytosucc-CRelyto: ⊦ CRelyto(m + 1, act, cs, act0, cs0) → (¬ CRelyto(m, act, cs, act0, cs0) ↔ false);%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2