Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Similarity of Formulae

by
Agata Darmochwal, and
Andrzej Trybulec

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

theorem :: CQC_SIM1:32
for q,k,K,f st ['not' 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
;

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] = [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 &

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
{ [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
{ [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;
```