[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 12 from proof fair-always-left-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''))) ∧ (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''))) -+-> (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) ⊦

User applied rule insert spec-lemma

And obtained the following new goals

Proof step 13:
RG-restr(n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2), Pre1(n2, act, cs), Pre2(n2, act, cs), IV(n2, Act4, CS4), □ (R1(n2, Act4', CS4', Act4'', CS4'') ∧ R2(n2, Act4', CS4', Act4'', CS4'')), [:Act4, CS4 | [PL ◇ ¬ R1(n2, Act4', CS4', Act4'', CS4'') ∧ R1(n2, Act4', CS4', Act4'', CS4'') -+-> (last ⊃ Post1(n2, act, cs, Act4, CS4);G1(n2, Act4, CS4, Act4', CS4')) ] ∥ [PL R2(n2, Act4', CS4', Act4'', CS4'') -+-> (last ⊃ Post2(n2, act, cs, Act4, CS4);G2(n2, Act4, CS4, Act4', CS4'))] ] ⊦
Proof step 14:
□ (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''))) ∧ (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''))) -+-> (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''))) ∧ (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''))) -+-> (last ⊃ CInv(n0, Act, CS);CGuarto(n, Act, CS, Act', CS') ∧ (CInv(n0, Act, CS) → CInv(n0, Act', CS'))) ] ]

Rule argument

spec: RG-I-2-Theory inst: RG-I-n-Instance name: fair-always-left-rely seq: RG-restr(n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2), Pre1(n2, act, cs), Pre2(n2, act, cs), IV(n2, Act4, CS4), □ ( R1(n2, Act4', CS4', Act4'', CS4'') ∧ R2(n2, Act4', CS4', Act4'', CS4'')), [:Act4, CS4 | [PL ◇ ¬ R1(n2, Act4', CS4', Act4'', CS4'') ∧ R1(n2, Act4', CS4', Act4'', CS4'') -+-> (last ⊃ Post1(n2, act, cs, Act4, CS4) ;G1(n2, Act4, CS4, Act4', CS4') ) ] ∥ [PL R2(n2, Act4', CS4', Act4'', CS4'') -+-> (last ⊃ Post2(n2, act, cs, Act4, CS4) ;G2(n2, Act4, CS4, Act4', CS4') ) ] ] ⊦ subst: [n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2, act, cs, Act4, CS4] → [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), λ n. false, cs, Act, CS] flags: []

Additional information

Used terms: 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), λ n. false, cs, Act, CS