path: "vendor/opentheory/data/theories/natural-distance-def/natural-distance-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 1 ref 4 remove nil cons cons opType 11 def constTerm 12 def "Number.Natural.distance" "_16354" 1 ref var 13 def "_16355" 1 ref var 14 def "Data.Bool.cond" const 0 ref 2 ref 0 ref 1 ref 0 ref 1 ref 1 remove nil cons 15 def cons opType nil cons cons opType 16 def nil cons cons opType constTerm 17 def "Number.Natural.<=" const 11 remove constTerm 18 def 13 ref varTerm 19 def appTerm 14 ref varTerm 20 def appTerm appTerm "Number.Natural.-" const 16 ref constTerm 21 def 20 ref appTerm 19 ref appTerm appTerm 21 ref 19 ref appTerm 20 ref appTerm appTerm 22 def absTerm 23 def absTerm 24 def defineConst 25 def pop 16 remove constTerm 26 def 6 remove varTerm 27 def appTerm 9 remove varTerm 28 def appTerm appTerm 17 remove 18 remove 27 ref appTerm 28 ref appTerm appTerm 21 ref 28 ref appTerm 27 ref appTerm appTerm 21 remove 27 remove appTerm 28 remove appTerm appTerm appTerm absTerm appTerm absTerm 29 def nil cons cons nil cons nil cons cons "A" 15 remove cons nil cons nil nil cons cons 10 ref 0 ref 2 ref 0 ref 2 ref 3 ref cons opType nil cons cons opType constTerm 30 def 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 10 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 10 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 8 ref 14 ref 12 remove 26 remove 19 ref appTerm 20 ref appTerm appTerm 22 remove appTerm 41 def absTerm 42 def appTerm nil cons cons nil cons nil cons cons 30 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 25 remove 19 ref refl appThm 24 remove 19 remove appTerm betaConv trans 20 ref refl appThm 23 remove 20 remove appTerm betaConv trans eqMp absThm eqMp eqMp absThm eqMp nil 8 remove 29 remove appTerm thm