class ADSL::DS::DSForEachPreLambdaObjset

Public Instance Methods

prepare_action(translation) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 555
def prepare_action(translation); end
resolve_action_objset(translation, ps, o) click to toggle source
# File lib/adsl/spass/spass_ds_extensions.rb, line 557
def resolve_action_objset(translation, ps, o)
  raise "Not implemented for flexible arities"
  translation.reserve_names :parent, :prev_context do |parent, prev_context|
    return FOL::ForAll.new(parent, FOL::Implies.new(@context.parent_of_pred[parent, :c],
      FOL::IfThenElseEq.new(
        @context.first[parent, c],
        @before_var[c, o],
        FOL::Exists.new( prev_context, FOL::And.new(
          @context.just_before[prev_context, c],
          @inside_var[prev_context, o]
        ))
      )
    ))
  end
end