[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 monotone-set-fixpoint
Status:
Proved!
Axioms: 7, User Theorems: 16 (Proved: 16, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 113, Interactions: 70
compl-def(0,0)
fixpoint-nu(9,7)
monotone-def(0,0)
prefixpoint-aux(4,2)
subset-trans(9,3)
compl-inverse(4,4)
greatest-prefixpoint-def(0,0)
mu-is-IS(3,3)
prefixpoint-aux-nu(5,3)
subseteq-def(0,0)
compl-monotone(18,10)
intersection-def(0,0)
mu-subset-nu(3,2)
prefixpoint-aux2(8,4)
union-def(0,0)
eq-bothsubset(8,5)
least-fixpoint(4,3)
nu-is-UN(24,14)
prefixpoint-rev(4,3)
fixpoint(4,3)
least-prefixpoint-def(0,0)
prefixpoint(5,3)
subset-refl(1,1)