úÎ'Ü&     (C) 2009 John D. RamsdellGPLSafe ÌThe ¯ function takes a list of integers that specifies the coefficients of linear Diophantine equation and a constant, and returns the equation's minimal, non-negative solutions.–When solving an inhomogeneous equation, the first element of a solution is zero if it solves the associated homogeneous equation, and one otherwise.!Thus to solve 2x + y - z = 2, use BlinDiophEq [2,1,-1] 2 = [[0,0,1,1],[1,1,0,0],[0,1,0,2],[1,0,2,0]] ÿ9The two minimal solutions to the homogeneous equation are [0,1,1] and [1,0,2], so any linear combinations of these solutions contributes to a solution. The solution that corresponds to [1,0,0] is x = w + 1, y = v, and z = v + 2w. The solution that corresponds to [0,2,0] is x = w, y = v + 2, and z = v + 2w.(C) 2009 John D. RamsdellGPLSafe%zÆA substitution maps variables into terms. For the show and read methods, the substitution is a list of maplets, and the variable and the term in each element of the list are separated by a colon.nAn equation is a pair of terms. For the show and read methods, the two terms are separated by an equal sign.ÿ9A term in a commutative monoid is represented by the identity element, or as the sum of factors. A factor is the product of a positive integer coefficient and a variable. No variable occurs twice in a term. For the show and read methods, zero is the identity element, the plus sign is the monoid operation.( represents the identity element (zero).ÂA variable is an alphabetic Unicode character followed by a sequence of alphabetic or numeric digit Unicode characters. The show method for a term works correctly when variables satisfy the  predicate.1Return a term that consists of a single variable.@Multiply every coefficient in a term by an non-negative integer. Add two terms. OReturn all variable-coefficient pairs in the term in ascending variable order.9Convert a list of variable-coefficient pairs into a term. <Construct a substitution from a list of variable-term pairs. ;Return all variable-term pairs in ascending variable order. 7Return the result of applying a substitution to a term.Given  (t0, t1), return a most general substitution s such that s(t0) = s(t1) modulo the equational axioms of a commutative monoid.         cmu-1.11-3qRycQl6tgD6FDtDRqIA1g$Algebra.CommutativeMonoid.LinDiophEq%Algebra.CommutativeMonoid.Unification linDiophEq SubstitutionEquationTermideisVarvarmuladdassocssubstmapletsapplyunify $fReadTerm $fShowTerm$fReadEquation$fShowEquation$fReadSubstitution$fShowSubstitution $fReadMaplet $fShowMaplet$fEqTerm $fEqEquation$fEqSubstitution $fEqMaplettermMaplet