The abstract of the Mizar article:

Reduction Relations

by

Grzegorz Bancerek

Received November 14, 1995

MML identifier: REWRITE1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, BOOLE, RELAT_1, FUNCT_1, FINSEQ_5, ARYTM_1, WELLORD1,
      PBOOLE, RELAT_2, FUNCOP_1, BHSP_3, ISOCAT_1, EQREL_1, REWRITE1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
      FUNCT_1, RELAT_1, RELAT_2, WELLORD1, EQREL_1, FUNCOP_1, FINSEQ_1, PBOOLE,
      FINSEQ_5, LANG1;
 constructors NAT_1, WELLORD1, EQREL_1, FUNCOP_1, PBOOLE, FINSEQ_5, LANG1,
      XREAL_0, MEMBERED, PARTFUN1, TOLER_1, RELAT_1, RELAT_2, RELSET_1;
 clusters SUBSET_1, RELAT_1, FINSEQ_1, XREAL_0, FUNCOP_1, ARYTM_3, MEMBERED,
      NUMBERS, ORDINAL2, EQREL_1, TOLER_1, PARTFUN1, RELSET_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Forgetting concatenation and reduction sequence

definition
 let p,q be FinSequence;
 func p$^q -> FinSequence means
:: REWRITE1:def 1

  it = p^q if p = {} or q = {} otherwise
  ex i being Nat, r being FinSequence st len p = i+1 & r = p|Seg i & it = r^q;
end;

reserve p,q,r for FinSequence, x,y for set;

theorem :: REWRITE1:1
   {}$^p = p & p$^{} = p;

theorem :: REWRITE1:2
 q <> {} implies (p^<*x*>)$^q = p^q;

theorem :: REWRITE1:3
   (p^<*x*>)$^(<*y*>^q) = p^<*y*>^q;

theorem :: REWRITE1:4
   q <> {} implies <*x*>$^q = q;

theorem :: REWRITE1:5
   p <> {} implies ex x,q st p = <*x*>^q & len p = len q+1;

scheme PathCatenation {P[set,set], p,q() -> FinSequence}:
 for i being Nat st i in dom (p()$^q()) & i+1 in dom (p()$^q())
 for x,y being set st x = (p()$^q()).i & y = (p()$^q()).(i+1) holds P[x,y]
  provided
  for i being Nat st i in dom p() & i+1 in dom p() holds P[p().i, p().(i+1)]
  and
  for i being Nat st i in dom q() & i+1 in dom q() holds P[q().i, q().(i+1)]
  and
  len p() > 0 & len q() > 0 & p().len p() = q().1;

definition
 let R be Relation;
 mode RedSequence of R -> FinSequence means
:: REWRITE1:def 2

  len it > 0 &
  for i being Nat st i in dom it & i+1 in dom it holds [it.i, it.(i+1)] in R;
end;

definition
 let R be Relation;
 cluster -> non empty RedSequence of R;
end;

canceled;

theorem :: REWRITE1:7
 for R being Relation, a being set holds <*a*> is RedSequence of R;

theorem :: REWRITE1:8
 for R being Relation, a,b being set st [a,b] in R holds
   <*a,b*> is RedSequence of R;

theorem :: REWRITE1:9
 for R being Relation, p,q being RedSequence of R st p.len p = q.1 holds
   p$^q is RedSequence of R;

theorem :: REWRITE1:10
 for R being Relation, p being RedSequence of R holds
   Rev p is RedSequence of R~;

theorem :: REWRITE1:11
 for R,Q being Relation st R c= Q for p being RedSequence of R
  holds p is RedSequence of Q;

begin :: Reducibility, convertibility, and normal forms

definition
 let R be Relation;
 let a,b be set;
 pred R reduces a,b means
:: REWRITE1:def 3

  ex p being RedSequence of R st p.1 = a & p.len p = b;
end;

definition
 let R be Relation;
 let a,b be set;
 pred a,b are_convertible_wrt R means
:: REWRITE1:def 4

  R \/ R~ reduces a,b;
end;

theorem :: REWRITE1:12
 for R being Relation, a,b being set holds
  R reduces a,b iff
  ex p being FinSequence st len p > 0 & p.1 = a & p.len p = b &
   for i being Nat st i in dom p & i+1 in dom p holds [p.i, p.(i+1)] in R;

theorem :: REWRITE1:13
 for R being Relation, a being set holds R reduces a,a;

theorem :: REWRITE1:14
 for a,b being set st {} reduces a,b holds a = b;

theorem :: REWRITE1:15
 for R being Relation, a,b being set st R reduces a,b & not a in field R
   holds a = b;

theorem :: REWRITE1:16
 for R being Relation, a,b being set st [a,b] in R holds R reduces a,b;

