[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 for Specification bnat

This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.

Name:	Sequent:	Type:
add-def	⊦ bm +b bn = (bm.toNat + bn.toNat).toBNat	An Axiom
le-def	⊦ bm ≤b bn ↔ bn.toNat ≤ bm.toNat	An Axiom
toNat-toBNat-inv	m ≤ MAX_Nat ⊦ m.toBNat.toNat = m	An Axiom
ls-def	⊦ bm <b bn ↔ bm.toNat < bn.toNat	An Axiom
bounded	⊦ bm.toNat ≤ MAX_Nat	An Axiom
gen	BNat generated by toBNat;	An Axiom
toBNat-toNat-def	⊦ bm.toNat.toBNat = bm	An Axiom
sub-def	⊦ bm -b bn = (bm.toNat - bn.toNat).toBNat	An Axiom
gr-def	⊦ bm >b bn ↔ bn.toNat > bm.toNat	An Axiom
ge-def	⊦ bm ≥b bn ↔ bm ≤b bn	An Axiom
elim-toNat	⊦ m = bm.toNat ↔ bm = m.toBNat ∧ m ≤ MAX_Nat	A User Theorem