Certification Problem

Input (COPS 336)

The rewrite relation of the following conditional TRS is considered.

Property / Task

Answer / Result

Proof (by ConCon @ CoCo 2020)

1 Removal of Infeasible Rules

1.1 Rules with Infeasible Conditions

• 1.1.1 Rule with Infeasible Conditions

  The rule

  filter(n,r,cons(x,xs))

  →

  pair(x,xs)

  | eq(div(x,n),pair(q,r)) ≈ true

  has infeasible conditions.

  1.1.1.1 Infeasible Equation

  The equation is infeasible.

  1.1.1.1.1 Non-reachability

  We show non-reachability w.r.t. the underlying TRS.

  1.1.1.1.1.1 Non-reachability by TCAP

  Non-reachability is shown by the TCAP approximation.
  
  

• 1.1.2 Rule with Infeasible Conditions

  The rule

  filter(n,r,cons(x,xs))

  →

  pair(y,cons(x,ys))

  | filter(n,r,xs) ≈ pair(y,ys), eq(div(x,n),pair(q,r)) ≈ false

  has infeasible conditions.

  1.1.2.1 Infeasible Compound Conditions

  We collect the conditions in the fresh compound-symbol conds.

  1.1.2.1.1 Non-reachability

  We show non-reachability w.r.t. the underlying TRS.

  1.1.2.1.1.1 Non-reachability by TCAP

  Non-reachability is shown by the TCAP approximation.
  
  

1.2 Almost-orthogonal