Quelle 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

quality78%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.