path: "vendor/opentheory/data/theories/relation-natural-def/relation-natural-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 constTerm 8 def "n" 1 ref var 9 def "=" const 10 def 0 ref 2 ref 0 ref 2 ref 3 ref cons opType nil cons cons opType constTerm 11 def "Number.Natural.isSuc" "_11239" 1 ref var 12 def "_11240" 1 ref var 13 def 10 ref 0 ref 1 ref 4 remove nil cons cons opType 14 def constTerm 15 def "Number.Natural.suc" const 0 ref 1 ref 1 remove nil cons 16 def cons opType constTerm 17 def 12 ref varTerm 18 def appTerm appTerm 13 ref varTerm 19 def appTerm 20 def absTerm 21 def absTerm 22 def defineConst 23 def pop 14 ref constTerm 24 def 6 remove varTerm 25 def appTerm 9 remove varTerm 26 def appTerm appTerm 15 remove 17 remove 25 remove appTerm appTerm 26 remove appTerm appTerm absTerm appTerm absTerm 27 def nil cons cons nil cons nil cons cons "A" 16 ref cons nil cons nil nil cons 28 def cons 11 ref 7 ref 0 ref 0 ref "A" varType 29 def 3 ref cons opType 30 def 3 ref cons opType 31 def constTerm 32 def "P" 30 ref var 33 def varTerm 34 def appTerm appTerm refl "p" 30 ref var 35 def 10 ref 0 ref 30 ref 31 ref nil cons cons opType constTerm 35 remove varTerm appTerm "x" 29 ref var 36 def "Data.Bool.T" const 2 ref constTerm 37 def absTerm appTerm absTerm 38 def 34 ref appTerm betaConv appThm nil 10 remove 0 ref 31 ref 0 ref 31 remove 3 ref cons opType nil cons cons opType constTerm 32 ref appTerm 38 remove appTerm axiom 34 remove refl appThm eqMp sym 39 def subst 40 def subst 12 remove nil "t" 2 remove var 41 def 8 ref 13 ref 11 ref 24 remove 18 ref appTerm 19 ref appTerm appTerm 20 remove appTerm 42 def absTerm 43 def appTerm nil cons cons nil cons nil cons cons 11 ref 41 ref varTerm 44 def appTerm 37 ref appTerm assume sym nil 37 remove axiom 45 def eqMp 44 remove assume 45 remove deductAntisym deductAntisym 46 def subst nil 5 remove 43 remove nil cons cons nil cons nil cons cons 40 remove subst 13 remove nil 41 ref 42 remove nil cons cons nil cons nil cons cons 46 ref subst 23 remove 18 ref refl appThm 22 remove 18 remove appTerm betaConv trans 19 ref refl appThm 21 remove 19 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 8 remove 27 remove appTerm thm nil "P" 0 ref 0 ref 29 ref 16 remove cons opType 47 def 3 ref cons opType 48 def var "m" 47 ref var 49 def 32 ref 36 ref 32 ref "y" 29 ref var 50 def 11 ref "Relation.measure" "_12095" 47 ref var 51 def "_12096" 29 ref var 52 def "_12097" 29 ref var 53 def "Number.Natural.<" const 14 remove constTerm 54 def 51 ref varTerm 55 def 52 ref varTerm 56 def appTerm appTerm 55 ref 53 ref varTerm 57 def appTerm appTerm 58 def absTerm 59 def absTerm 60 def absTerm 61 def defineConst 62 def pop 0 ref 47 ref 0 ref 29 remove 30 remove nil cons cons opType nil cons cons opType constTerm 63 def 49 remove varTerm 64 def appTerm 36 remove varTerm 65 def appTerm 50 remove varTerm 66 def appTerm appTerm 54 remove 64 ref 65 remove appTerm appTerm 64 remove 66 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm 67 def nil cons cons nil cons nil cons cons "A" 47 remove nil cons cons nil cons 28 remove cons 39 ref subst subst 51 remove nil 41 ref 32 ref 52 ref 32 remove 53 ref 11 remove 63 remove 55 ref appTerm 56 ref appTerm 57 ref appTerm appTerm 58 remove appTerm 68 def absTerm 69 def appTerm 70 def absTerm 71 def appTerm nil cons cons nil cons nil cons cons 46 ref subst nil 33 ref 71 remove nil cons cons nil cons nil cons cons 39 ref subst 52 remove nil 41 ref 70 remove nil cons cons nil cons nil cons cons 46 ref subst nil 33 remove 69 remove nil cons cons nil cons nil cons cons 39 remove subst 53 remove nil 41 remove 68 remove nil cons cons nil cons nil cons cons 46 remove subst 62 remove 55 ref refl appThm 61 remove 55 remove appTerm betaConv trans 56 ref refl appThm 60 remove 56 remove appTerm betaConv trans 57 ref refl appThm 59 remove 57 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp eqMp absThm eqMp nil 7 remove 0 remove 48 remove 3 remove cons opType constTerm 67 remove appTerm thm