nil
"Data.Bool.!"
const
0
def
"->"
typeOp
1
def
1
ref
"Number.Natural.natural"
typeOp
nil
opType
2
def
"bool"
typeOp
nil
opType
nil
cons
3
def
cons
opType
3
ref
cons
opType
constTerm
4
def
"n"
2
ref
var
5
def
"="
const
1
ref
"Algebra.Monoid.monoid"
typeOp
nil
opType
6
def
1
ref
6
ref
3
ref
cons
opType
7
def
nil
cons
cons
opType
constTerm
8
def
"Algebra.Monoid.*"
const
1
ref
6
ref
1
ref
2
ref
6
ref
nil
cons
9
def
cons
opType
nil
cons
cons
opType
constTerm
10
def
"Algebra.Monoid.0"
const
6
ref
constTerm
11
def
appTerm
5
ref
varTerm
12
def
appTerm
appTerm
11
remove
appTerm
absTerm
appTerm
13
def
axiom
nil
13
remove
thm
nil
0
remove
1
ref
7
remove
3
remove
cons
opType
constTerm
14
def
"x"
6
ref
var
15
def
4
ref
"m"
2
ref
var
16
def
4
ref
5
ref
8
ref
10
ref
15
ref
varTerm
17
def
appTerm
18
def
"Number.Natural.+"
const
1
ref
2
ref
1
ref
2
ref
2
ref
nil
cons
cons
opType
19
def
nil
cons
cons
opType
20
def
constTerm
16
ref
varTerm
21
def
appTerm
12
ref
appTerm
appTerm
appTerm
"Algebra.Monoid.+"
const
1
ref
6
ref
1
remove
6
remove
9
remove
cons
opType
nil
cons
cons
opType
constTerm
22
def
18
ref
21
ref
appTerm
23
def
appTerm
18
ref
12
ref
appTerm
24
def
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
25
def
axiom
nil
25
remove
thm
nil
14
ref
15
ref
4
ref
5
ref
8
ref
18
ref
"Number.Natural.suc"
const
19
ref
constTerm
12
ref
appTerm
appTerm
appTerm
22
ref
24
remove
appTerm
17
ref
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
26
def
axiom
nil
26
remove
thm
nil
14
ref
15
ref
4
ref
16
remove
4
remove
5
remove
8
ref
18
ref
"Number.Natural.*"
const
20
remove
constTerm
21
remove
appTerm
12
ref
appTerm
appTerm
appTerm
10
remove
23
remove
appTerm
12
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
27
def
axiom
nil
27
remove
thm
nil
14
ref
15
ref
8
ref
18
ref
"Number.Natural.bit1"
const
19
ref
constTerm
"Number.Natural.zero"
const
2
remove
constTerm
appTerm
28
def
appTerm
appTerm
17
ref
appTerm
absTerm
appTerm
29
def
axiom
nil
29
remove
thm
nil
14
remove
15
remove
8
remove
18
remove
"Number.Natural.bit0"
const
19
remove
constTerm
28
remove
appTerm
appTerm
appTerm
22
remove
17
ref
appTerm
17
remove
appTerm
appTerm
absTerm
appTerm
30
def
axiom
nil
30
remove
thm