path: "vendor/opentheory/data/theories/monoid-comm-witness/monoid-comm-witness.art"
6 version nil "P" "->" typeOp 0 def "Algebra.Monoid.monoid" "HOLLight.mk_monoid" "HOLLight.dest_monoid" nil "A" "Data.Unit.unit" typeOp nil opType 1 def nil cons 2 def cons nil cons 3 def nil nil cons 4 def cons 5 def nil "=" const 6 def 0 ref 0 ref 0 ref "A" varType 7 def "bool" typeOp nil opType 8 def nil cons 9 def cons opType 10 def 9 ref cons opType 11 def 0 ref 11 ref 9 ref cons opType nil cons cons opType constTerm 12 def "Data.Bool.?" const 11 ref constTerm 13 def appTerm "p" 10 ref var 14 def 14 ref varTerm 15 def "select" const 16 def 0 ref 10 ref 7 ref nil cons cons opType constTerm 15 ref appTerm appTerm absTerm appTerm axiom subst "x" 1 ref var 17 def "Data.Bool.T" const 8 ref constTerm 18 def absTerm 19 def refl appThm "p" 0 ref 1 ref 9 ref cons opType 20 def var 21 def 21 remove varTerm 22 def 16 remove 0 ref 20 ref 2 ref cons opType constTerm 22 remove appTerm appTerm absTerm 19 remove appTerm betaConv trans 5 remove "t" 8 ref var 23 def 6 ref 0 ref 8 ref 0 ref 8 ref 9 ref cons opType 24 def nil cons cons opType 25 def constTerm 26 def 13 remove "x" 7 remove var 27 def 23 ref varTerm 28 def absTerm appTerm appTerm 28 ref appTerm absTerm 29 def 18 ref appTerm 30 def betaConv nil "Data.Bool.!" const 31 def 0 ref 24 ref 9 ref cons opType 32 def constTerm 29 ref appTerm 33 def axiom nil "p" 8 ref var 34 def 33 remove nil cons cons "q" 8 ref var 35 def 30 remove nil cons cons nil cons cons nil cons cons 26 ref "Data.Bool.==>" const 25 ref constTerm 36 def 34 ref varTerm 37 def appTerm 35 ref varTerm 38 def appTerm 39 def appTerm refl 34 ref 35 ref 26 ref "Data.Bool./\\" const 25 ref constTerm 40 def 37 ref appTerm 41 def 38 ref appTerm 42 def appTerm 43 def 37 ref appTerm absTerm 44 def absTerm 45 def 37 ref appTerm betaConv 38 ref refl 46 def appThm 44 remove 38 ref appTerm betaConv trans appThm nil 6 ref 0 ref 25 ref 0 ref 25 ref 9 ref cons opType 47 def nil cons cons opType constTerm 48 def 36 remove appTerm 45 remove appTerm axiom 37 ref refl 49 def appThm 46 ref appThm eqMp 50 def sym 51 def 43 remove refl 35 ref 6 ref 0 ref 47 ref 0 ref 47 remove 9 ref cons opType nil cons cons opType constTerm 52 def "f" 25 remove var 53 def 53 ref varTerm 54 def 37 ref appTerm 38 ref appTerm absTerm 55 def appTerm 53 ref 54 ref 18 ref appTerm 18 ref appTerm absTerm 56 def appTerm absTerm 57 def 38 ref appTerm betaConv appThm 6 ref 0 ref 24 ref 32 remove nil cons cons opType constTerm 58 def 41 remove appTerm refl 34 ref 57 remove absTerm 59 def 37 ref appTerm betaConv appThm nil 48 remove 40 ref appTerm 59 ref appTerm axiom 60 def 49 remove appThm eqMp 46 ref appThm eqMp 61 def sym 53 ref 54 ref refl nil 23 ref 37 ref nil cons 62 def cons nil cons nil cons cons 26 ref 28 ref appTerm 18 ref appTerm assume sym nil 18 ref axiom 63 def eqMp 28 remove assume 63 ref deductAntisym deductAntisym 64 def subst 37 ref assume 65 def eqMp appThm nil 23 ref 38 ref nil cons 66 def cons nil cons nil cons cons 64 ref subst 38 ref assume eqMp appThm absThm eqMp 67 def nil "P" 8 ref var 68 def 62 remove cons "Q" 8 ref var 69 def 66 remove cons nil cons cons nil cons cons 26 ref refl 70 def 53 ref 54 remove 68 ref varTerm 71 def appTerm 72 def 69 ref varTerm 73 def appTerm absTerm 34 ref 35 ref 37 ref absTerm absTerm 74 def appTerm betaConv 74 ref 71 ref appTerm betaConv 73 ref refl 75 def appThm 35 ref 71 ref absTerm 73 ref appTerm betaConv trans trans appThm 56 ref 74 ref appTerm betaConv 74 ref 18 ref appTerm betaConv 18 ref refl 76 def appThm 35 ref 18 ref absTerm 18 ref appTerm betaConv trans trans appThm 26 ref 40 remove 71 ref appTerm 77 def 73 ref appTerm 78 def appTerm refl 35 ref 52 remove 53 remove 72 remove 38 ref appTerm absTerm appTerm 56 ref appTerm absTerm 73 remove appTerm betaConv appThm 58 remove 77 remove appTerm refl 59 remove 71 ref appTerm betaConv appThm 60 remove 71 remove refl appThm eqMp 75 remove appThm eqMp 78 remove assume eqMp 74 remove refl appThm eqMp sym 63 ref eqMp 79 def subst deductAntisym eqMp 50 remove 39 remove assume eqMp sym 65 remove eqMp 70 remove 55 remove 34 ref 35 ref 38 ref absTerm 80 def absTerm 81 def appTerm betaConv 81 ref 37 remove appTerm betaConv 46 remove appThm 80 ref 38 remove appTerm betaConv trans trans appThm 56 remove 81 ref appTerm betaConv 81 ref 18 ref appTerm betaConv 76 remove appThm 80 remove 18 ref appTerm betaConv trans trans appThm 61 remove 42 remove assume eqMp 81 remove refl appThm eqMp sym 63 ref eqMp 82 def proveHyp deductAntisym 83 def subst proveHyp "A" 9 ref cons nil cons "P" 24 remove var 29 remove nil cons cons "x" 8 remove var 18 ref nil cons cons nil cons cons nil cons cons nil 34 ref 31 ref 11 ref constTerm 84 def "P" 10 ref var varTerm 85 def appTerm 86 def nil cons 87 def cons 35 ref 85 ref 27 ref varTerm 88 def appTerm 89 def nil cons 90 def cons nil cons cons nil cons cons 91 def 51 remove subst 91 remove 82 remove 67 remove deductAntisym subst 26 ref 89 remove appTerm refl 27 remove 18 remove absTerm 92 def 88 ref appTerm betaConv appThm 14 remove 6 ref 0 ref 10 remove 11 remove nil cons cons opType constTerm 15 remove appTerm 92 remove appTerm absTerm 93 def 85 ref appTerm betaConv 94 def nil 12 remove 84 remove appTerm 93 remove appTerm axiom 85 remove refl appThm 95 def 86 ref assume eqMp eqMp 88 remove refl appThm eqMp sym 63 ref eqMp eqMp nil 68 remove 87 remove cons 69 remove 90 remove cons nil cons cons nil cons cons 79 remove subst deductAntisym eqMp 96 def subst eqMp eqMp sym 63 remove eqMp subst eqMp defineTypeOp pop 97 def pop 98 def pop 99 def pop nil opType 100 def 9 ref cons opType 101 def var 102 def "x" 100 ref var 103 def 6 ref 0 ref 100 ref 101 ref nil cons cons opType constTerm 104 def "Algebra.Monoid.+" "_30410" 100 ref var "_30411" 100 ref var "Algebra.Monoid.0" 99 remove 0 ref 1 ref 100 ref nil cons 105 def cons opType constTerm 106 def "Data.Unit.()" const 1 ref constTerm 107 def appTerm 108 def defineConst pop 100 ref constTerm 109 def absTerm absTerm defineConst pop 0 ref 100 ref 0 ref 100 ref 105 ref cons opType nil cons cons opType constTerm 110 def 109 ref appTerm 103 ref varTerm 111 def appTerm 112 def appTerm 111 ref appTerm 113 def absTerm 114 def nil cons cons nil cons nil cons cons "A" 105 remove cons nil cons 115 def 4 remove cons 26 remove 86 remove appTerm refl 94 remove appThm 95 remove eqMp sym subst 116 def subst 103 ref nil 23 ref 113 remove nil cons cons nil cons nil cons cons 64 ref subst 104 ref refl 117 def nil 103 ref 112 remove nil cons cons nil cons nil cons cons 117 ref 103 ref 104 ref 111 ref appTerm 106 ref 98 remove 0 ref 100 ref 2 remove cons opType constTerm 118 def 111 ref appTerm 119 def appTerm 120 def appTerm 121 def absTerm 122 def 111 ref appTerm 123 def betaConv 31 ref 0 ref 101 remove 9 ref cons opType constTerm 124 def refl 103 ref 121 remove assume sym 104 ref 120 remove appTerm 111 ref appTerm assume sym deductAntisym absThm appThm nil 102 ref "a" 100 ref var 125 def 104 ref 106 ref 118 ref 125 ref varTerm 126 def appTerm appTerm 127 def appTerm 126 ref appTerm 128 def absTerm nil cons cons nil cons nil cons cons 116 ref subst 125 ref nil 23 ref 128 remove nil cons cons nil cons nil cons cons 64 ref subst 117 ref 125 ref 127 remove absTerm 126 ref appTerm betaConv appThm 125 remove 126 ref absTerm 126 ref appTerm betaConv appThm 97 remove 126 remove refl appThm eqMp eqMp absThm eqMp eqMp nil 34 ref 124 ref 122 ref appTerm nil cons cons 35 ref 123 remove nil cons cons nil cons cons nil cons cons 83 ref subst proveHyp 115 remove 102 ref 122 remove nil cons cons 103 ref 111 ref nil cons cons nil cons cons nil cons cons 96 ref subst eqMp eqMp 129 def appThm nil 103 ref 109 ref nil cons cons nil cons nil cons cons 129 remove subst appThm sym 117 ref 106 remove refl 130 def nil "v" 1 ref var 131 def 119 remove nil cons cons nil cons nil cons cons 131 ref 6 remove 0 ref 1 remove 20 ref nil cons cons opType constTerm 131 ref varTerm 132 def appTerm 107 remove appTerm absTerm 133 def 132 ref appTerm 134 def betaConv nil 31 remove 0 remove 20 ref 9 remove cons opType constTerm 133 ref appTerm 135 def axiom nil 34 remove 135 remove nil cons cons 35 remove 134 remove nil cons cons nil cons cons nil cons cons 83 remove subst proveHyp 3 remove "P" 20 remove var 133 remove nil cons cons 17 remove 132 remove nil cons cons nil cons cons nil cons cons 96 remove subst eqMp eqMp 136 def subst appThm appThm 130 remove nil 131 remove 118 remove 109 ref appTerm nil cons cons nil cons nil cons cons 136 remove subst appThm appThm sym 108 remove refl eqMp eqMp 137 def subst appThm 137 ref appThm sym 109 remove refl 138 def eqMp eqMp absThm eqMp nil 124 ref 114 remove appTerm thm nil 102 ref 103 ref 124 ref "y" 100 ref var 139 def 124 ref "z" 100 remove var 140 def 104 ref 110 ref 110 ref 111 ref appTerm 141 def 139 ref varTerm 142 def appTerm 143 def appTerm 140 ref varTerm 144 def appTerm 145 def appTerm 141 remove 110 remove 142 remove appTerm 146 def 144 remove appTerm appTerm 147 def appTerm 148 def absTerm 149 def appTerm 150 def absTerm 151 def appTerm 152 def absTerm 153 def nil cons cons nil cons nil cons cons 116 ref subst 103 ref nil 23 ref 152 remove nil cons cons nil cons nil cons cons 64 ref subst nil 102 ref 151 remove nil cons cons nil cons nil cons cons 116 ref subst 139 ref nil 23 ref 150 remove nil cons cons nil cons nil cons cons 64 ref subst nil 102 ref 149 remove nil cons cons nil cons nil cons cons 116 ref subst 140 remove nil 23 ref 148 remove nil cons cons nil cons nil cons cons 64 ref subst 117 ref nil 103 ref 145 remove nil cons cons nil cons nil cons cons 137 ref subst appThm nil 103 ref 147 remove nil cons cons nil cons nil cons cons 137 ref subst appThm sym 138 ref eqMp eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 124 ref 153 remove appTerm thm nil 102 ref 103 ref 124 ref 139 ref 104 remove 143 ref appTerm 146 remove 111 remove appTerm 154 def appTerm 155 def absTerm 156 def appTerm 157 def absTerm 158 def nil cons cons nil cons nil cons cons 116 ref subst 103 ref nil 23 ref 157 remove nil cons cons nil cons nil cons cons 64 ref subst nil 102 remove 156 remove nil cons cons nil cons nil cons cons 116 remove subst 139 remove nil 23 remove 155 remove nil cons cons nil cons nil cons cons 64 remove subst 117 remove nil 103 ref 143 remove nil cons cons nil cons nil cons cons 137 ref subst appThm nil 103 remove 154 remove nil cons cons nil cons nil cons cons 137 remove subst appThm sym 138 remove eqMp eqMp absThm eqMp eqMp absThm eqMp nil 124 remove 158 remove appTerm thm