6
version
nil
"P"
"->"
typeOp
0
def
"Data.Word16.word16"
typeOp
nil
opType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
var
"w"
1
ref
var
5
def
"="
const
6
def
0
ref
"Data.Pair.*"
typeOp
"Data.Byte.byte"
typeOp
nil
opType
7
def
7
ref
nil
cons
8
def
cons
opType
9
def
0
ref
9
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
10
def
"Data.Word16.toBytes"
"_31280"
1
ref
var
11
def
"Data.Pair.,"
const
0
ref
7
ref
0
ref
7
ref
9
remove
nil
cons
12
def
cons
opType
nil
cons
cons
opType
constTerm
13
def
"Data.Byte.fromNatural"
const
0
ref
"Number.Natural.natural"
typeOp
nil
opType
14
def
8
ref
cons
opType
constTerm
15
def
"Data.Word16.toNatural"
const
0
ref
1
ref
14
ref
nil
cons
16
def
cons
opType
constTerm
17
def
11
ref
varTerm
18
def
appTerm
appTerm
appTerm
15
ref
17
ref
"Data.Word16.shiftRight"
const
0
ref
1
ref
0
ref
14
ref
1
ref
nil
cons
19
def
cons
opType
20
def
nil
cons
cons
opType
21
def
constTerm
22
def
18
ref
appTerm
"Number.Natural.bit0"
const
0
ref
14
ref
16
ref
cons
opType
23
def
constTerm
24
def
24
ref
24
remove
"Number.Natural.bit1"
const
23
remove
constTerm
"Number.Natural.zero"
const
14
remove
constTerm
appTerm
appTerm
appTerm
appTerm
25
def
appTerm
appTerm
appTerm
appTerm
26
def
absTerm
27
def
defineConst
28
def
pop
0
ref
1
ref
12
remove
cons
opType
constTerm
29
def
5
remove
varTerm
30
def
appTerm
appTerm
13
remove
15
ref
17
ref
30
ref
appTerm
appTerm
appTerm
15
remove
17
remove
22
remove
30
remove
appTerm
25
ref
appTerm
appTerm
appTerm
appTerm
appTerm
absTerm
31
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
19
ref
cons
nil
cons
nil
nil
cons
32
def
cons
6
ref
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
33
def
"Data.Bool.!"
const
34
def
0
ref
0
ref
"A"
varType
35
def
3
ref
cons
opType
36
def
3
ref
cons
opType
37
def
constTerm
38
def
"P"
36
ref
var
varTerm
39
def
appTerm
appTerm
refl
"p"
36
ref
var
40
def
6
ref
0
ref
36
remove
37
ref
nil
cons
cons
opType
constTerm
40
remove
varTerm
appTerm
"x"
35
remove
var
"Data.Bool.T"
const
2
ref
constTerm
41
def
absTerm
appTerm
absTerm
42
def
39
ref
appTerm
betaConv
appThm
nil
6
ref
0
ref
37
ref
0
ref
37
remove
3
ref
cons
opType
nil
cons
cons
opType
constTerm
38
remove
appTerm
42
remove
appTerm
axiom
39
remove
refl
appThm
eqMp
sym
43
def
subst
subst
11
remove
nil
"t"
2
remove
var
44
def
10
remove
29
remove
18
ref
appTerm
appTerm
26
remove
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
33
remove
44
ref
varTerm
45
def
appTerm
41
ref
appTerm
assume
sym
nil
41
remove
axiom
46
def
eqMp
45
remove
assume
46
remove
deductAntisym
deductAntisym
47
def
subst
28
remove
18
ref
refl
appThm
27
remove
18
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
nil
34
ref
0
ref
4
ref
3
ref
cons
opType
constTerm
31
remove
appTerm
thm
nil
"P"
0
ref
7
ref
3
ref
cons
opType
48
def
var
49
def
"b0"
7
ref
var
50
def
34
remove
0
ref
48
remove
3
remove
cons
opType
constTerm
51
def
"b1"
7
ref
var
52
def
6
remove
0
ref
1
ref
4
remove
nil
cons
cons
opType
constTerm
53
def
"Data.Word16.fromBytes"
"_31285"
7
ref
var
54
def
"_31286"
7
ref
var
55
def
"Data.Word16.or"
const
0
ref
1
ref
0
ref
1
remove
19
ref
cons
opType
nil
cons
cons
opType
constTerm
56
def
"Data.Word16.fromNatural"
const
20
remove
constTerm
57
def
"Data.Byte.toNatural"
const
0
ref
7
ref
16
remove
cons
opType
constTerm
58
def
54
ref
varTerm
59
def
appTerm
appTerm
appTerm
"Data.Word16.shiftLeft"
const
21
remove
constTerm
60
def
57
ref
58
ref
55
ref
varTerm
61
def
appTerm
appTerm
appTerm
25
ref
appTerm
appTerm
62
def
absTerm
63
def
absTerm
64
def
defineConst
65
def
pop
0
ref
7
ref
0
remove
7
remove
19
remove
cons
opType
nil
cons
cons
opType
constTerm
66
def
50
remove
varTerm
67
def
appTerm
52
remove
varTerm
68
def
appTerm
appTerm
56
remove
57
ref
58
ref
67
remove
appTerm
appTerm
appTerm
60
remove
57
remove
58
remove
68
remove
appTerm
appTerm
appTerm
25
remove
appTerm
appTerm
appTerm
absTerm
appTerm
absTerm
69
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
8
remove
cons
nil
cons
32
remove
cons
43
remove
subst
70
def
subst
54
remove
nil
44
ref
51
ref
55
ref
53
remove
66
remove
59
ref
appTerm
61
ref
appTerm
appTerm
62
remove
appTerm
71
def
absTerm
72
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
47
ref
subst
nil
49
remove
72
remove
nil
cons
cons
nil
cons
nil
cons
cons
70
remove
subst
55
remove
nil
44
remove
71
remove
nil
cons
cons
nil
cons
nil
cons
cons
47
remove
subst
65
remove
59
ref
refl
appThm
64
remove
59
remove
appTerm
betaConv
trans
61
ref
refl
appThm
63
remove
61
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
51
remove
69
remove
appTerm
thm