[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 51 from proof CSEQ-sat-rely-guar (previous step)

INDHYP-nat(n0 + 1), m ≤ n, act(m), CInv(n, act, cs), ¬ false, boolvar → n0 = n1 ∧ act = act0 ∧ cs = cs0 ∧ outp = outp0 ∧ inp = inp0 ⊦ ( ( ( (true ⊃ CInv(n, act, cs) ∧ Idle(m, cs) ∧ act(m);CGuar(m, act, cs, act, cs) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act, cs) ∧ act(m))) ∧ ¬(CRely(m, act, cs, act, cs) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act, cs) ∧ act(m)))) ∧ true → ( (act0 = (act(m; false)) ∧ outp = outp0 ∧ cs = cs0 ∧ inp = inp0) ∧ ¬ boolvar ∧ ¬ false → CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0))) ∧ ( (act0 = (act(m; false)) ∧ outp = outp0 ∧ cs = cs0 ∧ inp = inp0) ∧ ¬ boolvar ∧ ¬ false ∧ CGuar(m, act, cs, act0, cs0) ∧ (CRely(m, act0, cs0, Act, CS) ∧ n0 = N + 1) ∧ (CInv(n, act0, cs0) → CInv(n, Act, CS)) → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star ] CInv(n, Act, CS))) ∧ ( ( (false ⊃ CInv(n, act, cs) ∧ Idle(m, cs) ∧ act(m) ;CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act0, cs0) ∧ act0(m)) ) ∧ ¬(CRely(m, act0, cs0, Act, CS) ∧ (CInv(n, act0, cs0) ∧ act0(m) → CInv(n, Act, CS) ∧ Act(m)))) ∧ true → CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0))) ∧ ( ( ( (false ⊃ CInv(n, act, cs) ∧ Idle(m, cs) ∧ act(m) ;CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act0, cs0) ∧ act0(m)) ) ∧ ¬(CRely(m, act0, cs0, Act, CS) ∧ (CInv(n, act0, cs0) ∧ act0(m) → CInv(n, Act, CS) ∧ Act(m)))) ∧ true) ∧ CGuar(m, act, cs, act0, cs0) ∧ (CRely(m, act0, cs0, Act, CS) ∧ n0 = N + 1) ∧ (CInv(n, act0, cs0) → CInv(n, Act, CS)) → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , {[PL true]; Act(m) := false; { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star} ] CInv(n, Act, CS))) ∧ ( ( (true ⊃ CInv(n, act, cs) ∧ Idle(m, cs) ∧ act(m);CGuar(m, act, cs, act, cs) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act, cs) ∧ act(m))) ∧ CRely(m, act, cs, act, cs) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act, cs) ∧ act(m))) ∧ true → ( (act0 = (act(m; false)) ∧ outp = outp0 ∧ cs = cs0 ∧ inp = inp0) ∧ ¬ boolvar ∧ ¬ false → CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0))) ∧ ( (act0 = (act(m; false)) ∧ outp = outp0 ∧ cs = cs0 ∧ inp = inp0) ∧ ¬ boolvar ∧ ¬ false ∧ CGuar(m, act, cs, act0, cs0) ∧ (CRely(m, act0, cs0, Act, CS) ∧ n0 = N + 1) ∧ (CInv(n, act0, cs0) → CInv(n, Act, CS)) → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star ] CInv(n, Act, CS))) ∧ ( ( (false ⊃ CInv(n, act, cs) ∧ Idle(m, cs) ∧ act(m) ;CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act0, cs0) ∧ act0(m)) ) ∧ CRely(m, act0, cs0, Act, CS) ∧ (CInv(n, act0, cs0) ∧ act0(m) → CInv(n, Act, CS) ∧ Act(m))) ∧ true → CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) → CInv(n, act0, cs0))) ∧ ( ( ( (false ⊃ CInv(n, act, cs) ∧ Idle(m, cs) ∧ act(m) ;CGuar(m, act, cs, act0, cs0) ∧ (CInv(n, act, cs) ∧ act(m) → CInv(n, act0, cs0) ∧ act0(m)) ) ∧ CRely(m, act0, cs0, Act, CS) ∧ (CInv(n, act0, cs0) ∧ act0(m) → CInv(n, Act, CS) ∧ Act(m))) ∧ true) ∧ CGuar(m, act, cs, act0, cs0) ∧ (CRely(m, act0, cs0, Act, CS) ∧ n0 = N + 1) ∧ (CInv(n, act0, cs0) → CInv(n, Act, CS)) → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , {[PL (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false; { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star} ] CInv(n, Act, CS))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 52:
INDHYP-nat(n0 + 1), m ≤ n, act(m), CInv(n, act, cs), boolvar → n0 = n1 ∧ act = act0 ∧ cs = cs0 ∧ outp = outp0 ∧ inp = inp0 ⊦ ( CInv(n, act0, cs0) ∧ act0(m) ∧ ¬ Act(m) ∧ CGuar(m, act, cs, act0, cs0) ∧ CRely(m, act0, cs0, Act, CS) ∧ n0 = N + 1 ∧ CInv(n, Act, CS) → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , {Act(m) := false; { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star} ] CInv(n, Act, CS)) ∧ ( Idle(m, cs) ∧ CRely(m, act, cs, act, cs) → ( act0 = (act(m; false)) ∧ outp = outp0 ∧ cs = cs0 ∧ inp = inp0 ∧ ¬ boolvar → CGuar(m, act, cs0, act(m; false), cs0) ∧ CInv(n, act(m; false), cs0)) ∧ ( act0 = (act(m; false)) ∧ outp = outp0 ∧ cs = cs0 ∧ inp = inp0 ∧ ¬ boolvar ∧ CGuar(m, act, cs0, act(m; false), cs0) ∧ CRely(m, act(m; false), cs0, Act, CS) ∧ n0 = N + 1 ∧ (CInv(n, act(m; false), cs0) → CInv(n, Act, CS)) → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star ] CInv(n, Act, CS))) ∧ ( CInv(n, act0, cs0) ∧ act0(m) ∧ CInv(n, Act, CS) ∧ Act(m) ∧ CGuar(m, act, cs, act0, cs0) ∧ CRely(m, act0, cs0, Act, CS) ∧ n0 = N + 1 → [: Act, Inp, CS, Outp | (CRely(m, Act', CS', Act'', CS'') ∧ N = N'' + 1) , CGuar(m, Act, CS, Act', CS') , CInv(n, Act, CS) , {[PL (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false; { skip or {Act(m) := true; [PL CInv(n, Act, CS) ∧ Act(m) ∧ m ≤ n ∧ Idle(m, CS) → (CRely(m, Act', CS', Act'', CS'') ∧ (CInv(n, Act', CS') ∧ Act'(m) → CInv(n, Act'', CS'') ∧ Act''(m))) -+-> (last ⊃ CInv(n, Act, CS) ∧ Idle(m, CS) ∧ Act(m) ;CGuar(m, Act, CS, Act', CS') ∧ (CInv(n, Act, CS) ∧ Act(m) → CInv(n, Act', CS') ∧ Act'(m)) ) ]; Act(m) := false}} star} ] CInv(n, Act, CS))

Rule argument

Additional information

Used simplifier rules: CRely-refl: ⊦ CInv(n, act, cs) → (¬ CRely(m, act, cs, act, cs) ↔ false);