The abstract of the Mizar article:

Similarity of Formulae

by

Agata Darmochwal, and

Andrzej Trybulec

Received November 22, 1991

MML identifier: CQC_SIM1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, FUNCT_4, FUNCOP_1, RELAT_1, BOOLE, CQC_LANG, QC_LANG1,
      ZF_LANG, FINSEQ_1, FUNCT_2, FINSUB_1, SQUARE_1, FINSET_1, QC_LANG3,
      GROUP_2, PRE_TOPC, PARTFUN1, SETWISEO, SETFAM_1, SUBSET_1, CQC_SIM1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, DOMAIN_1,
      MCART_1, SETFAM_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, PARTFUN1,
      FUNCOP_1, FINSEQ_1, FINSET_1, FINSUB_1, FRAENKEL, NAT_1, SETWISEO,
      QC_LANG1, QC_LANG2, QC_LANG3, CQC_LANG, FUNCT_4;
 constructors DOMAIN_1, SETFAM_1, FUNCOP_1, FRAENKEL, NAT_1, SETWISEO,
      QC_LANG3, CQC_LANG, FUNCT_4, PARTFUN1, XREAL_0, MEMBERED, RELAT_2,
      XBOOLE_0;
 clusters SUBSET_1, RELSET_1, CQC_LANG, QC_LANG1, FINSUB_1, FUNCOP_1, FINSEQ_1,
      ARYTM_3, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET;


begin

theorem :: CQC_SIM1:1
 for x,y being set, f being Function holds (f+*({x} --> y)).:{x} = {y};

theorem :: CQC_SIM1:2
 for K,L being set
 for x,y being set, f being Function holds (f+*(L --> y)).:K c= f.:K \/ {y};

theorem :: CQC_SIM1:3
  for x,y being set, g being Function, A being set
   holds (g +* ({x} --> y)).:(A \ {x}) = g.:(A \ {x});

theorem :: CQC_SIM1:4
  for x,y being set
  for g being Function
  for A being set st not y in g.:(A \ {x}) holds
    (g +* ({x} --> y)).:(A \ {x}) = (g +* ({x} --> y)).:A \ {y};

reserve p,q,r,s for Element of CQC-WFF,
        x for Element of bound_QC-variables,
        i,j,k,l,m,n for Element of NAT,
        a,b,e for set,
        ll for CQC-variable_list of k,
        P for QC-pred_symbol of k;

theorem :: CQC_SIM1:5
p is atomic implies ex k,P,ll st p = P!ll;


theorem :: CQC_SIM1:6
   p is negative implies ex q st p = 'not' q;

theorem :: CQC_SIM1:7
   p is conjunctive implies ex q,r st p = q '&' r;

theorem :: CQC_SIM1:8
   p is universal implies ex x,q st p = All(x,q);

theorem :: CQC_SIM1:9
for l being FinSequence holds
  rng l = { l.i : 1 <= i & i <= len l };

scheme QC_Func_ExN { D() -> non empty set,
                V() -> Element of D(),
                A(set) -> Element of D(),
                N(set,set) -> Element of D(),
                C(set,set,set) -> Element of D(),
                Q(set,set) -> Element of D()} :
ex F being Function of QC-WFF, D() st
    F.VERUM = V() &
        for p being Element of QC-WFF holds
        (p is atomic implies F.p = A(p)) &
        (p is negative implies F.p = N(F.the_argument_of p,p)) &
        (p is conjunctive implies
          F.p = C(F.the_left_argument_of p, F.the_right_argument_of p, p)) &
        (p is universal implies F.p = Q(F.the_scope_of p, p));

scheme CQCF2_Func_Ex { D, E() -> non empty set,
                V() -> Element of Funcs(D(),E()),
                A(set,set,set) -> Element of Funcs(D(),E()),
                N(set,set) -> Element of Funcs(D(),E()),
                C(set,set,set,set) -> Element of Funcs(D(),E()),
                Q(set,set,set) -> Element of Funcs(D(),E()) }:
  ex F being Function of CQC-WFF, Funcs(D(),E()) st
   F.VERUM = V() &
   (for k for l being CQC-variable_list of k
    for P being QC-pred_symbol of k holds F.(P!l) = A(k,P,l)) &
   for r,s,x holds
      F.('not' r) = N(F.r,r) &
      F.(r '&' s) = C(F.r,F.s,r,s) &
      F.All(x,r) = Q(x,F.r,r);


