[Imprint][Data Privacy Statement][E-Mail]

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,

Theorem base summary for Specification Set

SetGInv(0,0)disj-ADoInsert-ARetMember(0,0)disj-AInvMember-tau(0,0)disj-retInsert-retMember(0,0)gstepf-retMember-RETMEMBER(0,0)lstepf-invInsert-DOINSERT(0,0)pre-retInsert(0,0)sel-mkgs-dotset(0,0)upd-mkstate-dotgstate(0,0)updsel--dotlsf-dotlsf(0,0)
SetInv(0,0)disj-ADoInsert-tau(0,0)disj-ARetInsert-ARetMember(0,0)elim-mkgs(0,0)inj-ADoInsert(0,0)lstepf-invMember-DOMEMBER(0,0)pre-retMember(0,0)sel-mkls-dotlb(0,0)upd-mkstate-dotlsf(0,0)updsel--dotlsf-dotpcf(0,0)
SetLInv(0,0)disj-ADoMember-AInvInsert(0,0)disj-ARetInsert-tau(0,0)elim-mkls(0,0)inj-ADoMember(0,0)lstepf-retInsert-RETINSERT(0,0)sel-ADoInsert-dotb(0,0)sel-mkls-dotle(0,0)upd-mkstate-dotpcf(0,0)updsel--dotpcf-dotgstate(0,0)
SetRely(0,0)disj-ADoMember-AInvMember(0,0)disj-ARetMember-tau(0,0)elim-mkstate(0,0)inj-AInvInsert(0,0)lstepf-retMember-RETMEMBER(0,0)sel-ADoInsert-dottid(0,0)sel-mkls-dottid(0,0)updsel--dotgstate-dotgstate(0,0)updsel--dotpcf-dotlsf(0,0)
case-SetAction(0,0)disj-ADoMember-ARetInsert(0,0)disj-idle-invInsert(0,0)gen-SetAction(0,0)inj-AInvMember(0,0)pcstepf-idle-INVINSERT(0,0)sel-ADoMember-dottid(0,0)sel-mkstate-dotgstate(0,0)updsel--dotgstate-dotlsf(0,0)updsel--dotpcf-dotpcf(0,0)
case-SetGState(0,0)disj-ADoMember-ARetMember(0,0)disj-idle-invMember(0,0)gen-SetGState(0,0)inj-ARetInsert(0,0)pcstepf-idle-INVMEMBER(0,0)sel-AInvInsert-dote(0,0)sel-mkstate-dotlsf(0,0)updsel--dotgstate-dotpcf(0,0)updsel--dotset-dotset(0,0)
case-SetLState(0,0)disj-ADoMember-tau(0,0)disj-idle-retInsert(0,0)gen-SetLState(0,0)inj-ARetMember(0,0)pcstepf-invInsert-DOINSERT(0,0)sel-AInvInsert-dottid(0,0)sel-mkstate-dotpcf(0,0)updsel--dotlb-dotlb(0,0)updsel--dottid-dotlb(0,0)
case-SetPC(0,0)disj-AInvInsert-AInvMember(0,0)disj-idle-retMember(0,0)gen-SetPC(0,0)inj-mkgs(0,0)pcstepf-invMember-DOMEMBER(0,0)sel-AInvMember-dote(0,0)setInit(0,0)updsel--dotlb-dotle(0,0)updsel--dottid-dotle(0,0)
case-SetState(0,0)disj-AInvInsert-ARetInsert(0,0)disj-invInsert-invMember(0,0)gen-SetState(0,0)inj-mkls(0,0)pcstepf-retInsert-RETINSERT(0,0)sel-AInvMember-dottid(0,0)setStep(0,0)updsel--dotlb-dottid(0,0)updsel--dottid-dottid(0,0)
disj-ADoInsert-ADoMember(0,0)disj-AInvInsert-ARetMember(0,0)disj-invInsert-retInsert(0,0)gstepf-idle(0,0)inj-mkstate(0,0)pcstepf-retMember-RETMEMBER(0,0)sel-ARetInsert-dotb(0,0)upd-mkgs-dotset(0,0)updsel--dotle-dotlb(0,0)
disj-ADoInsert-AInvInsert(0,0)disj-AInvInsert-tau(0,0)disj-invInsert-retMember(0,0)gstepf-invInsert-DOINSERT(0,0)lstep(0,0)pre-idle(0,0)sel-ARetInsert-dottid(0,0)upd-mkls-dotlb(0,0)updsel--dotle-dotle(0,0)
disj-ADoInsert-AInvMember(0,0)disj-AInvMember-ARetInsert(0,0)disj-invMember-retInsert(0,0)gstepf-invMember-DOMEMBER(0,0)lstepf-idle-INVINSERT(0,0)pre-invInsert(0,0)sel-ARetMember-dotb(0,0)upd-mkls-dotle(0,0)updsel--dotle-dottid(0,0)
disj-ADoInsert-ARetInsert(0,0)disj-AInvMember-ARetMember(0,0)disj-invMember-retMember(0,0)gstepf-retInsert-RETINSERT(0,0)lstepf-idle-INVMEMBER(0,0)pre-invMember(0,0)sel-ARetMember-dottid(0,0)upd-mkls-dottid(0,0)updsel--dotlsf-dotgstate(0,0)