1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
\chapter{Pre-proved Theorems}
\input{theorems-intro}
\section{Definitions}
\THEOREM ASCII\_DEF ascii
|- !b0 b1 b2 b3 b4 b5 b6 b7.
ASCII b0 b1 b2 b3 b4 b5 b6 b7 =
ABS_ascii(Node(b0,b1,b2,b3,b4,b5,b6,b7)[])
\ENDTHEOREM
\THEOREM ascii\_ISO\_DEF ascii
|- (!a. ABS_ascii(REP_ascii a) = a) /\
(!r.
TRP
(\v tl.
(?b0 b1 b2 b3 b4 b5 b6 b7. v = b0,b1,b2,b3,b4,b5,b6,b7) /\
(LENGTH tl = 0))
r =
(REP_ascii(ABS_ascii r) = r))
\ENDTHEOREM
\THEOREM ascii\_TY\_DEF ascii
|- ?rep.
TYPE_DEFINITION
(TRP
(\v tl.
(?b0 b1 b2 b3 b4 b5 b6 b7. v = b0,b1,b2,b3,b4,b5,b6,b7) /\
(LENGTH tl = 0)))
rep
\ENDTHEOREM
\THEOREM STRING\_DEF string
|- !a s. STRING a s = ABS_string(Node(INR a)[REP_string s])
\ENDTHEOREM
\THEOREM string\_ISO\_DEF string
|- (!a. ABS_string(REP_string a) = a) /\
(!r.
TRP
(\v tl.
(v = INL one) /\ (LENGTH tl = 0) \/
(?a. v = INR a) /\ (LENGTH tl = SUC 0))
r =
(REP_string(ABS_string r) = r))
\ENDTHEOREM
\THEOREM string\_TY\_DEF string
|- ?rep.
TYPE_DEFINITION
(TRP
(\v tl.
(v = INL one) /\ (LENGTH tl = 0) \/
(?a. v = INR a) /\ (LENGTH tl = SUC 0)))
rep
\ENDTHEOREM
\THEOREM ``\_DEF string
|- `` = ABS_string(Node(INL one)[]))
\ENDTHEOREM
\section{Theorems}
\THEOREM ASCII\_11 ascii
|- !b0 b1 b2 b3 b4 b5 b6 b7 b0' b1' b2' b3' b4' b5' b6' b7'.
(ASCII b0 b1 b2 b3 b4 b5 b6 b7 =
ASCII b0' b1' b2' b3' b4' b5' b6' b7') =
(b0 = b0') /\
(b1 = b1') /\
(b2 = b2') /\
(b3 = b3') /\
(b4 = b4') /\
(b5 = b5') /\
(b6 = b6') /\
(b7 = b7')
\ENDTHEOREM
\THEOREM ascii\_Axiom ascii
|- !f.
?! fn.
!b0 b1 b2 b3 b4 b5 b6 b7.
fn(ASCII b0 b1 b2 b3 b4 b5 b6 b7) = f b0 b1 b2 b3 b4 b5 b6 b7
\ENDTHEOREM
\THEOREM ascii\_CASES ascii
|- !a. ?b0 b1 b2 b3 b4 b5 b6 b7. a = ASCII b0 b1 b2 b3 b4 b5 b6 b7
\ENDTHEOREM
\THEOREM ascii\_Induct ascii
|- !P.
(!b0 b1 b2 b3 b4 b5 b6 b7. P(ASCII b0 b1 b2 b3 b4 b5 b6 b7)) ==>
(!a. P a)
\ENDTHEOREM
\THEOREM NOT\_EMPTY\_STRING string
|- !a s. ~(STRING a s = ``)
\ENDTHEOREM
\THEOREM NOT\_STRING\_EMPTY string
|- !a s. ~(`` = STRING a s)
\ENDTHEOREM
\THEOREM STRING\_11 string
|- !a s a' s'. (STRING a s = STRING a' s') = (a = a') /\ (s = s')
\ENDTHEOREM
\THEOREM string\_Axiom string
|- !e f. ?! fn. (fn `` = e) /\ (!a s. fn(STRING a s) = f(fn s)a s)
\ENDTHEOREM
\THEOREM string\_CASES string
|- !s. (s = ``) \/ (?s' a. s = STRING a s')
\ENDTHEOREM
\THEOREM string\_Induct string
|- !P. P `` /\ (!s. P s ==> (!a. P(STRING a s))) ==> (!s. P s)
\ENDTHEOREM
|
