Certification Problem

Input (COPS 806)

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

  b

  →

  d

  | d ≈ x, e ≈ x

  has infeasible conditions.

  1.1.1.1 Infeasible Compound Conditions

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

  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

  c

  →

  d

  | d ≈ x, e ≈ x

  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 Quasi-reductive SDTRS where all CCPs are joinable

1.2.1 Quasi-Reductive CTRS

1.2.1.1 Unraveling

To prove that the CTRS is quasi-reductive, we show termination of the following unraveled system.

1.2.1.1.1 Bounds

• final states:

  {23, 21, 20, 14, 13, 10, 9, 6}

• transitions:

  c3	→	20
  c2	→	13
  a0	→	6
  a1	→	6
  b1	→	10
  c1	→	9
  U21(9,20)	→	6
  U21(9,13)	→	6
  U21(9,9)	→	6
  U21(13,13)	→	6
  U21(23,23)	→	6
  U21(13,23)	→	6
  U21(9,23)	→	6
  U21(23,6)	→	6
  U21(20,23)	→	6
  U21(23,21)	→	6
  U21(23,9)	→	6
  U21(9,21)	→	6
  U21(13,14)	→	6
  U21(20,10)	→	6
  U21(13,21)	→	6
  U21(20,21)	→	6
  U21(23,14)	→	6
  U21(9,14)	→	6
  U21(20,20)	→	6
  U21(13,20)	→	6
  U21(20,13)	→	6
  U21(13,9)	→	6
  U21(13,10)	→	6
  U21(20,6)	→	6
  U21(13,6)	→	6
  U21(9,10)	→	6
  U21(9,6)	→	6
  U21(20,14)	→	6
  U21(23,20)	→	6
  U21(23,10)	→	6
  U21(23,13)	→	6
  U21(20,9)	→	6
  U20(23,21)	→	6
  U20(23,14)	→	6
  U20(20,21)	→	6
  U20(10,13)	→	6
  U20(13,13)	→	6
  U20(20,13)	→	6
  U20(9,13)	→	6
  U20(23,20)	→	6
  U20(23,13)	→	6
  U20(6,10)	→	6
  U20(14,9)	→	6
  U20(13,10)	→	6
  U20(6,9)	→	6
  U20(10,9)	→	6
  U20(9,21)	→	6
  U20(10,21)	→	6
  U20(9,23)	→	6
  U20(13,9)	→	6
  U20(14,6)	→	6
  U20(13,21)	→	6
  U20(9,20)	→	6
  U20(9,6)	→	6
  U20(9,9)	→	6
  U20(23,23)	→	6
  U20(9,10)	→	6
  U20(21,14)	→	6
  U20(14,14)	→	6
  U20(9,14)	→	6
  U20(20,9)	→	6
  U20(10,10)	→	6
  U20(14,13)	→	6
  U20(6,23)	→	6
  U20(10,23)	→	6
  U20(6,13)	→	6
  U20(10,6)	→	6
  U20(13,6)	→	6
  U20(21,10)	→	6
  U20(20,14)	→	6
  U20(21,13)	→	6
  U20(20,23)	→	6
  U20(14,21)	→	6
  U20(10,20)	→	6
  U20(13,20)	→	6
  U20(13,14)	→	6
  U20(21,21)	→	6
  U20(23,6)	→	6
  U20(20,6)	→	6
  U20(6,20)	→	6
  U20(14,10)	→	6
  U20(14,23)	→	6
  U20(23,10)	→	6
  U20(23,9)	→	6
  U20(6,6)	→	6
  U20(21,20)	→	6
  U20(20,20)	→	6
  U20(21,23)	→	6
  U20(10,14)	→	6
  U20(13,23)	→	6
  U20(6,21)	→	6
  U20(14,20)	→	6
  U20(6,14)	→	6
  U20(21,9)	→	6
  U20(21,6)	→	6
  U20(20,10)	→	6
  b2	→	14
  b0	→	6
  U23(20,14)	→	6
  U23(23,21)	→	6
  U23(23,14)	→	6
  U23(20,21)	→	6
  b3	→	21
  c0	→	6
  a2	→	6
  U22(23,14)	→	6
  U22(13,21)	→	6
  U22(20,21)	→	6
  U22(23,10)	→	6
  U22(13,10)	→	6
  U22(23,21)	→	6
  U22(20,10)	→	6
  U22(13,14)	→	6
  U22(20,14)	→	6
  U13(21)	→	6
  U24(23,21)	→	6
  U10(10)	→	6
  U10(6)	→	6
  U10(13)	→	6
  U10(20)	→	6
  U10(14)	→	6
  U10(21)	→	6
  U10(9)	→	6
  U10(23)	→	6
  U12(14)	→	6
  U12(21)	→	6
  c4	→	23
  U11(21)	→	6
  U11(14)	→	6
  U11(10)	→	6

1.2.2 All CCPs are joinable