[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 string-ops
Status:
Proved!
Axioms: 24, User Theorems: 32 (Proved: 32, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 228, Interactions: 107
Char-downcase-no(0,0)
String-downcaseFirst-empty(0,0)
butlast-in(2,1)
char-in-rec(1,1)
last-app(7,3)
prefix-def(0,0)
right-trim-done(0,0)
substring-offset-rec(10,3)
Char-downcase-yes(0,0)
String-upcase-empty(0,0)
butlast-length(6,2)
downcase-A(12,7)
last-def(0,0)
prefix-empty(1,1)
right-trim-empty(0,0)
substring-zero-rec(10,3)
Char-upcase-no(0,0)
String-upcase-rec(0,0)
char-in(5,3)
downcase-B(15,8)
last-in(7,3)
prefix-empty-01(2,1)
right-trim-rec(0,0)
test-downcaseFirst(4,4)
Char-upcase-yes(0,0)
String-upcaseFirst-def(0,0)
char-in-01(1,1)
downcase-C(15,8)
left-trim-done(0,0)
prefix-num(9,2)
right-trim-trim(5,3)
trim-number(0,0)
String-downcase-empty(0,0)
String-upcaseFirst-empty(0,0)
char-in-app(1,1)
downcase-lower-a(7,4)
left-trim-empty(0,0)
prefix-num-01(7,1)
substring-all(3,2)
trim-number-01(3,3)
String-downcase-rec(0,0)
butlast-app(5,3)
char-in-empty(2,1)
downcase-rec(5,2)
left-trim-rec(0,0)
prefix-reflexive(1,1)
substring-app-rec(10,2)
trim-number-02(2,2)
String-downcaseFirst-def(0,0)
butlast-def(0,0)
char-in-one(1,1)
in-def(0,0)
natstring-chars(47,16)
right-trim-app(10,7)
substring-def(0,0)
upcase-a(12,7)