products/sources/formale Sprachen/Isabelle/HOL/Bali image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: orthogonality.pvs   Sprache: PVS

%%-------------------** Term Rewriting System (TRS) **------------------------
%%                                                                          
%% Authors         : Ana Cristina Rocha Oliveira, Andre Galdino and Mauricio Ayala Rincon  
%%                   Universidade de Brasília - Brasil         
%% Orthogonality theory formalizing confluence of orthogonal rewriting systems
%% subtheories mem_test and mem_tes2 specify properties between finite sequences
%% and associated sets that are necessary for dealing adequately with sequences
%% of positions, rules and substitutions involved in parallel rewriting steps.
%% The theory orthogonality is the main one.
%%
%% Last Modified On: June 28, 2013                                    
%%                                                                          
%%--------------------------------------------------------------------------

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% mem_test is an auxiliary theory formalising properties related with length and
%% cardinality and membership of elements in finite_sequences and associated sets.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
mem_test[T: TYPE] : THEORY
BEGIN
       IMPORTING   structures@seq_extras[T],
                   structures@seq2set[T]

              x : VAR T
 seq, seq1, seq2: VAR finseq[T]
              E : VAR set[T]
              n : VAR nat
              P : VAR [[T, T] -> bool]
             P1 : VAR [[nat, T] -> bool]
     
 member_seq(x, seq): bool =
     EXISTS(i:below[seq`length]): x = seq(i)

 subseq(seq1, seq2): bool =
     FORALL(i:below[seq1`length]): member_seq(seq1(i),seq2)

  member(seq, E): bool = FORALL(i:below[seq`length]):
                         member(seq`seq(i),E)

  power(x,n): finseq[T] =
     (# length := n,
           seq := (LAMBDA(i:below[n]): x) #)

 member_seq_in_seq2set: LEMMA
    member_seq(x, seq) IFF seq2set(seq)(x)

 subseq_rest: LEMMA
    subseq(seq1, rest(seq2)) IMPLIES subseq(seq1, seq2)

 seq2set_comp: LEMMA
    seq2set(seq1 o seq2)(x)
    IFF seq2set(seq1)(x) OR seq2set(seq2)(x)

  seq_construct: LEMMA
    seq1`length = n &
    seq2`length = n &
    (FORALL (i:below[n]):
      EXISTS x: P(seq1`seq(i), x) & 
                P(seq2`seq(i), x))
    IMPLIES EXISTS seq: seq`length = n &
      FORALL (i:below[n]):
              P(seq1`seq(i), seq`seq(i)) & 
              P(seq2`seq(i), seq`seq(i))

  seq_construct2: LEMMA
    (FORALL (i:below[n]):
      EXISTS x: P1(i, x))
    IMPLIES EXISTS seq: seq`length = n &
      FORALL (i:below[n]):
              P1(i, seq`seq(i))

END mem_test

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Orthogonality contains specification of notions related with orthogonal
%% rewriting systems, parallel rewriting and the formalization of theorems
%% of confluence of left and right linear non-ambiguous TRSs and the main 
%% theorem of confluence of orthogonal TRSs.
%% The inductive proof of the main theorem uses the Parallel Moves Lemma. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

orthogonality[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 critical_pairs[variable,symbol,arity],
              mem_test[term],
              mem_test[position],
              mem_test[rewrite_rule],
              mem_test[Sub]       
                                       
                               n: VAR nat
                    s, t, t1, t2: VAR term 
   sigma, sg1, sg2, alpha, delta, theta: VAR Sub
              p,q,p1,p2,p3,q1,q2: VAR position
                 rho, rho1, rho2: VAR Ren 
   e, e1o, e2o, e1, e1p, e2, e2p: VAR rewrite_rule
                               E: VAR set[rewrite_rule]
                               R: VAR pred[[term, term]]
                            x, y: VAR (V)
            fsq, fsp, fsp1, fsp2: VAR finseq[position]
                 fse, fse1, fse2: VAR finseq[rewrite_rule]
                 fss, fss1, fss2: VAR finseq[Sub]
                             fsv: VAR finseq[(V)]
                 fst, fst1, fst2: VAR finseq[term]
                    PO1, PO2, PE: VAR PP
 
%%%% Basic specific definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% ntCP? is the predicate for non trivially generated CPs %%%%%%%%%%%%%%%%%%%%%%%%
%%%%% This in contrast with CP? excludes all CPs generated by sobreposition of %%%%%%
%%%%% a rule with itself at root position and is used to define ambiguity.     %%%%%%
%%%%% The necessity of this notion was gently pointed out by Rene Thiemann.    %%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  ntCP?(E)(t1, t2): bool =
    EXISTS (sigma,rho,
           (e1 | member(e1, E)),
           (e2p | member(e2p, E)),
           (p: positions?(lhs(e1)))):
         NOT (e1 = e2p AND p = empty_seq) AND
         LET e2 = (# lhs := ext(rho)(lhs(e2p)), rhs := ext(rho)(rhs(e2p)) #) IN
               disjoint?(Vars(lhs(e1)),Vars(lhs(e2)))                        &
               NOT vars?(subtermOF(lhs(e1), p))                              &
               mgu(sigma)(subtermOF(lhs(e1), p), lhs(e2))                    &
               t1 = ext(sigma)(rhs(e1))                                      &
               t2 = replaceTerm(ext(sigma)(lhs(e1)), ext(sigma)(rhs(e2)), p)

 ntCP_lemma_aux1: LEMMA
   FORALL E, (p: position), (e1 | member(e1, E)), (e2 | member(e2, E)):
    ( ( positionsOF(lhs(e1))(p) &
       NOT vars?(subtermOF(lhs(e1), p))                                     &
       ext(sg1)(subtermOF(lhs(e1), p)) = ext(sg2)(lhs(e2)) )                &
       NOT (e1 = e2 AND p = empty_seq) )
          =>
           EXISTS t1, t2, delta:
             ntCP?(E)(t1, t2)                                               &
             ext(delta)(t1) = ext(sg1)(rhs(e1))                             &
             ext(delta)(t2) = replaceTerm(ext(sg1)(lhs(e1)), ext(sg2)(rhs(e2)), p)

 Ambiguous?(E): bool =  EXISTS (t1, t2) : ntCP?(E)(t1,t2)

 linear?(t): bool = FORALL (x | member(x,Vars(t))) : Card[position](Pos_var(t,x)) = 1 

 Right_Linear?(E): bool = FORALL (e1 | member(e1, E)) : linear?(rhs(e1))   

 Left_Linear?(E): bool = FORALL (e1 | member(e1, E)) : linear?(lhs(e1))   

 Linear?(E): bool = Left_Linear?(E) AND Right_Linear?(E)

 
 local_joinability_triangle?(R) : bool = FORALL(t, t1, t2) : R(t, t1) & R(t, t2) =>
               EXISTS s : (RC(R)(t1, s) & RC(R)(t2, s))


%%%% Some Lemmas %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 Orth_lemma_aux0 : LEMMA
  Card(Pos_var(t, x)) = 1  => EXISTS (p1) : (positionsOF(t)(p1) AND subtermOF(t,p1) = x )
 
 equality_replaceTerm : LEMMA 
  positionsOF(s)(p) =>
  (t1 = t2 iff replaceTerm(s, t1, p) =  replaceTerm(s, t2, p))


 Var_occurs_only_once_also_in_subterms : LEMMA
  vars?(x) & positionsOF(s)(p) & p`length /= 0 &
  x = subtermOF(s, p) &
  card(Pos_var(s,x)) = 1   => 
      card(Pos_var(subtermOF(s, #(first(p))),x)) = 1 
 

 SigmaP_equivalence : LEMMA 
  (NOT member(x, Vars(s)) &
  positionsOF(ext(sigma)(x))(p2))
      =>   ext(SigmaP(sigma, t, x, p2))(s) = ext(sigma)(s)


 SigmaP_vs_replaceTerm_linearR : LEMMA
  vars?(x) & positionsOF(s)(p1) &
  positionsOF(ext(sigma)(x))(p2) &
  x = subtermOF(s, p1) &
  Card(Pos_var(s,x)) = 1   => 
      ext(SigmaP(sigma, t, x, p2))(s) =
         replaceTerm( ext(sigma)(s), t, p1 o p2)
 
 Orth_lemma_aux: LEMMA
     LET e1o = (# lhs := ext(rho1)(lhs(e1p)), rhs := ext(rho1)(rhs(e1p)) #) IN
       LET e2o = (# lhs := ext(rho2)(lhs(e2p)), rhs := ext(rho2)(rhs(e2p)) #) IN
       member(e1p,E) & 
       member(e2p,E) &
       positionsOF(t)(p1) &
       positionsOF(t)(p3) &
       NOT Ambiguous?(E) &
       p3 = p1 o p2 &
       Linear?(E) &
         subtermOF(t, p1) = ext(sg1)(lhs(e1o)) & 
         t1 = replaceTerm(t, ext(sg1)(rhs(e1o)), p1) &
         subtermOF(t, p3) = ext(sg2)(lhs(e2o)) &
         t2 = replaceTerm(t, ext(sg2)(rhs(e2o)), p3) &
         disjoint?(Vars(lhs(e1o)),Vars(t))&
         disjoint?(Vars(lhs(e2o)),Vars(t))
   =>
     EXISTS s:  (RC(reduction?(E))(t1, s) & RC(reduction?(E))(t2, s))

 Linear_and_Non_ambiguous_implies_triangle: LEMMA
  FORALL (E) :  
    (Linear?(E) AND NOT Ambiguous?(E) ) IMPLIES
     local_joinability_triangle?(reduction?(E))

 Triangle_implies_conflent: LEMMA
        local_joinability_triangle?(R)
        IMPLIES confluent?(R)

 Linear_and_Non_ambiguous_implies_confluent: LEMMA
  FORALL (E) :  
    ((Linear?(E) AND NOT Ambiguous?(E) ) IMPLIES
     confluent?(reduction?(E)))
 


%%%% More definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 Orthogonal?(E): bool =  Left_Linear?(E) & NOT Ambiguous?(E)

 Orthogonal: TYPE = (Orthogonal?)


 replace_par_pos(s, (fsp : SPP(s)), fst | fst`length = fsp`length): RECURSIVE 
    term =
      IF length(fsp) = 0
       THEN 
        s
       ELSE
        replace_par_pos(replaceTerm(s, fst(0), fsp(0)), rest(fsp), rest(fst))
      ENDIF
   MEASURE length(fsp)

 reduction_fix?(E)(s,t,(p:positions?(s))): bool =
      EXISTS (e|member(e,E), sigma):
        subtermOF(s,p)=ext(sigma)(lhs(e))
          AND t=replaceTerm(s,ext(sigma)(rhs(e)),p)

 sigma_rhs(fss, (fse | fse`length = fss`length)): finseq[term] = 
     IF fss`length = 0 THEN empty_seq[term]
     ELSE
          (# length := fss`length,
                seq := (LAMBDA (i: below[fss`length]): ext(fss(i))(rhs(fse(i)))) #)
     ENDIF

 sigma_lhs(fss, (fse | fse`length = fss`length)): finseq[term] = 
     IF fss`length = 0 THEN empty_seq[term]
     ELSE
          (# length := fss`length,
                seq := (LAMBDA (i: below[fss`length]): ext(fss(i))(lhs(fse(i)))) #)
     ENDIF

  subtermsOF(t,(fsp:SP(t))): 
            finseq[term] = (# length := fsp`length,
                              seq := (LAMBDA (i: below[fsp`length]): subtermOF(t,fsp(i))) #);

 parallel_reduction_fix?(E)(s,t, (fsp: SPP(s))): bool =  
    EXISTS ((fse | member(fse, E)), fss) :
           fsp`length = fse`length AND fsp`length = fss`length
           AND subtermsOF(s,fsp) = sigma_lhs(fss, fse)
           AND t = replace_par_pos(s, fsp, sigma_rhs(fss, fse))

 parallel_reduction?(E)(s,t): bool =  EXISTS (fsp: SPP(s)): parallel_reduction_fix?(E)(s,t,fsp)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 sub_pos((fsp : PP), p): RECURSIVE finseq[position] =
     IF  length(fsp) = 0 THEN empty_seq[position]
        ELSIF p <= fsp`seq(0) AND p /= fsp`seq(0)
                THEN add_first(fsp`seq(0), sub_pos(rest(fsp), p))
                ELSE sub_pos(rest(fsp), p)
     ENDIF
    MEASURE length(fsp)

% Positions of fsp1 that have positions of fsp2 strictly below or are parallel to fsp2
 Pos_Over((fsp1 : PP), (fsp2 : PP)): RECURSIVE finseq[position] =
   (IF length(fsp1) = 0
       THEN empty_seq[position]
       ELSE (IF ( length(sub_pos(fsp2, fsp1`seq(0))) > 0  
                 OR PP?(add_first(fsp1`seq(0), fsp2)))
                THEN add_first(fsp1`seq(0), Pos_Over(rest(fsp1), fsp2))
                ELSE Pos_Over(rest(fsp1), fsp2)
             ENDIF)
     ENDIF)
    MEASURE length(fsp1)

% Positions of fsp1 that are strictly below some position of fsp2.

 Pos_Under((fsp1 : PP), (fsp2 : PP)): RECURSIVE finseq[position] =
     IF length(fsp2)=0
        THEN empty_seq[position]
        ELSE sub_pos(fsp1, fsp2`seq(0)) o Pos_Under(fsp1,rest(fsp2))
     ENDIF
   MEASURE length(fsp2)

% Positions of fsp1 and fsp2

 Pos_Equal((fsp1 : PP), (fsp2 : PP)): RECURSIVE finseq[position] =
     IF length(fsp1) = 0 THEN empty_seq[position]
     ELSIF member_seq(fsp1`seq(0),fsp2)
     THEN add_first(fsp1`seq(0), Pos_Equal(rest(fsp1), fsp2))
     ELSE Pos_Equal(rest(fsp1), fsp2)
     ENDIF
  MEASURE length(fsp1)

%%%% Lemmas about parallel reduction %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 comp_SPP_commute: LEMMA
    SPP?(s)(fsp1 o fsp2) IMPLIES SPP?(s)(fsp2 o fsp1)

 sub_pos_element: LEMMA
    PP?(fsp) & member_seq(p1 o p2, fsp) & p2`length /= 0
    IMPLIES sub_pos(fsp, p1)`length /= 0 & 
            member_seq(p1 o p2, sub_pos(fsp, p1))

 parallel_pos_are_dif: LEMMA
    PP?(fsp) IMPLIES FORALL(i,j: below[fsp`length]): i /= j => fsp(i) /= fsp(j)

 same_pos_in_Pos_Equal: LEMMA
    PP?(fsp1) & PP?(fsp2) & member_seq(p, fsp1) & member_seq(p, fsp2)
    IMPLIES member_seq(p, Pos_Equal(fsp1, fsp2))

 Pos_Over_is_sub_seq: LEMMA
    PP?(fsp1) & PP?(fsp2)
     IMPLIES subseq(Pos_Over(fsp1,fsp2), fsp1)

 Pos_Equal_is_sub_seq: LEMMA
    PP?(fsp1) & PP?(fsp2)
    IMPLIES subseq(Pos_Equal(fsp1,fsp2),fsp1)
 
 sub_pos_is_sub_seq: LEMMA
    PP?(fsp) IMPLIES subseq(sub_pos(fsp,p), fsp)
 
 Pos_Under_is_sub_seq: LEMMA
    PP?(fsp1) & PP?(fsp2)
    IMPLIES subseq(Pos_Under(fsp1,fsp2), fsp1)

 Pos_Over_is_PP: LEMMA
    PP?(fsp1) & PP?(fsp2) IMPLIES
    PP?(Pos_Over(fsp1, fsp2))

 Pos_Over_is_SPP: LEMMA 
    SPP?(s)(fsp1) & SPP?(s)(fsp2) IMPLIES
    SPP?(s)(Pos_Over(fsp1, fsp2))

 pos_up_in_Pos_Over: LEMMA
    PP?(fsp1) & PP?(fsp2) &
    p2`length /= 0 & member_seq(p1, fsp1) & member_seq(p1 o p2, fsp2)
    IMPLIES member_seq(p1, Pos_Over(fsp1, fsp2))

 parallel_pos_in_Pos_Over:  LEMMA    
    PP?(fsp1) & PP?(fsp2) & member_seq(p, fsp1) & PP?(add_first(p, fsp2))
    IMPLIES member_seq(p, Pos_Over(fsp1, fsp2))

 sub_pos_in_Pos_Under_aux: LEMMA
    PP?(fsp) & member_seq(p2, fsp) &
    p1 /= p2 & p1 <= p2 IMPLIES
    member_seq(p2, sub_pos(fsp,p1))
    
 sub_pos_in_Pos_Under: LEMMA
    PP?(fsp1) & PP?(fsp2) & member_seq(p1, fsp1) &
    member_seq(p2, fsp2) & p1 /= p2 & p2 <= p1 IMPLIES
      member_seq(p1, Pos_Under(fsp1, fsp2))

 sub_pos_is_under: LEMMA
    PP?(fsp) & member_seq(p1, sub_pos(fsp,p))
      IMPLIES p<=p1 & p/=p1

 sub_pos_is_PP: LEMMA
    PP?(fsp) IMPLIES PP?(sub_pos(fsp,p))

 sub_pos_is_SPP: LEMMA
    SPP?(s)(fsp) IMPLIES SPP?(s)(sub_pos(fsp,p))

 Pos_Under_character: LEMMA
    PP?(fsp1) & PP?(fsp2) & member_seq(p, Pos_Under(fsp1,fsp2))
     IMPLIES  EXISTS(j:below[fsp2`length]):
           member_seq(p, sub_pos(fsp1,fsp2(j)))

 union_positions: LEMMA 
    PP?(fsp1) & PP?(fsp2) IMPLIES
    seq2set(fsp1) = seq2set(Pos_Over(fsp1, fsp2) o Pos_Equal(fsp1, fsp2) o Pos_Under(fsp1, fsp2))

%% Auxiliary lemma on sigma_rhs.
 sigma_rhs_rest: LEMMA
     fse`length = fss`length 
        IMPLIES rest(sigma_rhs(fss, fse)) = sigma_rhs(rest(fss), rest(fse))

%% Auxiliary lemma on sigma_rhs. 
 sigma_rhs_o: LEMMA
   fse1`length = fss1`length AND fse2`length = fss2`length
     IMPLIES
       sigma_rhs(fss1 o fss2, fse1 o fse2) = sigma_rhs(fss1, fse1) o sigma_rhs(fss2, fse2)

%% Auxiliary lemma on subtermsOF.
 subtermsOF_rest: LEMMA
     SP?(t)(fsp) IMPLIES rest(subtermsOF(t,fsp)) = subtermsOF(t, rest(fsp))

% Lemma of inclusions of the rewriting relation in the parallel rewriting relation
% and the latter in the reflexive-transitive closure of the former relation.
 parallel_reduction_inclusion: LEMMA 
  subset?(reduction?(E), parallel_reduction?(E)) 
   & subset?(parallel_reduction?(E), RTC(reduction?(E)))

% The reflexive-transitive clousures of the rewriting and the parallel 
% rewriting relations are equivalent.
 parallel_reduction_RTC: LEMMA
  RTC(reduction?(E)) = RTC(parallel_reduction?(E))

% Once you rewrite in parallel at positions fsp which are
% parallel to position p ("p || fsp"), a term in which position p is 
% preserved is obtained.
 replace_par_pos_preservs_pos: LEMMA
  SPP?(t)(add_first(p,fsp)) AND fst`length = fsp`length
        => positionsOF(replace_par_pos(t, fsp, fst))(p)

% When you replace the subterms at the positions in fsp,
% those positions are preserved in the resulting term.
  replace_par_pos_preservs_PP: LEMMA
   SPP?(t)(fsp) AND fst`length = fsp`length
         => (FORALL (i : below[fsp`length]) : positionsOF(replace_par_pos(t, fsp, fst))(fsp(i)))

% Same of replace_par_pos_preserv_pos but instead for
% a unique position p || fsp for a sequence of positions fsq || fsp.
 replace_par_pos_preservs_PP_o_PP: LEMMA
  SPP?(t)(fsp o fsq ) AND fst`length = fsp`length
        => (FORALL (i : below[fsq`length]) : positionsOF(replace_par_pos(t, fsp, fst))(fsq(i)))

% If you replace the first parallel position firstly or lastly,
% that does not change the resulting term.
 replace_par_pos_equivalence: LEMMA
  SPP?(s)(fsp) AND fsp`length /= 0 AND fst`length = fsp`length
    => replace_par_pos(replaceTerm(s, fst(0), fsp(0)), rest(fsp), rest(fst)) = 
            replaceTerm(replace_par_pos(s, rest(fsp), rest(fst)), fst(0), fsp(0))

% Generalization of the previous result: you can pick up any position to start to work
% with replace_par_pos and that does not change the result.
 replace_par_pos_equivalence1: LEMMA
  SPP?(s)(fsp) AND fsp`length /= 0 AND fst`length = fsp`length AND n < fsp`length
    => replace_par_pos(replaceTerm(s, fst(n), fsp(n)), delete(fsp,n), delete[term](fst,n)) 
            replace_par_pos(s,fsp,fst)

% If you apply replace_par_pos in positions fsp, then the subterm
% at any position p || fsp is preserved.
 replace_par_pos_preservs_subterm: LEMMA
  SPP?(t)(add_first(p,fsp)) AND fst`length = fsp`length
        => subtermOF(replace_par_pos(t, fsp, fst), p) = subtermOF(t, p)

% When one rewrites in parallel at fsp, the subterms of the resulting term
% at fsp are exatly the terms in fst.
  replace_par_pos_subterm: LEMMA
    SPP?(t)(fsp) AND fst`length = fsp`length
         => (FORALL (i : below[fsp`length]) : subtermOF(replace_par_pos(t, fsp, fst),fsp(i))=fst(i))

% If you replace the subterms at a composition of sequences 'fsp1 o fsp2',
% that are parallel, it is the same that doing it separately.
 replace_par_pos_comp: LEMMA
  SPP?(t)(fsp1 o fsp2) AND fst1`length = fsp1`length
                       AND fst2`length = fsp2`length
         => replace_par_pos(t, fsp1 o fsp2, fst1 o fst2) =
                        replace_par_pos(replace_par_pos(t, fsp1, fst1),fsp2, fst2)

%% In general, applying replace_par_pos at a parallel composition of sequences
%% fsp1 o fsp2 is commutative.
 replace_par_pos_comp_commute: LEMMA
    SPP?(t)(fsp1 o fsp2) AND fst1`length = fsp1`length AND fst2`length = fsp2`length
      IMPLIES 
        replace_par_pos(t, fsp1 o fsp2, fst1 o fst2) = 
                                              replace_par_pos(t, fsp2 o fsp1, fst2 o fst1)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 complement_pos_set(p1,p): set[position] = 
         IF p1 <= p & p1 /= p 
           THEN {p2 | p=p1 o p2}
           ELSE emptyset
         ENDIF

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 complement_pos(p,(fsp:PP)):
       RECURSIVE finseq[position] = 
           IF length(fsp)=0 THEN empty_seq
           ELSIF nonempty?(complement_pos_set(p,fsp`seq(0)))
              THEN add_first(choose(complement_pos_set(p,fsp`seq(0))),
                             complement_pos(p,rest(fsp)))
              ELSE complement_pos(p,rest(fsp))
           ENDIF
       MEASURE(length(fsp))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 parallel_pos_same_prefix: LEMMA
    parallel(p1,p2) & p1= p o q1 & p2= p o q2
     IMPLIES parallel(q1,q2)

 complement_pos_character: LEMMA
    PP?(fsp) & member_seq(p1, complement_pos(p,fsp))
     IMPLIES EXISTS (i:below[fsp`length]):
             fsp`seq(i)= p o p1

 complement_pos_is_PP: LEMMA
    PP?(fsp) IMPLIES PP?(complement_pos(p,fsp))

 complement_pos_preservs_sub_pos_length1: LEMMA
   PP?(fsp) IMPLIES
  complement_pos(p, fsp)`length = sub_pos(fsp, p)`length

 complement_pos_empty: LEMMA
   PP?(add_first(p, fsp)) => complement_pos(p, fsp)`length = 0

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 comp_pos(p,fsp): finseq[position] = (# length := fsp`length,
                                              seq := (LAMBDA (i: below[fsp`length]): p o fsp(i)) #);

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 comp_preservs_parallel_pos: LEMMA
     parallel(p1,p2) IMPLIES parallel(p o p1,p o p2)

 comp_preservs_parallel_pos2: LEMMA
    parallel(p1,p2) IMPLIES parallel(p1 o q1,p2)

 comp_preservs_parallel_pos3: LEMMA
    parallel(p1,p2) IMPLIES parallel(p1 o q1,p2 o q2)

 comp_pos_rest: LEMMA
     comp_pos(p,rest(fsp)) = rest(comp_pos(p,fsp))

 comp_pos_preservs_length: LEMMA
     comp_pos(p, fsp)`length=fsp`length

 comp_pos_character: LEMMA
     FORALL(i:below[fsp`length]):
     comp_pos(p,fsp)`seq(i)= p o fsp`seq(i)

 comp_pos_is_PP: LEMMA
     PP?(fsp) IMPLIES PP?(comp_pos(p,fsp))

%% Replacing at the position q of t by the result of replacing in parallel at positions fsp of s
%% gives as result the same as replacing at positions q o fsp of t[q<-s].
 replace_replace_par_pos: LEMMA
    positionsOF(t)(q) AND SPP?(s)(fsp) AND fst`length = fsp`length
       IMPLIES
       replaceTerm(t, replace_par_pos(s,fsp,fst), q) = replace_par_pos(replaceTerm(t,s,q), comp_pos(q,fsp), fst)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 complement_pos_preservs_sub_pos_length: LEMMA
   PP?(fsp) IMPLIES 
    complement_pos(p1,complement_pos(p, fsp))`length
       = sub_pos(fsp, p o p1)`length

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 Pos_Over_character: LEMMA
     PP?(fsp1) & PP?(fsp2)
       => FORALL (i:below[Pos_Over(fsp1,fsp2)`length]):
            PP?(add_first(Pos_Over(fsp1,fsp2)`seq(i),fsp2))
             OR  EXISTS (j:below[fsp2`length]):
                         Pos_Over(fsp1,fsp2)`seq(i) <= fsp2`seq(j)
                         & Pos_Over(fsp1,fsp2)`seq(i) /= fsp2`seq(j)

 Pos_Equal_character: LEMMA
     PP?(fsp1) & PP?(fsp2) 
       => FORALL (i:below[Pos_Equal(fsp1,fsp2)`length]):
             EXISTS (j:below[fsp2`length]):
                     Pos_Equal(fsp1,fsp2)`seq(i) = fsp2`seq(j)

 Pos_Equal_is_PP: LEMMA
     PP?(fsp1) & PP?(fsp2)
       => PP?(Pos_Equal(fsp1, fsp2))
            
 Pos_Over_and_Pos_Equal_is_PP: LEMMA
     PP?(fsp1) & PP?(fsp2)
       => PP?(Pos_Over(fsp1, fsp2) o Pos_Over(fsp2, fsp1) o Pos_Equal(fsp1,fsp2))


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  comp_pos_in_SP_preservs_SP_in_replace: LEMMA
    SPP?(t)(fsp) & SP?(s)(fsp1) & fsp`length > 0 IMPLIES
     SP?(replaceTerm(t, s, fsp`seq(0)))(comp_pos(fsp`seq(0), fsp1) o rest(fsp))

  comp_pos_in_PP_preservs_PP: LEMMA
    PP?(fsp) & PP?(fsp1) & fsp`length > 0 IMPLIES
     PP?(comp_pos(fsp`seq(0), fsp1) o rest(fsp))

  comp_pos_in_SPP_preservs_SPP_in_replace: LEMMA
    SPP?(t)(fsp) & SPP?(s)(fsp1) & fsp`length > 0 IMPLIES
     SPP?(replaceTerm(t, s, fsp`seq(0)))(comp_pos(fsp`seq(0), fsp1) o rest(fsp))

  comp_pos_in_SPP_preservs_SPP_in_replace_par_pos: LEMMA
    SPP?(t)(fsp) & fsp`length=fst`length & fsp`length /= 0 &
    SPP?(fst`seq(0))(fsp1) &
    SPP?(replace_par_pos(t, fsp, fst))(fsp2) &
    PP?(add_first(fsp`seq(0),fsp2)) IMPLIES
     SPP?(replace_par_pos(t, fsp, fst))(comp_pos(fsp`seq(0), fsp1) o fsp2)

  parallel_reduction_reflexive: LEMMA reflexive?(parallel_reduction?(E))

  non_ambiguous_implies_same_term: LEMMA
       NOT Ambiguous?(E) & positionsOF(s)(p) &
       reduction_fix?(E)(s,t1,p) &
       reduction_fix?(E)(s,t2,p)
         IMPLIES t1 = t2

  parallel_reduction_context_aux2: LEMMA   
    SPP?(t)(fsp) AND fst1`length = fsp`length AND fst2`length = fsp`length AND
    (FORALL (i : below[fsp`length]): parallel_reduction?(E)(fst1(i),fst2(i)))
        IMPLIES EXISTS (fsq:SPP(replace_par_pos(t, fsp, fst1))):
           parallel_reduction_fix?(E)(replace_par_pos(t, fsp, fst1),replace_par_pos(t, fsp, fst2), fsq)
            AND (FORALL(p:positions?(t)): PP?(add_first(p,fsp)) => PP?(add_first(p,fsq)))

  parallel_reduction_context: LEMMA
    SPP?(t)(fsp) AND fst1`length = fsp`length AND fst2`length = fsp`length AND
    (FORALL (i : below[fsp`length]): parallel_reduction?(E)(fst1(i),fst2(i)))
        IMPLIES 
           parallel_reduction?(E)(replace_par_pos(t, fsp, fst1),replace_par_pos(t, fsp, fst2))

  replace_par_pos_of_app_is_app: LEMMA
    app?(t) & SPP?(t)(fsp) & fst`length = fsp`length IMPLIES
     fsp = #(empty_seq) OR
          app?(replace_par_pos(t, fsp, fst))

  replace_par_pos_preservs_f: LEMMA
    app?(t) & SPP?(t)(fsp) & fst`length = fsp`length IMPLIES
     fsp = #(empty_seq) OR
       f(t) = f(replace_par_pos(t,fsp,fst))

  parallel_reduction_closed_subs: LEMMA
    (FORALL (x: Vars?(t)): parallel_reduction?(E)(ext(sigma)(x), ext(theta)(x)))
      IMPLIES
        parallel_reduction?(E)(ext(sigma)(t), ext(theta)(t))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  compo_sufix(fsp:PP, p): 
      finseq[position] = (# length := fsp`length,
                               seq := (LAMBDA(i:below[fsp`length]): fsp`seq(i) o p) #)

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  parallel_reduction_result: LEMMA
     Orthogonal?(E) & E(e) & SPP?(ext(sigma)(lhs(e)))(fsp) &
     parallel_reduction_fix?(E)(ext(sigma)(lhs(e)), t, fsp)
       IMPLIES
          fsp = #(empty_seq) OR
          EXISTS(theta): t = ext(theta)(lhs(e))

  replace_par_pos_subterm2: LEMMA
      SPP?(s)(fsp) & member_seq(p1, fsp) &
      p <= p1 & p /= p1 &
      fsp`length = fst`length IMPLIES
        EXISTS fst1 : (complement_pos(p, fsp)`length = fst1`length &
          subtermOF(replace_par_pos(s, fsp, fst), p) =
                 replace_par_pos(subtermOF(s, p), complement_pos(p, fsp), fst1))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  C(e, sigma, s, t, (p|positionsOF(s)(p) & positionsOF(t)(p))): bool = 
        subtermOF(s, p) = ext(sigma)(lhs(e)) AND
        subtermOF(t, p) = ext(sigma)(rhs(e))

  D(s, t, (fsp|SPP?(s)(fsp) & SPP?(t)(fsp)), E)(i:below[fsp`length], e): bool =
           member(e, E) &
            EXISTS sigma : C(e, sigma, s, t, fsp`seq(i))

  G(s, t, (fsp|SPP?(s)(fsp) & SPP?(t)(fsp)),E)(i:below[fsp`length], sigma): bool =
            EXISTS (e|member(e, E)) : C(e, sigma, s, t, fsp`seq(i))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  parallel_reduction_variables: LEMMA
   NOT Ambiguous?(E) & E(e) &
    SPP?(ext(sigma)(lhs(e)))(fsp) &
    parallel_reduction_fix?(E)(ext(sigma)(lhs(e)), ext(theta)(lhs(e)),fsp) &
    NOT fsp = #(empty_seq)    
      IMPLIES
        FORALL (x:Vars?(lhs(e))):
         parallel_reduction?(E)(ext(sigma)(x), ext(theta)(x))


  Parallel_Moves_Lemma: LEMMA
      Orthogonal?(E) & member(e,E) &
      parallel_reduction?(E)(ext(sigma)(lhs(e)), t)
      IMPLIES EXISTS s: parallel_reduction?(E)(ext(sigma)(rhs(e)),s) &
                        parallel_reduction?(E)(t,s)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  replace_par_pos_dominance: LEMMA
    SPP?(t)(fsp) & SPP?(t)(fsp1) & parallel_reduction_fix?(E)(t,s,fsp1) &
    (FORALL(i:below[fsp1`length]):
               EXISTS(j:below[fsp`length]):fsp`seq(j) <= fsp1`seq(i))
       IMPLIES s = replace_par_pos(t,fsp,subtermsOF(s,fsp))

  Pos_Over_and_Pos_Equal_dominance: LEMMA
    SPP?(t)(fsp1) & SPP?(t)(fsp2) IMPLIES
    (FORALL(i:below[fsp1`length]):
        EXISTS(j:below[(Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2))`length]):
         (Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2))`seq(j) <= fsp1`seq(i))

  divergence_in_Pos_Over_aux: LEMMA
     SPP?(t)(fsp2) &
     parallel_reduction_fix?(E)(t, t2, fsp2) &
     positionsOF(t)(p) &
     member_seq(p, Pos_Over( #(p), fsp2))
            => parallel_reduction_fix?(E)(subtermOF(t, p), subtermOF(t2, p), complement_pos(p, fsp2))

  divergence_in_Pos_Over: LEMMA
     SPP?(t)(fsp1) & SPP?(t)(fsp2) &
     parallel_reduction_fix?(E)(t, t1, fsp1) &
     parallel_reduction_fix?(E)(t, t2, fsp2) &
     member_seq(p, Pos_Over(fsp1, fsp2))
            => (EXISTS((e | member(e, E)), sigma):
                     subtermOF(t, p) = ext(sigma)(lhs(e)) &
                     subtermOF(t1, p) = ext(sigma)(rhs(e)) &
                     parallel_reduction?(E)(subtermOF(t, p),subtermOF(t2,p)) )

  subterm_joinability: LEMMA
    Orthogonal?(E) &
    SPP?(t)(fsp1) & SPP?(t)(fsp2) &
         parallel_reduction_fix?(E)(t,t1,fsp1) &
         parallel_reduction_fix?(E)(t,t2,fsp2) &
         fsp = Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2)
     IMPLIES FORALL(i:below[fsp`length]): 
         EXISTS s :
       parallel_reduction?(E)(subtermOF(t1,fsp(i)), s) &
       parallel_reduction?(E)(subtermOF(t2,fsp(i)), s)

  subterms_joinability: LEMMA
    Orthogonal?(E) &
    SPP?(t)(fsp1) & SPP?(t)(fsp2) &
         parallel_reduction_fix?(E)(t,t1,fsp1) &
         parallel_reduction_fix?(E)(t,t2,fsp2) &
         fsp = Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2)
     IMPLIES EXISTS fst : fsp`length = fst`length AND
     FORALL(i:below[fsp`length]): 
       parallel_reduction?(E)(subtermOF(t1,fsp(i)), fst(i)) &
       parallel_reduction?(E)(subtermOF(t2,fsp(i)), fst(i))

 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 parallel_reduction_has_DP: LEMMA
  Orthogonal?(E) => diamond_property?(parallel_reduction?(E))

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 Orthogonal_implies_confluent: LEMMA 
  FORALL (E : Orthogonal) :  
    LET RRE = reduction?(E) IN
    confluent?(RRE)

 END orthogonality


[ Dauer der Verarbeitung: 0.36 Sekunden  (vorverarbeitet)  ]