[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 MeydenIntransWithState
Status:
Proved!
Axioms: 8, User Theorems: (Proved: 21, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 462, Interactions: 78
Security(12,6)
eqds-def(0,0)
eqs-reflexivity(1,1)
lemma2(4,3)
locally-respects2(2,1)
sources-base(0,0)
Security-simple(9,5)
eqds-refl(1,1)
eqs-step(14,6)
lemma3-2(34,9)
run-base(0,0)
sources-ipurge(197,1)
eqd-reflexivity(1,1)
eqds-symm(5,2)
ipurge-base(0,0)
lemma4(9,3)
run-initial(0,0)
sources-rec(0,0)
eqd-symmetry(5,2)
eqds-trans(8,4)
ipurge-idempotent(42,1)
lemma5-2(83,15)
run-rec(0,0)
weakly-step-consistent2(11,5)
eqd-transitivity(7,5)
eqs-ipurged(3,2)
ipurge-rec(0,0)
locally-respects(6,3)
sources-1(8,2)