[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-never-violates-left-rely (previous step)

□ (CRelyto(n + 1, Act', CS', Act'', CS'') ∧ CInv(n0, Act', CS') ∧ CInv(n0, Act'', CS'')), [:Act, CS | [PL Act = act ∧ CS = 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(cs1), 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, act0, cs0), CRely(n + 1, act0, cs0, Act, CS), CInv(n0, Act, CS), n < n0, ¬ CRely(n + 1, act0, cs0, act, cs) ∨ ¬ CInv(n0, act, cs), ∀ n. Idle(n, cs1) ⊦

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), Pre2(n2, act5, cs5), IV(n2, act4, cs4), □ (R1(n2, Act4', CS4', Act4'', CS4'') ∧ R2(n2, Act4', CS4', Act4'', CS4'')), [:Act4, CS4 | [PL Act4 = act ∧ CS4 = cs] ∥ [PL R2(n2, Act4', CS4', Act4'', CS4'') -+-> (last ⊃ Post2(n2, act5, cs5, Act4, CS4);G2(n2, Act4, CS4, Act4', CS4'))] ], ¬ R1(n2, act4, cs4, act, cs), R1(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 Act = act ∧ CS = 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(cs1), 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, act0, cs0), CRely(n + 1, act0, cs0, Act, CS), CInv(n0, Act, CS), n < n0, ¬ CRely(n + 1, act0, cs0, act, cs) ∨ ¬ CInv(n0, act, cs), ∀ n. Idle(n, cs1) ⊦ CInitto(n, λ n. false, cs1) ∧ CInv(n0, λ n. false, cs1) ∧ □ ( (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''))) ∧ ¬(CRely(n + 1, act0, cs0, act, cs) ∧ (CInv(n0, act0, cs0) → CInv(n0, act, cs))) ∧ (CInv(n0, act0, cs0) → CInv(n0, Act, CS))

Rule argument

spec: RG-I-2-Theory inst: RG-I-n-Instance name: fair-never-violates-left-rely seq: RG-restr(n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2), Pre2(n2, act5, cs5), IV(n2, act4, cs4), □ ( R1(n2, Act4', CS4', Act4'', CS4'') ∧ R2(n2, Act4', CS4', Act4'', CS4'')), [:Act4, CS4 | [PL Act4 = act ∧ CS4 = cs] ∥ [PL R2(n2, Act4', CS4', Act4'', CS4'') -+-> (last ⊃ Post2(n2, act5, cs5, Act4, CS4) ;G2(n2, Act4, CS4, Act4', CS4') ) ] ], ¬ R1(n2, act4, cs4, act, cs), R1(n2, act4, cs4, Act4, CS4) ⊦ subst: [n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2, act5, cs5, act4, cs4, Act4, CS4, act, cs] → [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, cs1, act0, cs0, Act, 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, cs1, act0, cs0, Act, CS, act, cs