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