6
version
nil
"P"
"->"
typeOp
0
def
"Number.Natural.natural"
typeOp
nil
opType
1
def
"bool"
typeOp
nil
opType
2
def
nil
cons
3
def
cons
opType
4
def
var
5
def
"n"
1
ref
var
6
def
"Data.Bool.!"
const
7
def
0
ref
4
ref
3
ref
cons
opType
constTerm
8
def
"r"
1
ref
var
9
def
8
ref
"k"
1
ref
var
10
def
8
ref
"a"
1
ref
var
11
def
"="
const
12
def
0
ref
1
ref
4
remove
nil
cons
cons
opType
constTerm
13
def
"Number.Natural.Montgomery.reduce"
"_42886"
1
ref
var
14
def
"_42887"
1
ref
var
15
def
"_42888"
1
ref
var
16
def
"_42889"
1
ref
var
17
def
"Number.Natural.div"
const
0
ref
1
ref
0
ref
1
ref
1
ref
nil
cons
18
def
cons
opType
nil
cons
cons
opType
19
def
constTerm
20
def
"Number.Natural.+"
const
19
ref
constTerm
21
def
17
ref
varTerm
22
def
appTerm
"Number.Natural.*"
const
19
ref
constTerm
23
def
"Number.Natural.mod"
const
19
ref
constTerm
24
def
23
ref
22
ref
appTerm
16
ref
varTerm
25
def
appTerm
appTerm
15
ref
varTerm
26
def
appTerm
appTerm
14
ref
varTerm
27
def
appTerm
appTerm
appTerm
26
ref
appTerm
28
def
absTerm
29
def
absTerm
30
def
absTerm
31
def
absTerm
32
def
defineConst
33
def
pop
0
ref
1
ref
0
ref
1
remove
19
remove
nil
cons
cons
opType
nil
cons
cons
opType
constTerm
34
def
6
remove
varTerm
35
def
appTerm
9
remove
varTerm
36
def
appTerm
10
remove
varTerm
37
def
appTerm
11
remove
varTerm
38
def
appTerm
appTerm
20
remove
21
remove
38
ref
appTerm
23
ref
24
remove
23
remove
38
remove
appTerm
37
remove
appTerm
appTerm
36
ref
appTerm
appTerm
35
remove
appTerm
appTerm
appTerm
36
remove
appTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
appTerm
absTerm
39
def
nil
cons
cons
nil
cons
nil
cons
cons
"A"
18
remove
cons
nil
cons
nil
nil
cons
cons
12
ref
0
ref
2
ref
0
ref
2
ref
3
ref
cons
opType
nil
cons
cons
opType
constTerm
40
def
7
remove
0
ref
0
ref
"A"
varType
41
def
3
ref
cons
opType
42
def
3
ref
cons
opType
43
def
constTerm
44
def
"P"
42
ref
var
varTerm
45
def
appTerm
appTerm
refl
"p"
42
ref
var
46
def
12
ref
0
ref
42
remove
43
ref
nil
cons
cons
opType
constTerm
46
remove
varTerm
appTerm
"x"
41
remove
var
"Data.Bool.T"
const
2
ref
constTerm
47
def
absTerm
appTerm
absTerm
48
def
45
ref
appTerm
betaConv
appThm
nil
12
remove
0
ref
43
ref
0
remove
43
remove
3
remove
cons
opType
nil
cons
cons
opType
constTerm
44
remove
appTerm
48
remove
appTerm
axiom
45
remove
refl
appThm
eqMp
sym
subst
49
def
subst
14
remove
nil
"t"
2
remove
var
50
def
8
ref
15
ref
8
ref
16
ref
8
ref
17
ref
13
remove
34
remove
27
ref
appTerm
26
ref
appTerm
25
ref
appTerm
22
ref
appTerm
appTerm
28
remove
appTerm
51
def
absTerm
52
def
appTerm
53
def
absTerm
54
def
appTerm
55
def
absTerm
56
def
appTerm
nil
cons
cons
nil
cons
nil
cons
cons
40
remove
50
ref
varTerm
57
def
appTerm
47
ref
appTerm
assume
sym
nil
47
remove
axiom
58
def
eqMp
57
remove
assume
58
remove
deductAntisym
deductAntisym
59
def
subst
nil
5
ref
56
remove
nil
cons
cons
nil
cons
nil
cons
cons
49
ref
subst
15
remove
nil
50
ref
55
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
5
ref
54
remove
nil
cons
cons
nil
cons
nil
cons
cons
49
ref
subst
16
remove
nil
50
ref
53
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
ref
subst
nil
5
remove
52
remove
nil
cons
cons
nil
cons
nil
cons
cons
49
remove
subst
17
remove
nil
50
remove
51
remove
nil
cons
cons
nil
cons
nil
cons
cons
59
remove
subst
33
remove
27
ref
refl
appThm
32
remove
27
remove
appTerm
betaConv
trans
26
ref
refl
appThm
31
remove
26
remove
appTerm
betaConv
trans
25
ref
refl
appThm
30
remove
25
remove
appTerm
betaConv
trans
22
ref
refl
appThm
29
remove
22
remove
appTerm
betaConv
trans
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
eqMp
absThm
eqMp
nil
8
remove
39
remove
appTerm
thm