scheme CQCF2_FUniq { D, E() -> non empty set,
                F1, F2() -> Function of CQC-WFF,Funcs(D(),E()),
                V() -> Function of D(),E(),
                A(set,set,set) -> Function of D(),E(),
                N(set,set) -> Function of D(),E(),
                C(set,set,set,set) -> Function of D(),E(),
                Q(set,set,set) -> Function of D(),E() }:
 F1() = F2() provided
  F1().VERUM = V() and
  for k,ll,P holds F1().(P!ll) = A(k,P,ll) and
  for r,s,x holds F1().('not' r) = N(F1().r,r) &
       F1().(r '&' s) = C(F1().r,F1().s,r,s) &
       F1().All(x,r) = Q(x,F1().r,r) and
  F2().VERUM = V() and
  for k,ll,P holds F2().(P!ll) = A(k,P,ll) and
  for r,s,x holds F2().('not' r) = N(F2().r,r) &
       F2().(r '&' s) = C(F2().r,F2().s,r,s) &
       F2().All(x,r) = Q(x,F2().r,r);

theorem :: CQC_SIM1:10
p is_subformula_of 'not' p;

theorem :: CQC_SIM1:11
p is_subformula_of p '&' q & q is_subformula_of p '&' q;

theorem :: CQC_SIM1:12
p is_subformula_of All(x,p);

theorem :: CQC_SIM1:13
 for l being CQC-variable_list of k, i st 1<=i & i<=len l
  holds l.i in bound_QC-variables;

definition let D be non empty set, f be Function of D, CQC-WFF;
 func NEGATIVE f -> Element of Funcs(D, CQC-WFF) means
:: CQC_SIM1:def 1

   for a being Element of D
    for p being Element of CQC-WFF st p=f.a holds it.a = 'not' p;
end;

reserve f,h for Element of Funcs(bound_QC-variables,bound_QC-variables),
  K,L for Finite_Subset of bound_QC-variables;

definition let f,g be Function of
 [:NAT,Funcs(bound_QC-variables,bound_QC-variables):], CQC-WFF, n be Nat;
func CON(f,g,n) -> Element of
 Funcs([:NAT,Funcs(bound_QC-variables,bound_QC-variables):], CQC-WFF) means
:: CQC_SIM1:def 2
 for k,h,p,q st p = f.[k,h] & q = g.[k+n,h] holds it.[k,h] = p '&' q;
end;

definition let f be Function of
 [:NAT,Funcs(bound_QC-variables,bound_QC-variables):],CQC-WFF,
 x be bound_QC-variable;
func UNIVERSAL(x,f) -> Element of
 Funcs([:NAT,Funcs(bound_QC-variables,bound_QC-variables):],CQC-WFF) means
:: CQC_SIM1:def 3
 for k,h,p st p = f.[k+1,h +* ({x} --> x.k)] holds it.[k,h] = All(x.k,p);
end;

definition let k; let l be CQC-variable_list of k;
 let f be Element of Funcs(bound_QC-variables,bound_QC-variables);
 redefine func f*l -> CQC-variable_list of k;
end;

definition let k; let P be QC-pred_symbol of k, l be CQC-variable_list of k;
 func ATOMIC(P,l) -> Element of
  Funcs([:NAT,Funcs(bound_QC-variables,bound_QC-variables):], CQC-WFF) means
:: CQC_SIM1:def 4

   for n,h holds it.[n,h] = P!(h*l);
end;

definition let p;
func QuantNbr(p) -> Element of NAT means
:: CQC_SIM1:def 5

    ex F being Function of CQC-WFF, NAT st it = F.p &
      F.VERUM = 0 &
      for r,s,x,k for l being CQC-variable_list of k
       for P being QC-pred_symbol of k holds
         F.(P!l) = 0 &
         F.('not' r) = F.r &
         F.(r '&' s) = F.r + F.s &
         F.All(x,r) = F.r + 1;
end;

definition let f be Function of CQC-WFF,
 Funcs([:NAT,Funcs(bound_QC-variables,bound_QC-variables):],CQC-WFF),
 x be Element of CQC-WFF;
 redefine func f.x -> Element of
   Funcs([:NAT,Funcs(bound_QC-variables,bound_QC-variables):],CQC-WFF);
end;

definition
 func SepFunc -> Function of CQC-WFF,
    Funcs([:NAT,Funcs(bound_QC-variables,bound_QC-variables):],CQC-WFF)
 means
:: CQC_SIM1:def 6
  it.VERUM = [:NAT,Funcs(bound_QC-variables,bound_QC-variables):] --> VERUM &
  (for k for l being CQC-variable_list of k
   for P being QC-pred_symbol of k holds it.(P!l) = ATOMIC(P,l)) &
   for r,s,x holds
      it.('not' r) = NEGATIVE(it.r)
   & it.(r '&' s) = CON(it.r,it.s,QuantNbr(r))
   & it.All(x,r) = UNIVERSAL(x,it.r);
