[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,

Lemma dependency for Specification VF3conc

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
step-L1-L7provedall subs proved disj-58, disj-13, pcstepf-L1,
rely-L5-L6provedall subs proved gstepf-L5, pre-L5, pcstepf-L5,
step-L1-L8provedall subs proved gstepf-L1, lstepf-L1, pre-L1, disj-57, pcstepf-L1,
step-L6-L7provedall subs proved alltids-all, elim-02, elim-03, lstepf-L6, updsel-54, gstepf-L6, updsel-41, updsel-42, updsel-35, updsel-36, updsel-23, updsel-24, updsel-47, updsel-48, updsel-29, updsel-30, pre-L6, disj-16, pcstepf-L6,
rely-L6-L7provedall subs proved updsel-29, updsel-30, gstepf-L6, updsel-54, pre-L6, disj-16, pcstepf-L6,
rely-L6-L3provedall subs proved gstepf-L6, pre-L6, disj-16, pcstepf-L6,
step-L7-L3provedall subs proved updsel-14, lstepf-L7, gstepf-L7, updsel-11, pre-L7, pcstepf-L7,
rely-L2-L1provedall subs proved disj-07, gstepf-L2-0, inj-04, inj-07, upd-12, sel-09, upd-05, sel-08, sel-16, upd-08, sel-12, gstepf-L2-1, elim-02, elim-03, pre-L2, disj-35, pcstepf-L2,
step-L2-L1provedall subs proved disj-07, lstepf-L2-0, gstepf-L2-0, inj-04, updsel-11, lstepf-L2-1, inj-07, upd-12, updsel-14, sel-16, upd-08, sel-12, gstepf-L2-1, elim-03, pre-L2, disj-35, pcstepf-L2,
rely-L2-L3provedall subs proved updsel-26, updsel-30, updsel-14, updsel-11, gstepf-L2-1, updsel-54, disj-07, inj-04, pre-L2, disj-35, pcstepf-L2,
step-L2-L3provedall subs proved alltids-all, elim-02, elim-03, updsel-14, lstepf-L2-1, updsel-54, updsel-11, gstepf-L2-1, updsel-38, updsel-42, updsel-32, updsel-36, updsel-20, updsel-24, updsel-44, updsel-48, updsel-26, updsel-30, disj-07, inj-04, pre-L2, disj-35, pcstepf-L2,
step-L3-L1provedall subs proved gstepf-L3, lstepf-L3, pre-L3, disj-37, pcstepf-L3,
step-L3-L4provedall subs proved lstepf-L3, gstepf-L3, pre-L3, disj-37, pcstepf-L3,
step-L6-L3provedall subs proved lstepf-L6, gstepf-L6, pre-L6, disj-16, pcstepf-L6,
step-L4-L0provedall subs proved disj-08, inj-03, elim-02, elim-03, pre-L4, disj-26, pcstepf-L4,
step-L4-L5provedall subs proved updsel-15, lstepf-L4-0, updsel-12, updsel-18, disj-08, inj-03, gstepf-L4, pre-L4, disj-26, pcstepf-L4,
step-L5-L6provedall subs proved updsel-56, lstepf-L5, gstepf-L5, updsel-55, updsel-57, pre-L5, pcstepf-L5,
step-L1-L2provedall subs proved gstepf-L1, lstepf-L1, pre-L1, disj-57, pcstepf-L1,
initprovedall subs proved alltids-all,
disj-13axiom
disj-58axiom
updsel-47axiom
updsel-23axiom
updsel-35axiom
updsel-41axiom
updsel-29axiom
pcstepf-L7axiom
pre-L7axiom
gstepf-L7axiom
lstepf-L7axiom
sel-08axiom
upd-05axiom
sel-09axiom
sel-12axiom
upd-08axiom
sel-16axiom
upd-12axiom
inj-07axiom
gstepf-L2-0axiom
lstepf-L2-0axiom
pcstepf-L2axiom
disj-35axiom
pre-L2axiom
inj-04axiom
disj-07axiom
updsel-30axiom
updsel-26axiom
updsel-48axiom
updsel-44axiom
updsel-24axiom
updsel-20axiom
updsel-36axiom
updsel-32axiom
updsel-42axiom
updsel-38axiom
gstepf-L2-1axiom
updsel-11axiom
updsel-54axiom
lstepf-L2-1axiom
updsel-14axiom
pcstepf-L3axiom
disj-37axiom
pre-L3axiom
gstepf-L3axiom
lstepf-L3axiom
pcstepf-L6axiom
disj-16axiom
pre-L6axiom
gstepf-L6axiom
lstepf-L6axiom
elim-03axiom
elim-02axiom
pcstepf-L4axiom
disj-26axiom
pre-L4axiom
gstepf-L4axiom
inj-03axiom
disj-08axiom
updsel-18axiom
updsel-12axiom
lstepf-L4-0axiom
updsel-15axiom
pcstepf-L5axiom
pre-L5axiom
updsel-57axiom
updsel-55axiom
gstepf-L5axiom
lstepf-L5axiom
updsel-56axiom
pcstepf-L1axiom
disj-57axiom
pre-L1axiom
lstepf-L1axiom
gstepf-L1axiom
alltids-allaxiom