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