path: "vendor/opentheory/data/theories/monoid-comm-mult-add/monoid-comm-mult-add.art"
6 version nil "Data.Bool.!" const 0 def "->" typeOp 1 def 1 ref "Algebra.Monoid.monoid" typeOp nil opType 2 def "bool" typeOp nil opType 3 def nil cons 4 def cons opType 5 def 4 ref cons opType constTerm 6 def "z" 2 ref var 7 def 6 ref "x" 2 ref var 8 def "=" const 1 ref 2 ref 5 remove nil cons cons opType constTerm 9 def "Algebra.Monoid.multAdd" const 1 ref 2 ref 1 ref 2 ref 1 ref "Data.List.list" typeOp 4 ref opType 10 def 2 ref nil cons 11 def cons opType nil cons cons opType nil cons cons opType constTerm 12 def 7 ref varTerm 13 def appTerm 8 ref varTerm 14 def appTerm 15 def "Data.List.[]" const 10 ref constTerm appTerm appTerm 13 ref appTerm absTerm appTerm absTerm appTerm 16 def axiom nil 16 remove thm nil 6 ref 8 ref 0 ref 1 ref 1 ref "Number.Natural.natural" typeOp nil opType 17 def 4 ref cons opType 4 ref cons opType constTerm "n" 17 ref var 18 def 9 ref 12 ref "Algebra.Monoid.0" const 2 ref constTerm appTerm 14 ref appTerm "Number.Natural.Bits.toList" const 1 ref 17 ref 10 ref nil cons 19 def cons opType constTerm 18 remove varTerm 20 def appTerm appTerm appTerm "Algebra.Monoid.*" const 1 ref 2 ref 1 ref 17 ref 11 ref cons opType nil cons cons opType constTerm 14 ref appTerm 21 def 20 remove appTerm appTerm absTerm appTerm absTerm appTerm 22 def axiom nil 22 remove thm nil 6 ref 7 ref 6 ref 8 ref 0 ref 1 ref 1 ref 10 ref 4 ref cons opType 4 ref cons opType constTerm 23 def "l" 10 ref var 24 def 9 ref 15 ref 24 remove varTerm 25 def appTerm appTerm "Algebra.Monoid.+" const 1 ref 2 ref 1 ref 2 remove 11 remove cons opType nil cons cons opType 26 def constTerm 27 def 13 ref appTerm 28 def 21 remove "Number.Natural.Bits.fromList" const 1 ref 10 ref 17 remove nil cons cons opType constTerm 25 remove appTerm appTerm appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 29 def axiom nil 29 remove thm nil 6 ref 7 remove 6 remove 8 remove 0 remove 1 ref 1 ref 3 ref 4 ref cons opType 4 remove cons opType constTerm "h" 3 ref var 30 def 23 remove "t" 10 ref var 31 def 9 remove 15 remove "Data.List.::" const 1 ref 3 ref 1 ref 10 remove 19 remove cons opType nil cons cons opType constTerm 30 remove varTerm 32 def appTerm 31 remove varTerm 33 def appTerm appTerm appTerm 12 remove "Data.Bool.cond" const 1 remove 3 remove 26 remove nil cons cons opType constTerm 32 remove appTerm 28 remove 14 ref appTerm appTerm 13 remove appTerm appTerm 27 remove 14 ref appTerm 14 remove appTerm appTerm 33 remove appTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm absTerm appTerm 34 def axiom nil 34 remove thm