theorem :: REWRITE1:17
 for R being Relation, a,b,c being set st R reduces a,b & R reduces b,c
   holds R reduces a,c;

theorem :: REWRITE1:18
 for R being Relation, p being RedSequence of R, i,j being Nat st
  i in dom p & j in dom p & i <= j holds R reduces p.i,p.j;

theorem :: REWRITE1:19
 for R being Relation, a,b being set st R reduces a,b & a <> b
  holds a in field R & b in field R;

theorem :: REWRITE1:20
 for R being Relation, a,b being set st R reduces a,b holds
   a in field R iff b in field R;

theorem :: REWRITE1:21
 for R being Relation, a,b being set holds
   R reduces a,b iff a = b or [a,b] in R*;

theorem :: REWRITE1:22
 for R being Relation, a,b being set holds
   R reduces a,b iff R* reduces a,b;

theorem :: REWRITE1:23
 for R,Q being Relation st R c= Q for a,b being set st R reduces a,b
  holds Q reduces a,b;

theorem :: REWRITE1:24
   for R being Relation, X being set, a,b being set holds
  R reduces a,b iff R \/ id X reduces a,b;

theorem :: REWRITE1:25
 for R being Relation, a,b being set st R reduces a,b
   holds R~ reduces b,a;

theorem :: REWRITE1:26
 for R being Relation, a,b being set st R reduces a,b
   holds a,b are_convertible_wrt R & b,a are_convertible_wrt R;

theorem :: REWRITE1:27
 for R being Relation, a being set holds a,a are_convertible_wrt R;

theorem :: REWRITE1:28
 for a,b being set st a,b are_convertible_wrt {} holds a = b;

theorem :: REWRITE1:29
   for R being Relation, a,b being set st a,b are_convertible_wrt R &
   not a in field R holds a = b;

theorem :: REWRITE1:30
 for R being Relation, a,b being set st [a,b] in R
   holds a,b are_convertible_wrt R;

theorem :: REWRITE1:31
 for R being Relation, a,b,c being set st
  a,b are_convertible_wrt R & b,c are_convertible_wrt R
   holds a,c are_convertible_wrt R;

theorem :: REWRITE1:32
   for R being Relation, a,b being set st a,b are_convertible_wrt R
  holds b,a are_convertible_wrt R;

theorem :: REWRITE1:33
 for R being Relation, a,b being set st a,b are_convertible_wrt R & a <> b
   holds a in field R & b in field R;

definition
 let R be Relation;
 let a be set;
 pred a is_a_normal_form_wrt R means
:: REWRITE1:def 5
    not ex b being set st [a,b] in R;
end;

theorem :: REWRITE1:34
 for R being Relation, a,b being set st
  a is_a_normal_form_wrt R & R reduces a,b holds a = b;

theorem :: REWRITE1:35
 for R being Relation, a being set st not a in field R
   holds a is_a_normal_form_wrt R;

definition
 let R be Relation;
 let a,b be set;
 pred b is_a_normal_form_of a,R means
:: REWRITE1:def 6

  b is_a_normal_form_wrt R & R reduces a,b;

 pred a,b are_convergent_wrt R means
:: REWRITE1:def 7

  ex c being set st R reduces a,c & R reduces b,c;

 pred a,b are_divergent_wrt R means
:: REWRITE1:def 8

  ex c being set st R reduces c,a & R reduces c,b;

 pred a,b are_convergent<=1_wrt R means
:: REWRITE1:def 9

  ex c being set st ([a,c] in R or a = c) & ([b,c] in R or b = c);

 pred a,b are_divergent<=1_wrt R means
:: REWRITE1:def 10

  ex c being set st ([c,a] in R or a = c) & ([c,b] in R or b = c);
end;

theorem :: REWRITE1:36
 for R being Relation, a being set st not a in field R
   holds a is_a_normal_form_of a,R;

theorem :: REWRITE1:37
 for R being Relation, a,b being set st R reduces a,b
  holds a,b are_convergent_wrt R & a,b are_divergent_wrt R &
        b,a are_convergent_wrt R & b,a are_divergent_wrt R;

theorem :: REWRITE1:38
 for R being Relation, a,b being set st
   a,b are_convergent_wrt R or a,b are_divergent_wrt R
  holds a,b are_convertible_wrt R;

theorem :: REWRITE1:39
 for R being Relation, a being set holds
  a,a are_convergent_wrt R & a,a are_divergent_wrt R;

theorem :: REWRITE1:40
 for a,b being set st a,b are_convergent_wrt {} or a,b are_divergent_wrt {}
   holds a = b;

