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

Status: Proved!
Axioms: 14, User Theorems: 123 (Proved: 123, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 1174, Interactions: 406

abs-log-adr-explicit-in-leb-notin(5,0)	abs-log-toset-inter-restr-empty(9,3)	down-store-adr-in-explicit(2,1)	in-nodes-down-at-same(15,5)	jnlhd-notin-istore(5,1)	nds-split(10,3)	nodes-ginval-rem(17,6)	prefix-append-prefix(2,0)	restr-add-notin(9,4)	valid-group-nodes-entire(1,1)
abs-log-append-one(4,1)	abs-log-write-last(5,1)	down-store-adr-in-explicit-simp(2,0)	in-nodes-in-gstore(2,0)	key-in-ri-in-fs(2,0)	new-adrs-gstore(8,2)	nodes-ginval-rem-01(17,6)	prefixn-toset-inter-empty(6,1)	restr-empty-notin(5,1)	valid-group-nodes-last-end(4,2)
abs-log-base(0,0)	abs-log-write-nochange(14,1)	down-store-at(0,0)	in-restr-eq-notin-log(2,0)	key-in-update-index(2,0)	new-prefixn(5,1)	nodes-gstore-at(0,0)	prefixn-toset-restr-empty(6,1)	restr-toset-empty-notin(5,1)	valid-group-nodes-last-end-nosimp(3,0)
abs-log-change-other(5,1)	addresses-restr-subseteq0(2,0)	down-store-at-diff(7,3)	in-restr-notin-log(9,3)	keys-append(1,0)	nodes-allocate(21,7)	nodes-gstore-in(0,0)	prefixn-toset-subseteq(7,2)	ri-cons-range-restrict-notin-gstore(10,4)	valid-group-nodes-le(2,0)
abs-log-del(5,0)	adr-in-index-node-key(23,10)	down-store-dealloc(3,2)	in-ri(2,0)	keys-at(9,2)	nodes-append-subseteq(39,14)	nodes-no-change-eq(25,9)	range-in-ri-keys-in-ri(7,3)	ri-cons-subseteq(7,4)	valid-group-nodes-ls(6,1)
abs-log-eq-butlast(4,1)	adr-in-ri-in-gstore(5,1)	down-store-in(0,0)	index-update-adr-in(31,14)	keys-eq-empty(2,0)	nodes-append-subseteq-nodown(28,9)	nodes-referenced-adrs-leb(15,6)	range-rem-in(28,11)	size-0(37,14)	valid-group-nodes-prefixn-append-nonend(5,4)
abs-log-except-refsize(10,4)	adr-in-ri-leb-notin-ginval(5,2)	down-store-notin-notin(10,2)	index-update-append1(2,0)	keys-nodes-in-ri(11,5)	nodes-block-at(0,0)	nodes-remove-ginval-notin(13,4)	refsize-0-notin-index(6,2)	sub-restr-sub(4,2)	valid-group-nodes-rec(0,0)
abs-log-except-refsize-down(3,1)	adr-in-ri-notin-nodes(6,3)	down-store-write(3,1)	index-update-one(1,1)	keys-one(1,1)	nodes-block-in(0,0)	nodes-remove-refsize0(36,14)	refsize-cons-remove(2,0)	toSet-diff-get(2,1)	valid-group-nodes-shorter-prefix(12,3)
abs-log-gcrash-down(20,6)	adresses-restr-subseteq(1,1)	down-store-write-same(1,0)	induction-rev-list(8,4)	keys-remove-leb(15,9)	nodes-crash-down(32,12)	nodes-transaction(43,14)	refsize-nonzero-notin-ginval(11,5)	toSet-diff-in(2,0)	valid-group-nodes-shorter-prefix-right(10,1)
abs-log-new(13,5)	dom-remove-refsize0-down(8,3)	ginval-down(9,2)	insert-subset-old(3,2)	keys-same-fs(41,22)	nodes-dealloc(21,9)	nodes-write-at-other(16,5)	refsize0-addresses(0,0)	valid-group-nodes-app-transaction(9,1)	valid-group-nodes-single-end(1,1)
abs-log-no-change-eq(9,3)	down-block(0,0)	ginval-extract-abs-log(5,1)	inter-notin-add-empty(2,0)	keys-size(1,0)	nodes-empty(1,1)	nodes-write-nochange(16,4)	remove-nonend-inv(0,0)	valid-group-nodes-app-transaction-prefix(11,5)	valid-journal-head-valid-group-nodes(4,1)
abs-log-one(5,3)	down-block-explicit(1,1)	ginval-extract-nodes(11,4)	inter-subset-rem-empty(3,1)	ladr-split(8,3)	nodes-except-refsize(35,14)	nodes-write-same-flushed(29,8)	remove-refsize0-down(9,4)	valid-group-nodes-base(0,0)
abs-log-rec(0,0)	down-empty(1,1)	gstore-dom-eq-hole(16,9)	jnlhd-in-gstore(5,1)	last-notin-butlast-nodups(3,1)	nodes-except-refsize-down(3,1)	notin-down-eq-notin-down(2,0)	restore-log-inv(0,0)	valid-group-nodes-drop(3,1)
abs-log-split-head(2,0)	down-except-refsize(26,9)	in-keys-elim(9,0)	jnlhd-notin-ginval(5,2)	lebs-dom-remove-refsize0(17,8)	nodes-ginval-inter(13,4)	notin-notin-nodes-down(2,0)	restr-add-01(6,0)	valid-group-nodes-drop-superfluous-prefixn(8,1)