path: "vendor/opentheory/data/theories/natural-prime-def/natural-prime-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 "p" 1 ref var 5 def "=" const 6 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType 7 def nil cons cons opType 8 def constTerm 9 def "Number.Natural.prime" "_29118" 1 ref var 10 def "Data.Bool./\\" const 8 ref constTerm 11 def "Data.Bool.~" const 7 remove constTerm 12 def 6 ref 0 ref 1 ref 4 ref nil cons cons opType 13 def constTerm 14 def 10 ref varTerm 15 def appTerm "Number.Natural.bit1" const 0 ref 1 ref 1 ref nil cons 16 def cons opType constTerm "Number.Natural.zero" const 1 ref constTerm appTerm 17 def appTerm appTerm appTerm "Data.Bool.!" const 18 def 0 ref 4 ref 3 ref cons opType constTerm 19 def "n" 1 remove var 20 def "Data.Bool.==>" const 8 ref constTerm 21 def "Number.Natural.divides" const 13 remove constTerm 20 ref varTerm 22 def appTerm 23 def 15 ref appTerm appTerm "Data.Bool.\\/" const 8 remove constTerm 14 ref 22 remove appTerm 24 def 17 ref appTerm appTerm 25 def 24 ref 15 ref appTerm appTerm appTerm absTerm appTerm appTerm 26 def absTerm 27 def defineConst 28 def pop 4 remove constTerm 29 def 5 remove varTerm 30 def appTerm appTerm 11 remove 12 remove 14 remove 30 ref appTerm 17 remove appTerm appTerm appTerm 19 ref 20 remove 21 remove 23 remove 30 ref appTerm appTerm 25 remove 24 remove 30 remove appTerm appTerm appTerm absTerm appTerm appTerm appTerm absTerm 31 def nil cons cons nil cons nil cons cons "A" 16 remove cons nil cons nil nil cons cons 9 ref 18 remove 0 ref 0 ref "A" varType 32 def 3 ref cons opType 33 def 3 ref cons opType 34 def constTerm 35 def "P" 33 ref var varTerm 36 def appTerm appTerm refl "p" 33 ref var 37 def 6 ref 0 ref 33 remove 34 ref nil cons cons opType constTerm 37 remove varTerm appTerm "x" 32 remove var "Data.Bool.T" const 2 ref constTerm 38 def absTerm appTerm absTerm 39 def 36 ref appTerm betaConv appThm nil 6 remove 0 ref 34 ref 0 remove 34 remove 3 remove cons opType nil cons cons opType constTerm 35 remove appTerm 39 remove appTerm axiom 36 remove refl appThm eqMp sym subst subst 10 remove nil "t" 2 remove var 40 def 9 ref 29 remove 15 ref appTerm appTerm 26 remove appTerm nil cons cons nil cons nil cons cons 9 remove 40 remove varTerm 41 def appTerm 38 ref appTerm assume sym nil 38 remove axiom 42 def eqMp 41 remove assume 42 remove deductAntisym deductAntisym subst 28 remove 15 ref refl appThm 27 remove 15 remove appTerm betaConv trans eqMp absThm eqMp nil 19 remove 31 remove appTerm thm