[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 address-set-array-ops
Status:
Proved!
Axioms: 3, User Theorems: 17 (Proved: 17, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 125, Interactions: 39
disj(0,0)
disj-unique(2,0)
in-union-ext(12,4)
subseteq-union-one-add(2,1)
union-subset(12,5)
disj-in-both(5,1)
disj-write(19,3)
inter-union-empty-one-empty(7,2)
union-base(0,0)
union-union-one(1,0)
disj-rec(6,2)
in-index-in-union(7,2)
subseteq-union-diff-one(8,3)
union-eq-rem-subseteq(7,2)
union-write(17,7)
disj-union-rem(9,3)
in-index-in-union-1(5,1)
subseteq-union-one(2,1)
union-rec(0,0)
union-write-above(4,2)