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