[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 2 from proof RG-restr-ok (previous step)

m < n ⊦ n = 0, RG-restr (n, λ n, act, cs, act0, cs0. CRely(m + 1, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs, act0, cs0. CGuar(m + 1, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs. CInit(m + 1, act, cs) ∧ CInv(n, act, cs), λ n, act, cs, act0, cs0. CInv(n, act0, cs0), CInv, λ n, act, cs, act0, cs0. CRelyto(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs, act0, cs0. CGuarto(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs. CInitto(m, act, cs) ∧ CInv(n, act, cs), λ n, act, cs, act0, cs0. CInv(n, act0, cs0))

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 3:
⊦ RG-restr(n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2) ↔ ¬ ¬ ( (∀ act, cs, act4, cs4. (Pre1(n2, act, cs) ∧ R1(n2, act, cs, act4, cs4) → Pre1(n2, act4, cs4)) ∧ (R1(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → IV(n2, act4, cs4)) ∧ (R2(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → IV(n2, act4, cs4)) ∧ (Pre2(n2, act, cs) ∧ R2(n2, act, cs, act4, cs4) → Pre2(n2, act4, cs4)) ∧ (G1(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → R2(n2, act, cs, act4, cs4)) ∧ (G2(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → R1(n2, act, cs, act4, cs4))) ∧ (∀ act, cs, act4, cs4, act5, cs5. (Pre1(n2, act, cs) ∧ Post1(n2, act, cs, act4, cs4) ∧ IV(n2, act4, cs4) ∧ R1(n2, act4, cs4, act5, cs5) → Post1(n2, act, cs, act5, cs5)) ∧ (Pre2(n2, act, cs) ∧ Post2(n2, act, cs, act4, cs4) ∧ IV(n2, act4, cs4) ∧ R2(n2, act4, cs4, act5, cs5) → Post2(n2, act, cs, act5, cs5)) ∧ (R1(n2, act, cs, act4, cs4) ∧ R1(n2, act4, cs4, act5, cs5) ∧ IV(n2, act, cs) → R1(n2, act, cs, act5, cs5)) ∧ (R2(n2, act, cs, act4, cs4) ∧ R2(n2, act4, cs4, act5, cs5) ∧ IV(n2, act, cs) → R2(n2, act, cs, act5, cs5))) ∧ (∀ act, cs. (IV(n2, act, cs) → R1(n2, act, cs, act, cs) ∧ R2(n2, act, cs, act, cs)) ∧ (Pre1(n2, act, cs) → IV(n2, act, cs)) ∧ (Pre2(n2, act, cs) → IV(n2, act, cs))))
Proof step 4:
m < n ⊦ n = 0, (∀ act, cs, act4, cs4. ( (CInit(m + 1, act, cs) ∧ CInv(n, act, cs)) ∧ CRely(m + 1, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4)) → CInit(m + 1, act4, cs4) ∧ CInv(n, act4, cs4)) ∧ ((CRely(m + 1, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ CInv(n, act, cs) → CInv(n, act4, cs4)) ∧ ((CRelyto(m, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ CInv(n, act, cs) → CInv(n, act4, cs4)) ∧ ( (CInitto(m, act, cs) ∧ CInv(n, act, cs)) ∧ CRelyto(m, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4)) → CInitto(m, act4, cs4) ∧ CInv(n, act4, cs4)) ∧ ( (CGuar(m + 1, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ CInv(n, act, cs) → CRelyto(m, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ ( (CGuarto(m, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ CInv(n, act, cs) → CRely(m + 1, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4)))) ∧ (∀ act, cs, act4, cs4, act5, cs5. ( (CInit(m + 1, act, cs) ∧ CInv(n, act, cs)) ∧ CInv(n, act4, cs4) ∧ CInv(n, act4, cs4) ∧ CRely(m + 1, act4, cs4, act5, cs5) ∧ (CInv(n, act4, cs4) → CInv(n, act5, cs5)) → CInv(n, act5, cs5)) ∧ ( (CInitto(m, act, cs) ∧ CInv(n, act, cs)) ∧ CInv(n, act4, cs4) ∧ CInv(n, act4, cs4) ∧ CRelyto(m, act4, cs4, act5, cs5) ∧ (CInv(n, act4, cs4) → CInv(n, act5, cs5)) → CInv(n, act5, cs5)) ∧ ( (CRely(m + 1, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ (CRely(m + 1, act4, cs4, act5, cs5) ∧ (CInv(n, act4, cs4) → CInv(n, act5, cs5))) ∧ CInv(n, act, cs) → CRely(m + 1, act, cs, act5, cs5) ∧ (CInv(n, act, cs) → CInv(n, act5, cs5))) ∧ ( (CRelyto(m, act, cs, act4, cs4) ∧ (CInv(n, act, cs) → CInv(n, act4, cs4))) ∧ (CRelyto(m, act4, cs4, act5, cs5) ∧ (CInv(n, act4, cs4) → CInv(n, act5, cs5))) ∧ CInv(n, act, cs) → CRelyto(m, act, cs, act5, cs5) ∧ (CInv(n, act, cs) → CInv(n, act5, cs5)))) ∧ (∀ act, cs. ( CInv(n, act, cs) → (CRely(m + 1, act, cs, act, cs) ∧ (CInv(n, act, cs) → CInv(n, act, cs))) ∧ CRelyto(m, act, cs, act, cs) ∧ (CInv(n, act, cs) → CInv(n, act, cs))) ∧ (CInit(m + 1, act, cs) ∧ CInv(n, act, cs) → CInv(n, act, cs)) ∧ (CInitto(m, act, cs) ∧ CInv(n, act, cs) → CInv(n, act, cs)))

Rule argument

spec: RG-I-2-Theory inst: RG-I-n-Instance name: RG-restr-def seq: ⊦ RG-restr(n2, R1, G1, Pre1, Post1, IV, R2, G2, Pre2, Post2) ↔ ¬ ¬ ( (∀ act, cs, act4, cs4. ( Pre1(n2, act, cs) ∧ R1(n2, act, cs, act4, cs4) → Pre1(n2, act4, cs4)) ∧ ( R1(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → IV(n2, act4, cs4)) ∧ ( R2(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → IV(n2, act4, cs4)) ∧ ( Pre2(n2, act, cs) ∧ R2(n2, act, cs, act4, cs4) → Pre2(n2, act4, cs4)) ∧ ( G1(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → R2(n2, act, cs, act4, cs4)) ∧ ( G2(n2, act, cs, act4, cs4) ∧ IV(n2, act, cs) → R1(n2, act, cs, act4, cs4))) ∧ (∀ act, cs, act4, cs4, act5, cs5. ( Pre1(n2, act, cs) ∧ Post1(n2, act, cs, act4, cs4) ∧ IV(n2, act4, cs4) ∧ R1(n2, act4, cs4, act5, cs5) → Post1(n2, act, cs, act5, cs5)) ∧ ( Pre2(n2, act, cs) ∧ Post2(n2, act, cs, act4, cs4) ∧ IV(n2, act4, cs4) ∧ R2(n2, act4, cs4, act5, cs5) → Post2(n2, act, cs, act5, cs5)) ∧ ( R1(n2, act, cs, act4, cs4) ∧ R1(n2, act4, cs4, act5, cs5) ∧ IV(n2, act, cs) → R1(n2, act, cs, act5, cs5)) ∧ ( R2(n2, act, cs, act4, cs4) ∧ R2(n2, act4, cs4, act5, cs5) ∧ IV(n2, act, cs) → R2(n2, act, cs, act5, cs5))) ∧ (∀ act, cs. ( IV(n2, act, cs) → R1(n2, act, cs, act, cs) ∧ R2(n2, act, cs, act, cs)) ∧ (Pre1(n2, act, cs) → IV(n2, act, cs)) ∧ (Pre2(n2, act, cs) → IV(n2, act, cs)))) subst: [Post2, Pre2, G2, R2, IV, Post1, Pre1, G1, R1, n2] → [λ n, act, cs, act0, cs0. CInv(n, act0, cs0), λ n, act, cs. CInitto(m, act, cs) ∧ CInv(n, act, cs), λ n, act, cs, act0, cs0. CGuarto(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs, act0, cs0. CRelyto(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), CInv, λ n, act, cs, act0, cs0. CInv(n, act0, cs0), λ n, act, cs. CInit(m + 1, act, cs) ∧ CInv(n, act, cs), λ n, act, cs, act0, cs0. CGuar(m + 1, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs, act0, cs0. CRely(m + 1, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), n] flags: rewrite

Additional information

Used terms: λ n, act, cs, act0, cs0. CInv(n, act0, cs0), λ n, act, cs. CInitto(m, act, cs) ∧ CInv(n, act, cs), λ n, act, cs, act0, cs0. CGuarto(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs, act0, cs0. CRelyto(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), CInv, λ n, act, cs, act0, cs0. CInv(n, act0, cs0), λ n, act, cs. CInit(m + 1, act, cs) ∧ CInv(n, act, cs), λ n, act, cs, act0, cs0. CGuar(m + 1, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), λ n, act, cs, act0, cs0. CRely(m + 1, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0)), n