[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 gjournal-base

at-write-at(11,5)index-update-dom(1,1)key-cons-ext(14,5)keys-one(3,3)lebs-in-ri-in-gstore-explicit(8,3)nds-app(3,0)range-add-explicit(2,0)referenced-adrs-lookup-keys-lookup(9,4)ri-inj-index-update(27,14)transaction-prefix-is-transaction-prefix(44,9)
at-write-other(2,0)index-update-range(17,9)key-cons-one(3,3)keys-rec(0,0)lebs-index(0,0)nds-base(0,0)range-del-in(15,6)referenced-adrs-lookup-keys-nodups(21,10)transaction(0,0)transaction-prefix-last-nonend(14,3)
except-refsizeeq-valid-head(8,2)inos-dom(7,3)key-cons-rec(0,0)keys-rec-01(0,0)lebs-lookup-subseteq(13,5)nds-eq-empty(2,0)range-empty(1,0)referenced-adrs-nodups(7,2)transaction-empty(1,0)valid-journal-head(0,0)
flashsize-app(3,0)inos-empty(2,1)keys-app(3,0)keys-rec-full(1,1)lebs-range(1,1)nds-eq-one(6,0)range-write-in(23,10)referenced-adrs-one(3,3)transaction-empty-right(1,0)valid-journal-head-emptylog(2,0)
flashsize-node(0,0)inos-greater-del(7,2)keys-base(0,0)keys-rem(1,1)lebs-rec(0,0)nds-length(1,0)range-write-notin(3,1)referenced-adrs-rec(0,0)transaction-last-nend(2,0)
flashsize-nodes-base(0,0)inos-greater-notin(5,1)keys-base-01(0,0)keys-split(12,4)lebs-rem-subseteq(11,3)nds-one(1,1)referenced-adrs-app(3,0)referenced-adrs-split(18,6)transaction-length(2,0)
flashsize-nodes-rec(0,0)inos-greater-rem(7,2)keys-empty(6,3)ladrlist-to-adr-split(21,4)lebs-set(0,0)nds-rec(0,0)referenced-adrs-base(0,0)referenced-adrs-split-one(20,4)transaction-length0(2,0)
flashsize-one(3,3)inos-node-store-def(0,0)keys-eq-one(4,2)lebs-base(0,0)lebs-write(22,8)new-inter-empty(3,1)referenced-adrs-eq-one-lookup(5,1)referenced-adrs-subseteq-range(1,1)transaction-prefix(0,0)
in-data-explicit(2,0)inos-write(5,1)keys-in(4,2)lebs-del-subseteq(11,3)lebs-write-subseteq(13,4)nodes-cons(0,0)referenced-adrs-in(23,0)refsize-cons-crash(17,8)transaction-prefix-app(31,8)
in-index-in-range(2,0)key-cons(0,0)keys-inodekey-in(9,5)lebs-del-subseteq-set(11,3)lebs-write-subseteq0(15,5)nodes-cons-rec(23,6)referenced-adrs-inter-empty(7,2)refsize-cons-in-ri-0(11,4)transaction-prefix-app-last(43,9)
in-rem-keys-in-data(3,1)key-cons-app(12,0)keys-inodekeys(12,6)lebs-empty(2,1)natset-ls-add-max-ls(11,3)nodes-cons-write-app(30,7)referenced-adrs-lookup-key-cons(9,4)restrict-in-empty(5,1)transaction-prefix-app-nonlast(51,12)
in-write(1,1)key-cons-base(0,0)keys-len(1,0)lebs-in-ri-in-gstore(9,2)natset-ls-max-ls(6,2)nodes-cons-write-other(20,5)referenced-adrs-lookup-keys-in-dom(9,4)restrict-range-notin-lebs(3,1)transaction-prefix-empty(1,0)