path: "vendor/opentheory/data/theories/axiom-infinity/axiom-infinity.art"
6 version "A" "->" typeOp 0 def "ind" typeOp nil opType 1 def 1 ref nil cons 2 def cons opType 3 def nil cons cons nil cons 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 13 def 11 ref constTerm 14 def appTerm "p" 10 ref var 15 def "Data.Bool.!" const 16 def 0 ref 0 ref 8 ref 9 ref cons opType 17 def 9 ref cons opType 18 def constTerm 19 def "q" 8 ref var 20 def "Data.Bool.==>" const 0 ref 8 ref 17 ref nil cons cons opType 21 def constTerm 22 def 16 ref 11 ref constTerm 23 def "x" 7 ref var 24 def 22 ref 15 ref varTerm 25 def 24 ref varTerm 26 def appTerm appTerm 20 ref varTerm 27 def appTerm absTerm appTerm appTerm 27 ref appTerm absTerm appTerm absTerm appTerm axiom 28 def subst "p" 0 ref 3 ref 9 ref cons opType 29 def var 30 def "A" 9 ref cons nil cons 4 ref cons nil 12 remove 23 ref appTerm 15 remove 6 ref 0 ref 10 ref 11 remove nil cons cons opType constTerm 25 remove appTerm 24 ref "Data.Bool.T" const 8 ref constTerm 31 def absTerm 32 def appTerm absTerm 33 def appTerm axiom 34 def subst "p" 17 ref var 35 def 6 ref 0 ref 17 ref 18 remove nil cons cons opType constTerm 36 def 35 remove varTerm appTerm refl "x" 8 ref var 37 def nil 6 ref 21 ref constTerm 38 def 31 ref appTerm 36 ref "p" 8 ref var 39 def 39 ref varTerm 40 def absTerm 41 def appTerm 41 ref appTerm appTerm axiom 42 def absThm appThm absThm trans 43 def 20 ref nil 6 ref 0 ref 21 ref 0 ref 21 ref 9 ref cons opType 44 def nil cons cons opType constTerm 45 def 22 ref appTerm 39 ref 20 ref 38 ref "Data.Bool./\\" const 21 ref constTerm 46 def 40 ref appTerm 47 def 27 ref appTerm 48 def appTerm 49 def 40 ref appTerm absTerm 50 def absTerm 51 def appTerm axiom 52 def 39 ref 20 ref 38 ref refl 53 def nil 45 remove 46 ref appTerm 39 ref 20 ref 6 ref 0 ref 44 ref 0 ref 44 remove 9 ref cons opType nil cons cons opType constTerm 54 def "f" 21 ref var 55 def 55 ref varTerm 56 def 40 ref appTerm 27 ref appTerm absTerm 57 def appTerm 58 def 55 ref 56 ref 31 ref appTerm 31 ref appTerm absTerm 59 def appTerm absTerm 60 def absTerm 61 def appTerm axiom 62 def 39 ref 20 ref 58 remove refl 55 ref 56 ref refl 63 def 42 ref appThm 42 ref appThm absThm appThm absThm absThm trans 64 def 40 ref refl 65 def appThm 27 ref refl 66 def appThm appThm 65 ref appThm absThm absThm trans 67 def 5 remove 34 ref subst 30 ref 6 ref 0 ref 29 ref 0 ref 29 ref 9 ref cons opType 68 def nil cons cons opType constTerm 69 def 30 remove varTerm 70 def appTerm refl "x" 3 ref var 71 def 42 ref absThm appThm absThm trans 71 ref 67 ref 70 remove 71 remove varTerm appTerm refl appThm 66 ref appThm absThm appThm appThm 66 ref appThm absThm appThm absThm trans "f" 3 ref var 72 def 64 remove "A" 2 ref cons 73 def "B" 2 remove cons nil cons cons 4 ref cons 74 def "f" 0 ref 7 ref "B" varType 75 def nil cons cons opType 76 def var 77 def 38 ref "Function.injective" const 78 def 0 ref 76 ref 9 ref cons opType 79 def constTerm 77 ref varTerm 80 def appTerm appTerm 23 ref "x1" 7 ref var 81 def 23 ref "x2" 7 ref var 82 def 22 ref 6 ref 0 ref 75 ref 0 ref 75 ref 9 ref cons opType 83 def nil cons cons opType constTerm 84 def 80 ref 81 remove varTerm 85 def appTerm appTerm 80 ref 82 remove varTerm 86 def appTerm appTerm appTerm 6 ref 0 ref 7 remove 10 ref nil cons cons opType constTerm 85 remove appTerm 86 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 87 def 80 ref appTerm 88 def betaConv nil 16 ref 0 ref 79 ref 9 ref cons opType constTerm 89 def 87 ref appTerm 90 def axiom nil 39 ref 90 remove nil cons cons 20 ref 88 remove nil cons cons nil cons cons nil cons cons 38 ref 22 remove 40 ref appTerm 91 def 27 ref appTerm 92 def appTerm refl 51 remove 40 ref appTerm betaConv 66 ref appThm 50 remove 27 ref appTerm betaConv trans appThm 52 remove 65 ref appThm 66 ref appThm eqMp 93 def sym 94 def 49 remove refl 60 remove 27 ref appTerm betaConv appThm 36 ref 47 remove appTerm refl 61 ref 40 ref appTerm betaConv appThm 62 ref 65 ref appThm eqMp 66 ref appThm eqMp 95 def sym 55 ref 63 remove nil "t" 8 ref var 96 def 40 ref nil cons 97 def cons nil cons nil cons cons 38 ref 96 ref varTerm 98 def appTerm 31 ref appTerm assume sym nil 31 ref axiom 99 def eqMp 98 remove assume 99 ref deductAntisym deductAntisym 100 def subst 40 ref assume 101 def eqMp appThm nil 96 remove 27 ref nil cons 102 def cons nil cons nil cons cons 100 remove subst 27 ref assume eqMp appThm absThm eqMp 103 def nil "P" 8 ref var 104 def 97 remove cons "Q" 8 ref var 105 def 102 remove cons nil cons cons nil cons cons 53 ref 55 ref 56 remove 104 ref varTerm 106 def appTerm 107 def 105 ref varTerm 108 def appTerm absTerm 39 ref 20 ref 40 ref absTerm absTerm 109 def appTerm betaConv 109 ref 106 ref appTerm betaConv 108 ref refl 110 def appThm 20 ref 106 ref absTerm 108 ref appTerm betaConv trans trans appThm 59 ref 109 ref appTerm betaConv 109 ref 31 ref appTerm betaConv 31 ref refl 111 def appThm 20 ref 31 ref absTerm 31 ref appTerm betaConv trans trans appThm 38 ref 46 ref 106 ref appTerm 112 def 108 ref appTerm 113 def appTerm refl 20 ref 54 ref 55 remove 107 remove 27 ref appTerm absTerm appTerm 59 ref appTerm absTerm 108 remove appTerm betaConv appThm 36 ref 112 remove appTerm refl 61 remove 106 ref appTerm betaConv appThm 62 remove 106 remove refl appThm eqMp 110 remove appThm eqMp 113 remove assume eqMp 109 remove refl appThm eqMp sym 99 ref eqMp 114 def subst deductAntisym eqMp 93 remove 92 remove assume eqMp sym 101 remove eqMp 53 remove 57 remove 39 ref 20 ref 27 ref absTerm 115 def absTerm 116 def appTerm betaConv 116 ref 40 remove appTerm betaConv 66 ref appThm 115 ref 27 remove appTerm betaConv trans trans appThm 59 remove 116 ref appTerm betaConv 116 ref 31 ref appTerm betaConv 111 remove appThm 115 remove 31 remove appTerm betaConv trans trans appThm 95 remove 48 remove assume eqMp 116 remove refl appThm eqMp sym 99 ref eqMp 117 def proveHyp deductAntisym 118 def subst proveHyp "A" 76 ref nil cons cons nil cons 119 def "P" 79 ref var 120 def 87 remove nil cons cons "x" 76 remove var 80 ref nil cons cons nil cons 121 def cons nil cons cons nil 39 ref 23 remove "P" 10 remove var varTerm 122 def appTerm 123 def nil cons 124 def cons 20 ref 122 ref 26 ref appTerm 125 def nil cons 126 def cons nil cons cons nil cons cons 127 def 94 remove subst 127 remove 117 remove 103 remove deductAntisym subst 38 ref 125 remove appTerm refl 32 remove 26 ref appTerm betaConv appThm 33 remove 122 ref appTerm betaConv 34 ref 122 remove refl appThm 123 remove assume eqMp eqMp 26 ref refl appThm eqMp sym 99 remove eqMp eqMp nil 104 remove 124 remove cons 105 remove 126 remove cons nil cons cons nil cons cons 114 remove subst deductAntisym eqMp 128 def subst eqMp eqMp subst 73 remove nil cons 4 remove cons 129 def 34 remove subst "p" 0 ref 1 ref 9 ref cons opType 130 def var 131 def 6 ref 0 ref 130 ref 0 ref 130 ref 9 ref cons opType nil cons cons opType constTerm 132 def 131 ref varTerm 133 def appTerm refl "x" 1 ref var 134 def 42 remove absThm appThm absThm trans 135 def "x1" 1 ref var 136 def 135 ref "x2" 1 ref var 137 def 67 ref 6 remove 0 ref 1 ref 130 ref nil cons cons opType constTerm 138 def 72 ref varTerm 139 def 136 remove varTerm 140 def appTerm appTerm 139 ref 137 remove varTerm 141 def appTerm appTerm refl appThm 138 ref 140 remove appTerm 141 remove appTerm refl appThm absThm appThm absThm appThm trans appThm nil 36 ref "Data.Bool.~" const 17 ref constTerm 142 def appTerm 39 ref 91 remove "Data.Bool.F" const 8 ref constTerm 143 def appTerm absTerm appTerm axiom 39 ref 67 ref 65 remove appThm nil 38 ref 143 remove appTerm 19 remove 41 ref appTerm appTerm axiom 43 ref 41 remove refl appThm trans appThm absThm trans 74 remove 77 remove 38 ref "Function.surjective" const 144 def 79 remove constTerm 80 ref appTerm appTerm 16 remove 0 remove 83 remove 9 remove cons opType constTerm "y" 75 remove var 145 def 14 remove 24 remove 84 remove 145 remove varTerm appTerm 80 ref 26 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm absTerm 146 def 80 remove appTerm 147 def betaConv nil 89 remove 146 ref appTerm 148 def axiom nil 39 remove 148 remove nil cons cons 20 ref 147 remove nil cons cons nil cons cons nil cons cons 118 remove subst proveHyp 119 remove 120 remove 146 remove nil cons cons 121 remove cons nil cons cons 128 remove subst eqMp eqMp subst 135 ref "y" 1 ref var 149 def 129 remove 28 remove subst 131 remove 43 remove 20 remove 67 ref 135 remove 134 ref 67 remove 133 remove 134 ref varTerm 150 def appTerm refl appThm 66 ref appThm absThm appThm appThm 66 remove appThm absThm appThm absThm trans 134 remove 138 ref 149 ref varTerm 151 def appTerm 139 ref 150 remove appTerm appTerm absTerm refl appThm absThm appThm trans appThm appThm absThm appThm sym nil "a" 29 ref var 152 def "b" 17 remove var 153 def 36 ref 153 remove varTerm appTerm "c" 8 ref var 36 remove "d" 8 ref var 154 def 154 remove varTerm absTerm 155 def appTerm 155 ref appTerm 156 def absTerm appTerm absTerm 157 def "e" 8 ref var 158 def "f" 8 ref var 159 def "g" 8 ref var 160 def 38 remove "h" 8 ref var 161 def "i" 8 ref var 162 def 54 remove "j" 21 ref var 163 def 163 remove varTerm 161 remove varTerm appTerm 162 remove varTerm appTerm absTerm appTerm "k" 21 remove var 164 def 164 remove varTerm 156 ref appTerm 156 ref appTerm absTerm appTerm absTerm absTerm 165 def 159 remove varTerm 166 def appTerm 160 remove varTerm appTerm appTerm 166 remove appTerm absTerm absTerm 167 def "l" 29 ref var 168 def 69 remove 168 remove varTerm appTerm "m" 3 ref var 156 ref absTerm appTerm absTerm "n" 3 ref var 169 def 167 ref 152 remove varTerm 169 remove varTerm appTerm appTerm 158 remove varTerm 170 def appTerm absTerm appTerm appTerm 170 remove appTerm absTerm appTerm absTerm "p" 3 remove var 171 def 165 remove "q" 130 ref var 172 def 132 remove 172 remove varTerm appTerm "r" 1 ref var 156 remove absTerm appTerm absTerm 173 def "s" 1 ref var 174 def 173 ref "t" 1 ref var 175 def 167 ref 138 ref 171 remove varTerm 176 def 174 remove varTerm 177 def appTerm appTerm 176 ref 175 remove varTerm 178 def appTerm appTerm appTerm 138 ref 177 remove appTerm 178 remove appTerm appTerm absTerm appTerm absTerm appTerm appTerm "u" 8 remove var 179 def 167 ref 179 remove varTerm appTerm 157 ref 155 remove appTerm appTerm absTerm 173 ref "v" 1 ref var 180 def "w" 130 remove var 181 def 157 remove 37 ref 167 ref 173 remove 149 remove 167 remove 181 remove varTerm 151 remove appTerm appTerm 37 remove varTerm 182 def appTerm absTerm appTerm appTerm 182 remove appTerm absTerm appTerm absTerm "z" 1 remove var 183 def 138 remove 180 remove varTerm appTerm 176 remove 183 remove varTerm appTerm appTerm absTerm appTerm absTerm appTerm appTerm appTerm absTerm appTerm axiom eqMp nil 13 remove 68 remove constTerm 72 remove 46 remove 78 remove 29 ref constTerm 139 ref appTerm appTerm 142 remove 144 remove 29 remove constTerm 139 remove appTerm appTerm appTerm absTerm appTerm thm