# File AS.dat.rb, line 115
115:    def initialize(functor, *args)
116:       @functor    = functor
117:       @args       = TermList.new( args )
118:       # 0.l "Creating #{self.html}"
119:    end

     # File AS.dat.rb, line 156
156:    def apply(substitution)
157:       Term.new( @functor, *@args.apply(substitution) )
158:    end

     # File AS.dat.rb, line 125
125:    def argument_tag
126:       @functor + '(' + @args.collect{ |x| x.argument_tag }.join(',') + ')'
127:    end

     # File AS.dat.rb, line 167
167:    def equal_modulo_variables?(t)
168:       t.is_a?(Term) or return false
169:       @functor==t.functor or return nil
170:       @args.zip(t.args).all? { |t1, t2| t1.equal_modulo_variables?(t2) }
171:    end

     # File AS.dat.rb, line 138
138:    def html
139:       body = @args.collect{ |x| x.html }.join(',')
140:       if @functor=='~' then
141:          '¬'.color('functor') + body
142:       else
143:          @functor.color('functor') + '(' + body + ')'
144:       end.color('term')
145:    end

     # File AS.dat.rb, line 129
129:    def inspect
130:       body = @args.collect{ |x| x.inspect }.join(',')
131:       if @functor=='~' then
132:          '~' + body
133:       else
134:          @functor + '(' + body + ')'
135:       end
136:    end

     # File AS.dat.rb, line 161
161:    def negation
162:       # double negation is formula itself
163:       @functor=='~' ? @args.at(0) : Term.new( '~', self )
164:    end

     # File AS.dat.rb, line 121
121:    def rule_tag
122:       @functor=='~' ? 'neg_'+@args[0].functor : @functor
123:    end

     # File AS.dat.rb, line 148
148:    def unify(t, s=Substitution.new)
149:       # deb.unif. $out += "#{__LINE__}: T : #{self.inspect} (#{self.class}) ~ #{t.inspect} (#{t.class})\n"
150:       t.is_a?(Variable) and return s.merge!( t.name => self )
151:       t.is_a?(Term) && @functor==t.functor or return nil
152:       return @args.unify(t.args, s)
153:    end