end;

definition let p,k,f;
 func SepFunc (p,k,f) -> Element of CQC-WFF equals
:: CQC_SIM1:def 7
   (SepFunc.p).[k,f];
end;

theorem :: CQC_SIM1:14
QuantNbr(VERUM) = 0;

theorem :: CQC_SIM1:15
QuantNbr(P!ll) = 0;

theorem :: CQC_SIM1:16
QuantNbr('not' p) = QuantNbr(p);

theorem :: CQC_SIM1:17
QuantNbr(p '&' q) = QuantNbr(p) + QuantNbr(q);

theorem :: CQC_SIM1:18
QuantNbr(All(x,p)) = QuantNbr(p) + 1;

definition let A be non empty Subset of NAT;
 func min A -> Nat means
:: CQC_SIM1:def 8
   it in A & for k st k in A holds it <= k;
end;

theorem :: CQC_SIM1:19
 for A,B being non empty Subset of NAT st A c= B
   holds min B <= min A;

theorem :: CQC_SIM1:20
  for p being Element of QC-WFF holds still_not-bound_in p is finite;

scheme MaxFinDomElem {D()->non empty set, X()->set, P[set,set] }:
  ex x being Element of D() st x in X() &
   for y being Element of D() st y in X() holds P[x,y]
   provided
   X() is finite & X() <> {} & X() c= D() and
   for x,y being Element of D() holds P[x,y] or P[y,x] and
   for x,y,z being Element of D() st P[x,y] & P[y,z] holds P[x,z];

definition let p;
 func NBI p -> Subset of NAT equals
:: CQC_SIM1:def 9
   {k: for i st k<=i holds not x.i in still_not-bound_in p};
end;

definition let p;
 cluster NBI p -> non empty;
end;

definition let p;
 func index p -> Nat equals
:: CQC_SIM1:def 10
    min (NBI p);
end;

theorem :: CQC_SIM1:21
index p = 0 iff p is closed;

theorem :: CQC_SIM1:22
 x.i in still_not-bound_in p implies i < index p;

theorem :: CQC_SIM1:23
index VERUM = 0;

theorem :: CQC_SIM1:24
index ('not' p) = index p;

theorem :: CQC_SIM1:25
   index p <= index(p '&' q) & index q <= index(p '&' q);

definition let C be non empty set, D be non empty Subset of C;
 redefine func id(D) -> Element of Funcs(D,D);
end;

definition let p;
 func SepVar(p) -> Element of CQC-WFF equals
:: CQC_SIM1:def 11
 SepFunc(p, index p, id(bound_QC-variables));
end;

theorem :: CQC_SIM1:26
SepVar VERUM = VERUM;

scheme CQCInd{ P[set] }:
 for r holds P[r]
provided
 P[VERUM] and
 for k for l being CQC-variable_list of k
     for P being QC-pred_symbol of k holds P[P!l] and
 for r st P[r] holds P['not' r] and
 for r,s st P[r] & P[s] holds P[r '&' s] and
 for r,x st P[r] holds P[All(x, r)];

theorem :: CQC_SIM1:27
SepVar(P!ll) = P!ll;

theorem :: CQC_SIM1:28
p is atomic implies SepVar p = p;

theorem :: CQC_SIM1:29
SepVar 'not' p = 'not' SepVar p;

theorem :: CQC_SIM1:30
   p is negative & q = the_argument_of p implies SepVar p = 'not' SepVar q;

definition let p; let X be Subset of
          [:CQC-WFF,NAT,Fin bound_QC-variables,
            Funcs(bound_QC-variables,bound_QC-variables):];
 pred X is_Sep-closed_on p means
:: CQC_SIM1:def 12

  [p,index p, {}.bound_QC-variables,id(bound_QC-variables)] in X &
  (for q,k,K,f holds ['not' q,k,K,f] in X implies [q,k,K,f] in X) &
  (for q,r,k,K,f holds [q '&' r,k,K,f] in X implies
   [q,k,K,f] in X & [r,k+QuantNbr(q),K,f] in X) &
  for q,x,k,K,f st [All(x,q),k,K,f] in X
   holds [q,k+1,K \/ {x}, f+*({x} --> x.k)] in X;
end;

definition let D be non empty set; let x be Element of D;
 redefine func {x} -> Element of Fin D;
end;

definition let p;
 func SepQuadruples p -> Subset of
       [:CQC-WFF,NAT,Fin bound_QC-variables,
         Funcs(bound_QC-variables,bound_QC-variables):] means
