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