%%-------------------** Term Rewriting System (TRS) **------------------------
%%                                                                          
%% Authors         : Andre Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%
%%                         and 
%%
%%                   Mauricio Ayala Rincon  
%%                   Universidade de Brasília - Brasil  
%%            
%% Last Modified On: September 29, 2009                                      
%%                                                                          
%%----------------------------------------------------------------------------


critical_pairs_aux[variable:TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY

 BEGIN

   ASSUMING
 
     IMPORTING variables_term[variable,symbol, arity],
               sets_aux@countability[term],
               sets_aux@countable_props[term]
 
       var_countable: ASSUMPTION is_countably_infinite(V)
      
   ENDASSUMING


     IMPORTING rewrite_rules[variable,symbol, arity],
               replace_positions[variable,symbol, arity]
 

          s, t, t1, t2: VAR term
      sigma, sg1, sg2, 
     sig, delta, alpha: VAR Sub
                   rho: VAR Ren 
           e1, e2, e2p: VAR rewrite_rule
                     E: VAR set[rewrite_rule]
                     R: VAR pred[[term, term]]
                     x: VAR (V)


 CP_lemma_aux2b: LEMMA
   FORALL R, t, x, sg1, sg2, (fstp: SPP(t)):
     LET Mtn = replace_pos(ext(sg1)(t), ext(sg2)(x), fstp) IN
     (FORALL (i: below[length(fstp)]): subtermOF(t,fstp(i)) = x) &
                                       comp_cont?(R) & 
                                       RSigma(R, sg1, sg2, x) 
                 => iterate(R, length(fstp))(ext(sg1)(t), Mtn)




 CP_lemma_aux2c1: LEMMA
   FORALL R, t, x, sg1, sg2, (fst: SPP(t)), (q: positions?(t)):
       ( FORALL (i: below[length(fst)]): parallel(fst(i),q)           &
                                          subtermOF(t, fst(i)) = x  ) &
                                          subtermOF(t, q) = x         &
                                          comp_cont?(R)               & 
                                          RSigma(R, sg1, sg2, x)
   => 
iterate(R, length(fst))(replace_pos(ext(sg1)(t), ext(sg2)(x), #(q)), 
                        replace_pos(ext(sg1)(t), ext(sg2)(x), add_first(q,fst)))



 CP_lemma_aux2c: LEMMA
   FORALL R, t, x, sg1, sg2, (fstp: SPP(t)):
     fstp`length /= 0 &
     ( FORALL (i: below[length(fstp)]): subtermOF(t,fstp(i)) = x  ) &
                                        comp_cont?(R) & 
                                        RSigma(R, sg1, sg2, x)
   => ( FORALL (i: below[length(fstp)]):
iterate(R, length(fstp) - 1)(replace_pos(ext(sg1)(t), ext(sg2)(x), #(fstp(i))), 
                             replace_pos(ext(sg1)(t), ext(sg2)(x), fstp))  )


 

CP_lemma_aux2d: LEMMA
   FORALL R, t, x, sg1, sg2:
     LET Posv = Pos_var(t, x),
         seqv = set2seq(Posv) IN
     comp_cont?(R) & 
     RSigma(R, sg1, sg2, x) 
        => replace_pos(ext(sg1)(t), ext(sg2)(x), seqv) = ext(sg2)(t)


END critical_pairs_aux