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

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:
diff-02provedall subs proved diff-20,
diff-03provedall subs proved diff-16,
diff-04provedall subs proved diff-12,
diff-05provedall subs proved diff-08,
diff-06provedall subs proved diff-21,
diff-07provedall subs proved diff-17,
diff-09provedall subs proved diff-13,
diff-10provedall subs proved diff-18,
diff-11provedall subs proved diff-15,
diff-14provedall subs proved diff-19,
eqbytevalprovedall subs proved byteval, test-36, sel-08,
refvalprovedall subs proved refva-sel,
diff-20provedall subs proved test-102, test-101, test-30, test-26, test-32, test-82, test-07, test-170, test-199, test-198, test-197, test-290, test-23, test-24, test-29, test-28, test-33, test-25, test-01, gen,
diff-16provedall subs proved test-129, test-128, test-127, test-126, test-125, test-124, test-122, test-172, test-205, test-204, test-203, test-292, test-121, test-96, test-37, test-95, test-81, test-80, test-123, gen,
diff-12provedall subs proved test-106, test-105, test-51, test-42, test-135, test-84, test-22, test-174, test-211, test-210, test-209, test-294, test-41, test-13, test-14, test-134, test-133, test-15, test-03, gen,
diff-08provedall subs proved test-104, test-103, test-38, test-34, test-132, test-83, test-16, test-173, test-208, test-207, test-206, test-293, test-18, test-40, test-19, test-131, test-130, test-20, test-02, gen,
diff-21provedall subs proved test-102, test-101, test-30, test-26, test-32, test-82, test-07, test-170, test-199, test-198, test-197, test-290, test-23, test-24, test-29, test-28, test-20, test-25, test-01, gen,
diff-17provedall subs proved test-129, test-128, test-127, test-126, test-125, test-124, test-122, test-172, test-205, test-204, test-203, test-292, test-121, test-96, test-131, test-95, test-81, test-80, test-123, gen,
diff-13provedall subs proved test-106, test-105, test-51, test-42, test-135, test-84, test-22, test-174, test-211, test-210, test-209, test-294, test-18, test-13, test-14, test-134, test-133, test-15, test-03, gen,
diff-18provedall subs proved test-102, test-101, test-30, test-26, test-32, test-82, test-07, test-170, test-199, test-198, test-197, test-290, test-23, test-24, test-29, test-28, test-15, test-25, test-01, gen,
diff-15provedall subs proved test-129, test-128, test-127, test-126, test-125, test-124, test-122, test-172, test-205, test-204, test-203, test-292, test-121, test-96, test-134, test-95, test-81, test-80, test-123, gen,
diff-19provedall subs proved test-102, test-101, test-30, test-26, test-32, test-82, test-07, test-170, test-199, test-198, test-197, test-290, test-23, test-24, test-29, test-28, test-80, test-25, test-01, gen,
bytevalprovedall subs proved elim-03,
refva-selprovedall subs proved elim-13,
typevalprovedall subs proved elim-10,
shortval-selprovedall subs proved elim-07,
intvalprovedall subs proved elim-02,
inj-strongprovedall subs proved inj-01,
eqtypevalprovedall subs proved elim-10, sel-11,
eqrefval-01provedall subs proved elim-13, test-19, sel-09,
eqrefvalprovedall subs proved elim-13, test-19, sel-09,
elim-refvalprovedall subs proved elim-13, sel-09,
diff-01provedall subs proved test-114, test-120, test-119, test-27, test-31, test-169, test-100, test-12, test-196, test-289, test-288, test-287, test-324, test-75, test-74, test-168, test-167, test-73, test-77, gen,
diffprovedall subs proved test-118, ex-12,
concat-red-01provedall subs proved inj-01,
concat-redprovedall subs proved inj-01,
elim-07axiom
elim-02axiom
sel-11axiom
elim-10axiom
sel-08axiom
test-36axiom
sel-09axiom
elim-13axiom
test-33axiom
test-01axiom
test-25axiom
test-28axiom
test-29axiom
test-24axiom
test-23axiom
test-290axiom
test-197axiom
test-198axiom
test-199axiom
test-170axiom
test-07axiom
test-82axiom
test-32axiom
test-26axiom
test-30axiom
test-101axiom
test-102axiom
test-37axiom
test-123axiom
test-80axiom
test-81axiom
test-95axiom
test-96axiom
test-121axiom
test-292axiom
test-203axiom
test-204axiom
test-205axiom
test-172axiom
test-122axiom
test-124axiom
test-125axiom
test-126axiom
test-127axiom
test-128axiom
test-129axiom
test-03axiom
test-15axiom
test-133axiom
test-134axiom
test-14axiom
test-13axiom
test-41axiom
test-294axiom
test-209axiom
test-210axiom
test-211axiom
test-174axiom
test-22axiom
test-84axiom
test-135axiom
test-42axiom
test-51axiom
test-105axiom
test-106axiom
test-02axiom
test-20axiom
test-130axiom
test-131axiom
test-19axiom
test-40axiom
test-18axiom
test-293axiom
test-206axiom
test-207axiom
test-208axiom
test-173axiom
test-16axiom
test-83axiom
test-132axiom
test-34axiom
test-38axiom
test-103axiom
test-104axiom
genaxiom
test-77axiom
test-73axiom
test-167axiom
test-168axiom
test-74axiom
test-75axiom
test-324axiom
test-287axiom
test-288axiom
test-289axiom
test-196axiom
test-12axiom
test-100axiom
test-169axiom
test-31axiom
test-27axiom
test-119axiom
test-120axiom
test-114axiom
ex-12axiom
test-118axiom
inj-01axiom
elim-03axiom