theorem :: REWRITE1:41
   for R being Relation, a,b being set st a,b are_convergent_wrt R
  holds b,a are_convergent_wrt R;

theorem :: REWRITE1:42
   for R being Relation, a,b being set st a,b are_divergent_wrt R
  holds b,a are_divergent_wrt R;

theorem :: REWRITE1:43
 for R being Relation, a,b,c being set st
  R reduces a,b & b,c are_convergent_wrt R or
  a,b are_convergent_wrt R & R reduces c,b
 holds a,c are_convergent_wrt R;

theorem :: REWRITE1:44
   for R being Relation, a,b,c being set st
  R reduces b,a & b,c are_divergent_wrt R or
  a,b are_divergent_wrt R & R reduces b,c
 holds a,c are_divergent_wrt R;

theorem :: REWRITE1:45
 for R being Relation, a,b being set st a,b are_convergent<=1_wrt R
  holds a,b are_convergent_wrt R;

theorem :: REWRITE1:46
 for R being Relation, a,b being set st a,b are_divergent<=1_wrt R
  holds a,b are_divergent_wrt R;

definition
 let R be Relation;
 let a be set;
 pred a has_a_normal_form_wrt R means
:: REWRITE1:def 11

  ex b being set st b is_a_normal_form_of a,R;
end;

theorem :: REWRITE1:47
 for R being Relation, a being set st not a in field R
   holds a has_a_normal_form_wrt R;

definition
 let R be Relation, a be set;
 assume that
      a has_a_normal_form_wrt R and
      for b,c being set st b is_a_normal_form_of a,R &
     c is_a_normal_form_of a,R holds b = c;
 func nf(a,R) means
:: REWRITE1:def 12

  it is_a_normal_form_of a,R;
end;

begin :: Terminating reductions

definition
 let R be Relation;
 attr R is co-well_founded means
:: REWRITE1:def 13

  R~ is well_founded;

 attr R is weakly-normalizing means
:: REWRITE1:def 14

  for a being set st a in field R holds a has_a_normal_form_wrt R;

 attr R is strongly-normalizing means
:: REWRITE1:def 15 :: terminating, Noetherian
    for f being ManySortedSet of NAT ex i being Nat st not [f.i,f.(i+1)] in R;
end;

definition let R be Relation;
 redefine attr R is co-well_founded means
:: REWRITE1:def 16

  for Y being set st Y c= field R & Y <> {}
   ex a being set st a in Y &
    for b being set st b in Y & a <> b holds not [a,b] in R;
end;

scheme coNoetherianInduction{R() -> Relation, P[set]}:
 for a being set st a in field R() holds P[a]
  provided
   R() is co-well_founded
  and
   for a being set st for b being set st [a,b] in R() & a <> b holds P[b]
      holds P[a];

definition
 cluster strongly-normalizing -> irreflexive co-well_founded Relation;
 cluster co-well_founded irreflexive -> strongly-normalizing Relation;
end;

definition
 cluster empty -> weakly-normalizing strongly-normalizing Relation;
end;

definition
 cluster empty Relation;

end;

theorem :: REWRITE1:48
   for Q being co-well_founded Relation, R being Relation st R c= Q
  holds R is co-well_founded;

definition
 cluster strongly-normalizing -> weakly-normalizing Relation;
end;

begin :: Church-Rosser property

definition
 let R,Q be Relation;
 pred R commutes-weakly_with Q means
:: REWRITE1:def 17
    for a,b,c being set st [a,b] in R & [a,c] in Q
   ex d being set st Q reduces b,d & R reduces c,d;
 symmetry;
 pred R commutes_with Q means
:: REWRITE1:def 18

  for a,b,c being set st R reduces a,b & Q reduces a,c
   ex d being set st Q reduces b,d & R reduces c,d;
 symmetry;
end;

theorem :: REWRITE1:49
   for R,Q being Relation st R commutes_with Q holds R commutes-weakly_with Q;

definition
 let R be Relation;
 attr R is with_UN_property means
:: REWRITE1:def 19

  for a,b being set st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R &
   a,b are_convertible_wrt R holds a = b;

 attr R is with_NF_property means
:: REWRITE1:def 20
    for a,b being set st a is_a_normal_form_wrt R & a,b are_convertible_wrt R
   holds R reduces b,a;

 attr R is subcommutative means
:: REWRITE1:def 21

  for a,b,c being set st [a,b] in R & [a,c] in R
   holds b,c are_convergent<=1_wrt R;
 synonym R has_diamond_property;

 attr R is confluent means
:: REWRITE1:def 22

  for a,b being set st a,b are_divergent_wrt R holds a,b are_convergent_wrt R;

 attr R is with_Church-Rosser_property means
