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