6
version
nil
"P"
"bool"
typeOp
nil
opType
0
def
var
1
def
"="
const
2
def
"->"
typeOp
3
def
"Number.Natural.natural"
typeOp
nil
opType
4
def
3
ref
4
ref
0
ref
nil
cons
5
def
cons
opType
6
def
nil
cons
cons
opType
constTerm
"Number.GF(p).oddprime"
const
4
ref
constTerm
7
def
appTerm
"Number.Natural.zero"
const
4
remove
constTerm
8
def
appTerm
9
def
nil
cons
10
def
cons
11
def
nil
cons
nil
cons
cons
2
ref
3
ref
0
ref
3
ref
0
ref
5
ref
cons
opType
12
def
nil
cons
cons
opType
13
def
constTerm
14
def
"Data.Bool.~"
const
12
ref
constTerm
15
def
1
ref
varTerm
16
def
appTerm
17
def
appTerm
refl
"p"
0
ref
var
18
def
"Data.Bool.==>"
const
13
ref
constTerm
19
def
18
ref
varTerm
20
def
appTerm
21
def
"Data.Bool.F"
const
0
ref
constTerm
22
def
appTerm
absTerm
23
def
16
ref
appTerm
betaConv
appThm
nil
2
ref
3
ref
12
ref
3
ref
12
ref
5
ref
cons
opType
24
def
nil
cons
cons
opType
constTerm
25
def
15
ref
appTerm
23
remove
appTerm
axiom
16
ref
refl
26
def
appThm
eqMp
27
def
sym
subst
nil
18
ref
10
remove
cons
"q"
0
ref
var
28
def
22
ref
nil
cons
29
def
cons
nil
cons
30
def
cons
nil
cons
cons
31
def
14
ref
21
remove
28
ref
varTerm
32
def
appTerm
33
def
appTerm
refl
18
ref
28
ref
14
ref
"Data.Bool./\\"
const
13
ref
constTerm
34
def
20
ref
appTerm
35
def
32
ref
appTerm
36
def
appTerm
37
def
20
ref
appTerm
absTerm
38
def
absTerm
39
def
20
ref
appTerm
betaConv
32
ref
refl
40
def
appThm
38
remove
32
ref
appTerm
betaConv
trans
appThm
nil
2
ref
3
ref
13
ref
3
ref
13
ref
5
ref
cons
opType
41
def
nil
cons
cons
opType
constTerm
42
def
19
ref
appTerm
39
remove
appTerm
axiom
20
ref
refl
43
def
appThm
40
ref
appThm
eqMp
44
def
sym
45
def
subst
31
remove
14
ref
refl
46
def
"f"
13
remove
var
47
def
47
ref
varTerm
48
def
20
ref
appTerm
32
ref
appTerm
absTerm
49
def
18
ref
28
ref
32
ref
absTerm
50
def
absTerm
51
def
appTerm
betaConv
51
ref
20
ref
appTerm
betaConv
40
ref
appThm
50
ref
32
ref
appTerm
betaConv
trans
trans
appThm
47
ref
48
ref
"Data.Bool.T"
const
0
ref
constTerm
52
def
appTerm
52
ref
appTerm
absTerm
53
def
51
ref
appTerm
betaConv
51
ref
52
ref
appTerm
betaConv
52
ref
refl
54
def
appThm
50
ref
52
ref
appTerm
betaConv
trans
trans
55
def
appThm
37
remove
refl
28
ref
2
ref
3
ref
41
ref
3
ref
41
remove
5
ref
cons
opType
nil
cons
cons
opType
constTerm
56
def
49
remove
appTerm
53
ref
appTerm
absTerm
57
def
32
ref
appTerm
betaConv
appThm
25
ref
35
remove
appTerm
refl
18
ref
57
remove
absTerm
58
def
20
ref
appTerm
betaConv
appThm
nil
42
remove
34
ref
appTerm
58
ref
appTerm
axiom
59
def
43
remove
appThm
eqMp
40
ref
appThm
eqMp
60
def
36
remove
assume
eqMp
51
ref
refl
61
def
appThm
eqMp
sym
nil
52
ref
axiom
62
def
eqMp
63
def
60
remove
sym
47
ref
48
ref
refl
nil
"t"
0
ref
var
64
def
20
ref
nil
cons
65
def
cons
nil
cons
nil
cons
cons
14
ref
64
ref
varTerm
66
def
appTerm
52
ref
appTerm
assume
sym
62
ref
eqMp
66
ref
assume
62
ref
deductAntisym
deductAntisym
67
def
subst
20
ref
assume
68
def
eqMp
appThm
nil
64
ref
32
ref
nil
cons
69
def
cons
nil
cons
nil
cons
cons
67
remove
subst
32
ref
assume
70
def
eqMp
appThm
absThm
eqMp
71
def
deductAntisym
72
def
subst
nil
"Number.Natural.prime"
const
6
remove
constTerm
73
def
7
remove
appTerm
74
def
axiom
nil
18
ref
74
remove
nil
cons
75
def
cons
30
ref
cons
nil
cons
cons
45
ref
71
remove
nil
1
ref
65
ref
cons
"Q"
0
ref
var
76
def
69
ref
cons
nil
cons
77
def
cons
nil
cons
cons
46
ref
47
ref
48
remove
16
ref
appTerm
78
def
76
ref
varTerm
79
def
appTerm
absTerm
80
def
18
ref
28
ref
20
ref
absTerm
absTerm
81
def
appTerm
betaConv
81
ref
16
ref
appTerm
betaConv
79
ref
refl
82
def
appThm
28
ref
16
ref
absTerm
79
ref
appTerm
betaConv
trans
trans
appThm
53
ref
81
ref
appTerm
betaConv
81
ref
52
ref
appTerm
betaConv
54
remove
appThm
28
ref
52
ref
absTerm
52
ref
appTerm
betaConv
trans
trans
appThm
14
ref
34
remove
16
ref
appTerm
83
def
79
ref
appTerm
84
def
appTerm
refl
28
ref
56
remove
47
remove
78
remove
32
ref
appTerm
absTerm
appTerm
53
remove
appTerm
absTerm
79
ref
appTerm
betaConv
appThm
25
remove
83
remove
appTerm
refl
58
remove
16
ref
appTerm
betaConv
appThm
59
remove
26
remove
appThm
eqMp
82
ref
appThm
eqMp
84
remove
assume
eqMp
85
def
81
remove
refl
appThm
eqMp
sym
62
ref
eqMp
86
def
subst
deductAntisym
eqMp
44
remove
33
ref
assume
eqMp
sym
68
remove
eqMp
63
remove
proveHyp
deductAntisym
87
def
subst
proveHyp
nil
64
ref
75
remove
cons
nil
cons
nil
cons
cons
64
remove
14
ref
19
ref
66
ref
appTerm
22
ref
appTerm
appTerm
15
ref
66
ref
appTerm
appTerm
absTerm
88
def
66
ref
appTerm
89
def
betaConv
nil
"Data.Bool.!"
const
90
def
24
remove
constTerm
91
def
88
ref
appTerm
92
def
axiom
nil
18
ref
92
remove
nil
cons
cons
28
ref
89
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
87
ref
subst
proveHyp
"A"
5
ref
cons
nil
cons
93
def
"P"
12
remove
var
94
def
88
remove
nil
cons
cons
"x"
0
remove
var
95
def
66
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
nil
18
ref
90
remove
3
ref
3
ref
"A"
varType
96
def
5
ref
cons
opType
97
def
5
ref
cons
opType
98
def
constTerm
99
def
"P"
97
ref
var
varTerm
100
def
appTerm
101
def
nil
cons
102
def
cons
28
ref
100
ref
"x"
96
remove
var
103
def
varTerm
104
def
appTerm
105
def
nil
cons
106
def
cons
nil
cons
cons
nil
cons
cons
107
def
45
ref
subst
107
remove
72
ref
subst
14
ref
105
remove
appTerm
refl
103
remove
52
ref
absTerm
108
def
104
ref
appTerm
betaConv
appThm
"p"
97
ref
var
109
def
2
ref
3
ref
97
remove
98
ref
nil
cons
cons
opType
constTerm
109
remove
varTerm
appTerm
108
remove
appTerm
absTerm
110
def
100
ref
appTerm
betaConv
nil
2
remove
3
ref
98
ref
3
remove
98
remove
5
remove
cons
opType
nil
cons
cons
opType
constTerm
99
remove
appTerm
110
remove
appTerm
axiom
100
remove
refl
appThm
101
remove
assume
eqMp
eqMp
104
remove
refl
appThm
eqMp
sym
62
ref
eqMp
eqMp
nil
1
ref
102
remove
cons
76
ref
106
remove
cons
nil
cons
cons
nil
cons
cons
86
ref
subst
deductAntisym
eqMp
111
def
subst
eqMp
eqMp
subst
15
ref
refl
73
ref
refl
9
ref
assume
appThm
nil
15
ref
73
remove
8
remove
appTerm
112
def
appTerm
113
def
axiom
nil
18
ref
113
remove
nil
cons
cons
28
ref
14
ref
112
ref
appTerm
22
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
87
ref
subst
proveHyp
nil
1
ref
112
remove
nil
cons
cons
nil
cons
nil
cons
cons
nil
18
ref
17
ref
nil
cons
114
def
cons
28
ref
14
ref
16
ref
appTerm
22
ref
appTerm
nil
cons
115
def
cons
nil
cons
cons
nil
cons
cons
116
def
45
ref
subst
116
remove
72
ref
subst
nil
18
ref
16
ref
nil
cons
117
def
cons
30
remove
cons
nil
cons
cons
19
ref
refl
14
ref
20
ref
appTerm
32
ref
appTerm
assume
118
def
appThm
40
remove
appThm
sym
nil
18
ref
69
ref
cons
119
def
28
ref
69
ref
cons
nil
cons
cons
nil
cons
cons
120
def
45
ref
subst
120
remove
72
ref
subst
70
remove
eqMp
nil
1
ref
69
remove
cons
77
remove
cons
nil
cons
cons
86
ref
subst
deductAntisym
eqMp
121
def
eqMp
nil
18
ref
33
remove
nil
cons
122
def
cons
28
ref
19
ref
32
remove
appTerm
123
def
20
ref
appTerm
nil
cons
124
def
cons
nil
cons
cons
nil
cons
cons
72
ref
subst
proveHyp
123
remove
refl
118
remove
appThm
sym
121
remove
eqMp
eqMp
nil
119
remove
28
ref
65
remove
cons
nil
cons
cons
nil
cons
cons
87
ref
subst
nil
1
ref
122
remove
cons
76
ref
124
remove
cons
nil
cons
cons
nil
cons
cons
125
def
46
remove
80
remove
51
ref
appTerm
betaConv
51
remove
16
ref
appTerm
betaConv
82
remove
appThm
50
remove
79
remove
appTerm
betaConv
trans
trans
appThm
55
remove
appThm
85
remove
61
remove
appThm
eqMp
sym
62
ref
eqMp
subst
eqMp
87
ref
125
remove
86
ref
subst
eqMp
deductAntisym
deductAntisym
subst
27
remove
17
remove
assume
eqMp
nil
18
ref
19
ref
16
ref
appTerm
22
ref
appTerm
nil
cons
cons
28
ref
19
remove
22
ref
appTerm
16
ref
appTerm
nil
cons
cons
nil
cons
cons
nil
cons
cons
72
ref
subst
proveHyp
nil
18
ref
29
ref
cons
28
ref
117
ref
cons
nil
cons
cons
nil
cons
cons
126
def
45
remove
subst
126
remove
72
remove
subst
18
ref
20
remove
absTerm
127
def
16
remove
appTerm
128
def
betaConv
nil
14
ref
22
ref
appTerm
91
remove
127
ref
appTerm
129
def
appTerm
axiom
22
ref
assume
eqMp
nil
18
remove
129
remove
nil
cons
cons
28
remove
128
remove
nil
cons
cons
nil
cons
cons
nil
cons
cons
87
remove
subst
proveHyp
93
remove
94
remove
127
remove
nil
cons
cons
95
remove
117
ref
cons
nil
cons
cons
nil
cons
cons
111
remove
subst
eqMp
eqMp
eqMp
nil
1
ref
29
ref
cons
76
ref
117
remove
cons
nil
cons
cons
nil
cons
cons
86
ref
subst
deductAntisym
eqMp
eqMp
eqMp
eqMp
nil
1
remove
114
remove
cons
76
ref
115
remove
cons
nil
cons
cons
nil
cons
cons
86
ref
subst
deductAntisym
eqMp
subst
eqMp
trans
appThm
nil
14
remove
15
ref
22
remove
appTerm
appTerm
52
remove
appTerm
axiom
trans
trans
sym
62
remove
eqMp
eqMp
eqMp
nil
11
remove
76
remove
29
remove
cons
nil
cons
cons
nil
cons
cons
86
remove
subst
deductAntisym
eqMp
eqMp
nil
15
remove
9
remove
appTerm
thm