:: REWRITE1:def 23

  for a,b being set st a,b are_convertible_wrt R
   holds a,b are_convergent_wrt R;
 synonym R has_Church-Rosser_property;

 attr R is locally-confluent means
:: REWRITE1:def 24

  for a,b,c being set st [a,b] in R & [a,c] in R
   holds b,c are_convergent_wrt R;
 synonym R has_weak-Church-Rosser_property;
end;

theorem :: REWRITE1:50
 for R being Relation st R is subcommutative for a,b,c being set st
   R reduces a,b & [a,c] in R holds b,c are_convergent_wrt R;

theorem :: REWRITE1:51
   for R being Relation holds
   R is confluent iff R commutes_with R;

theorem :: REWRITE1:52
 for R being Relation holds
  R is confluent iff for a,b,c being set st
   R reduces a,b & [a,c] in R holds b,c are_convergent_wrt R;

theorem :: REWRITE1:53
   for R being Relation holds
   R is locally-confluent iff R commutes-weakly_with R;

definition
 cluster with_Church-Rosser_property -> confluent Relation;
 cluster confluent -> locally-confluent with_Church-Rosser_property Relation;
 cluster subcommutative -> confluent Relation;
 cluster with_Church-Rosser_property -> with_NF_property Relation;
 cluster with_NF_property -> with_UN_property Relation;
 cluster with_UN_property weakly-normalizing -> with_Church-Rosser_property
   Relation;
end;

definition
 cluster empty -> subcommutative Relation;
end;

definition
 cluster empty Relation;

end;


theorem :: REWRITE1:54
 for R being with_UN_property Relation
 for a,b,c being set st b is_a_normal_form_of a,R & c is_a_normal_form_of a,R
  holds b = c;

theorem :: REWRITE1:55
 for R being with_UN_property weakly-normalizing Relation
 for a being set holds nf(a,R) is_a_normal_form_of a,R;

theorem :: REWRITE1:56
 for R being with_UN_property weakly-normalizing Relation
 for a,b being set st a,b are_convertible_wrt R holds nf(a,R) = nf(b,R);

definition
 cluster strongly-normalizing locally-confluent -> confluent Relation;
end;

definition let R be Relation;
 attr R is complete means
:: REWRITE1:def 25
R is confluent strongly-normalizing;
end;

definition
 cluster complete -> confluent strongly-normalizing Relation;
 cluster confluent strongly-normalizing -> complete Relation;
end;

definition
 cluster empty Relation;

end;

definition
 cluster complete (non empty Relation);
end;

theorem :: REWRITE1:57
   for R,Q being with_Church-Rosser_property Relation st
   R commutes_with Q holds R \/ Q has_Church-Rosser_property;

theorem :: REWRITE1:58
   for R being Relation holds
   R is confluent iff R* has_weak-Church-Rosser_property;

theorem :: REWRITE1:59
   for R being Relation holds
   R is confluent iff R* is subcommutative;

begin :: Completion method

definition
 let R,Q be Relation;
 pred R,Q are_equivalent means
:: REWRITE1:def 26
    for a,b being set holds
   a,b are_convertible_wrt R iff a,b are_convertible_wrt Q;
 symmetry;
end;

definition
 let R be Relation;
 let a,b be set;
 pred a,b are_critical_wrt R means
:: REWRITE1:def 27

  a,b are_divergent<=1_wrt R & not a,b are_convergent_wrt R;
end;

theorem :: REWRITE1:60
 for R being Relation, a,b being set st a,b are_critical_wrt R
  holds a,b are_convertible_wrt R;

theorem :: REWRITE1:61
   for R being Relation st not ex a,b being set st a,b are_critical_wrt R
  holds R is locally-confluent;

theorem :: REWRITE1:62
   for R,Q being Relation st
   for a,b being set st [a,b] in Q holds a,b are_critical_wrt R
  holds R, R \/ Q are_equivalent;

theorem :: REWRITE1:63
 for R being Relation ex Q being complete Relation st
  field Q c= field R &
  for a,b being set holds
   a,b are_convertible_wrt R iff a,b are_convergent_wrt Q;

definition
 let R be Relation;
 mode Completion of R -> complete Relation means
:: REWRITE1:def 28

  for a,b being set holds
   a,b are_convertible_wrt R iff a,b are_convergent_wrt it;
end;

theorem :: REWRITE1:64
   for R being Relation, C being Completion of R holds R,C are_equivalent;

theorem :: REWRITE1:65
   for R being Relation, Q being complete Relation st R,Q are_equivalent
   holds Q is Completion of R;

theorem :: REWRITE1:66
   for R being Relation, C being Completion of R, a,b being set holds
   a,b are_convertible_wrt R iff nf(a,C) = nf(b,C);