path: "vendor/opentheory/data/theories/monoid-comm-mult-def/monoid-comm-mult-def.art"
nil "Data.Bool.!" const 0 def "->" typeOp 1 def 1 ref "Algebra.Monoid.monoid" typeOp nil opType 2 def "bool" typeOp nil opType nil cons 3 def cons opType 4 def 3 ref cons opType constTerm 5 def "x" 2 ref var 6 def 0 remove 1 ref 1 ref "Number.Natural.natural" typeOp nil opType 7 def 3 ref cons opType 3 remove cons opType constTerm "n" 7 ref var 8 def "=" const 1 ref 2 ref 4 remove nil cons cons opType constTerm 9 def "Algebra.Monoid.*" const 1 ref 2 ref 1 ref 7 ref 2 ref nil cons 10 def cons opType nil cons cons opType constTerm 6 ref varTerm 11 def appTerm 12 def "Number.Natural.suc" const 1 ref 7 ref 7 ref nil cons cons opType constTerm 8 remove varTerm 13 def appTerm appTerm appTerm "Algebra.Monoid.+" const 1 ref 2 ref 1 remove 2 ref 10 remove cons opType nil cons cons opType constTerm 11 remove appTerm 12 ref 13 remove appTerm appTerm appTerm absTerm appTerm absTerm appTerm 14 def axiom nil 14 remove thm nil 5 remove 6 remove 9 remove 12 remove "Number.Natural.zero" const 7 remove constTerm appTerm appTerm "Algebra.Monoid.0" const 2 remove constTerm appTerm absTerm appTerm 15 def axiom nil 15 remove thm