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