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