:: CQC_SIM1:def 13
   it is_Sep-closed_on p &
   for D being Subset of
    [:CQC-WFF,NAT,Fin bound_QC-variables,
      Funcs(bound_QC-variables,bound_QC-variables):]
     st D is_Sep-closed_on p holds it c= D;
end;

theorem :: CQC_SIM1:31
 [p,index p,{}.bound_QC-variables,id(bound_QC-variables)] in SepQuadruples(p);

theorem :: CQC_SIM1:32
 for q,k,K,f st ['not' q,k,K,f] in SepQuadruples p
  holds [q,k,K,f] in SepQuadruples p;

theorem :: CQC_SIM1:33
 for q,r,k,K,f st [q '&' r,k,K,f] in SepQuadruples p
  holds [q,k,K,f] in SepQuadruples p & [r,k+QuantNbr(q),K,f] in SepQuadruples p
;

theorem :: CQC_SIM1:34
 for q,x,k,K,f st [All(x,q),k,K,f] in SepQuadruples p
  holds [q,k+1,K \/ {x}, f+*({x} --> x.k)] in SepQuadruples p;

theorem :: CQC_SIM1:35
 [q,k,K,f] in SepQuadruples p implies
    [q,k,K,f] = [p,index p,{}.bound_QC-variables,id bound_QC-variables] or
    ['not' q,k,K,f] in SepQuadruples p or
    (ex r st [q '&' r, k, K,f] in SepQuadruples p) or
    (ex r,l st k = l+QuantNbr r & [r '&' q,l,K,f] in SepQuadruples p) or
    ex x,l,h st l+1 = k & h +*({x} --> x.l) = f &
     ([All(x,q),l,K,h] in SepQuadruples p or
      [All(x,q),l,K\{x},h] in SepQuadruples p);

scheme Sep_regression{p()-> Element of CQC-WFF, P[set,set,set,set] }:
 for q,k,K,f st [q,k,K,f] in SepQuadruples p() holds P[q,k,K,f]
provided
  P[p(),index p(),{}.bound_QC-variables,id bound_QC-variables] and
  for q,k,K,f st ['not' q,k,K,f] in SepQuadruples p() & P['not' q,k,K,f]
       holds P[q,k,K,f] and
  for q,r,k,K,f
       st [q '&' r, k, K,f] in SepQuadruples p() & P[q '&' r, k, K,f]
      holds P[q,k,K,f] & P[r,k+QuantNbr(q),K,f] and
  for q,x,k,K,f st [All(x,q),k,K,f] in SepQuadruples p() & P[All(x,q),k,K,f]
      holds P[q,k+1,K \/ {x},f+*({x} --> x.k)];

theorem :: CQC_SIM1:36
 for q,k,K,f holds [q,k,K,f] in SepQuadruples p implies q is_subformula_of p;

theorem :: CQC_SIM1:37
   SepQuadruples VERUM =
  { [VERUM,0,{}.bound_QC-variables,id bound_QC-variables] };

theorem :: CQC_SIM1:38
   for k for l being CQC-variable_list of k
  for P being QC-pred_symbol of k holds
 SepQuadruples(P!l) =
  { [P!l,index(P!l),{}.bound_QC-variables,id bound_QC-variables] };

theorem :: CQC_SIM1:39
 for q,k,K,f st [q,k,K,f] in SepQuadruples p holds
  still_not-bound_in q c= still_not-bound_in p \/ K;

theorem :: CQC_SIM1:40
 [q,m,K,f] in SepQuadruples p & x.i in f.:K implies i < m;

theorem :: CQC_SIM1:41
   [q,m,K,f] in SepQuadruples p implies not x.m in f.:K;

theorem :: CQC_SIM1:42
 [q,m,K,f] in SepQuadruples p & x.i in f.:still_not-bound_in p implies i < m;

theorem :: CQC_SIM1:43
 [q,m,K,f] in SepQuadruples p & x.i in f.:still_not-bound_in q implies i < m;

theorem :: CQC_SIM1:44
  [q,m,K,f] in SepQuadruples p implies not x.m in f.:(still_not-bound_in q);

theorem :: CQC_SIM1:45
still_not-bound_in p = still_not-bound_in SepVar p;

theorem :: CQC_SIM1:46
index p = index(SepVar p);

definition let p,q;
 pred p,q are_similar means
:: CQC_SIM1:def 14
   SepVar(p) = SepVar(q);
 reflexivity;
 symmetry;
end;

canceled 2;

theorem :: CQC_SIM1:49
p,q are_similar & q,r are_similar implies p,r are_similar;