:: Similarity of Formulae :: by Agata Darmochwa{\l} and Andrzej Trybulec :: :: Received November 22, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, TARSKI, XBOOLE_0, SUBSET_1, CQC_LANG, QC_LANG1, ZF_LANG, REALSET1, XXREAL_0, FINSEQ_1, XBOOLEAN, CLASSES2, BVFUNC_2, NAT_1, ARYTM_3, CARD_1, FUNCT_2, MARGREL1, FINSUB_1, ZFMISC_1, FINSET_1, ZF_LANG1, RCOMP_1, PARTFUN1, SETWISEO, SETFAM_1, MEMBER_1, CQC_SIM1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, DOMAIN_1, MCART_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, XCMPLX_0, PARTFUN1, XXREAL_0, FUNCOP_1, FINSEQ_1, FINSET_1, FINSUB_1, NAT_1, SETWISEO, QC_LANG1, QC_LANG2, QC_LANG3, CQC_LANG, FUNCT_4, RECDEF_1, SEQ_4; constructors SETFAM_1, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_4, SETWISEO, XXREAL_0, NAT_1, RECDEF_1, SEQ_4, QC_LANG3, CQC_LANG, XXREAL_2, RELSET_1, XTUPLE_0, XXREAL_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSUB_1, XXREAL_0, FINSEQ_1, QC_LANG1, CQC_LANG, FINSET_1, FUNCOP_1, RELSET_1, RELAT_1; requirements NUMERALS, REAL, BOOLE, SUBSET; begin reserve A for QC-alphabet; definition let A; let b be bound_QC-variable of A; func x. b -> QC-symbol of A means :: CQC_SIM1:def 1 x.it = b; end; theorem :: CQC_SIM1:1 for x,y being set, f being Function holds Im(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 i,j,k,l,m,n for Nat; reserve a,b,e for set; reserve t,u,v,w,z for QC-symbol of A; reserve p,q,r,s for Element of CQC-WFF(A); reserve x for Element of bound_QC-variables(A); reserve ll for CQC-variable_list of k,A; reserve P for QC-pred_symbol of k,A; 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 :: CQC_SIM1:sch 1 QCFuncExN { Al() -> QC-alphabet, D() -> non empty set, V() -> Element of D(), A(object) -> Element of D(), N(object,object) -> Element of D(), C(object,object,object) -> Element of D(), Q(object,object) -> Element of D()}: ex F being Function of QC-WFF(Al()), D() st F.VERUM(Al()) = V() & for p being Element of QC-WFF(Al()) 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 :: CQC_SIM1:sch 2 CQCF2FuncEx { Al() -> QC-alphabet, D, E() -> non empty set, V() -> Element of Funcs(D(),E()), A(object,object,object) -> Element of Funcs(D(),E()), N(object,object) -> Element of Funcs(D(),E()), C(object,object,object,object) -> Element of Funcs(D(),E()), Q(object,object,object) -> Element of Funcs(D(),E()) } : ex F being Function of CQC-WFF(Al()), Funcs(D(),E()) st F.VERUM(Al()) = V() & (for k for l being CQC-variable_list of k,Al() for P being QC-pred_symbol of k,Al() holds F.(P!l) = A(k,P,l)) & for r,s being Element of CQC-WFF(Al()) for x being Element of bound_QC-variables(Al()) 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 :: CQC_SIM1:sch 3 CQCF2FUniq { Al() -> QC-alphabet, D, E() -> non empty set, F1, F2() -> Function of CQC-WFF(Al()),Funcs(D(),E()), V() -> Function of D(),E(), A(object,object,object) -> Function of D(),E(), N(object,object) -> Function of D(),E(), C(object,object,object,object) -> Function of D(),E(), Q(object,object,object) -> Function of D(),E() } : F1() = F2() provided F1().VERUM(Al()) = V() and for k for ll be CQC-variable_list of k,Al() for P be QC-pred_symbol of k,Al() holds F1().(P!ll) = A(k,P,ll) and for r,s be Element of CQC-WFF(Al()) for x be Element of bound_QC-variables(Al()) 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(Al()) = V() and for k for ll be CQC-variable_list of k,Al() for P be QC-pred_symbol of k,Al() holds F2().(P!ll) = A(k,P,ll) and for r,s be Element of CQC-WFF(Al()) for x be Element of bound_QC-variables(Al()) 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,A, i st 1<=i & i<=len l holds l .i in bound_QC-variables(A); definition let A; let D be non empty set, f be Function of D, CQC-WFF(A); func NEGATIVE f -> Element of Funcs(D, CQC-WFF(A)) means :: CQC_SIM1:def 2 for a being Element of D for p being Element of CQC-WFF(A) st p=f.a holds it.a = 'not' p; end; reserve f,h for Element of Funcs(bound_QC-variables(A),bound_QC-variables(A)), K,L for Element of Fin bound_QC-variables(A); definition let A; let f,g be Function of [:QC-symbols(A),Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A), n be Nat; func CON(f,g,n) -> Element of Funcs([:QC-symbols(A), Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A)) means :: CQC_SIM1:def 3 for t,h,p,q st p = f.(t,h) & q = g .(t+n,h) holds it.(t,h) = p '&' q; end; definition let A; let f be Function of [:QC-symbols(A),Funcs(bound_QC-variables(A),bound_QC-variables(A)):], CQC-WFF(A),x be bound_QC-variable of A; func UNIVERSAL(x,f) -> Element of Funcs([:QC-symbols(A), Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A)) means :: CQC_SIM1:def 4 for t,h,p st p = f.(t++,h +* (x .--> x.t)) holds it.(t,h)=All(x.t,p); end; definition let A; let k; let l be CQC-variable_list of k,A; let f be Element of Funcs(bound_QC-variables(A),bound_QC-variables(A)); redefine func f*l -> CQC-variable_list of k,A; end; definition let A; let k; let P be QC-pred_symbol of k,A, l be CQC-variable_list of k,A; func ATOMIC(P,l) -> Element of Funcs([:QC-symbols(A), Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A)) means :: CQC_SIM1:def 5 for t,h holds it.(t,h) = P!(h*l); end; definition let A; let p; func QuantNbr(p) -> Element of NAT means :: CQC_SIM1:def 6 ex F being Function of CQC-WFF(A), NAT st it = F.p & F.VERUM(A) = 0 & for r,s,x,k for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A 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 A; let f be Function of CQC-WFF(A), Funcs([:QC-symbols(A), Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A)), x be Element of CQC-WFF(A); redefine func f.x -> Element of Funcs([:QC-symbols(A), Funcs(bound_QC-variables(A), bound_QC-variables(A)):],CQC-WFF(A)); end; definition let A; func SepFunc(A) -> Function of CQC-WFF(A), Funcs([:QC-symbols(A),Funcs(bound_QC-variables(A), bound_QC-variables(A)):], CQC-WFF(A)) means :: CQC_SIM1:def 7 it.VERUM(A) = [:QC-symbols(A),Funcs( bound_QC-variables(A),bound_QC-variables(A)):] --> VERUM(A) & (for k for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A 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 A; let p,t,f; func SepFunc(p,t,f) -> Element of CQC-WFF(A) equals :: CQC_SIM1:def 8 ((SepFunc(A)).p).[t,f]; end; theorem :: CQC_SIM1:14 QuantNbr(VERUM(A)) = 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; theorem :: CQC_SIM1:19 for p being Element of QC-WFF(A) holds still_not-bound_in p is finite; scheme :: CQC_SIM1:sch 4 MaxFinDomElem {D()->non empty set, X()->set, P[object,object] }: 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 X be set; redefine func id X -> Element of Funcs(X,X); end; definition let A; let p; func NBI p -> Subset of QC-symbols(A) equals :: CQC_SIM1:def 9 {t: for u st t<=u holds not x.u in still_not-bound_in p}; end; registration let A; let p; cluster NBI p -> non empty; end; definition let A; let p; func index p -> QC-symbol of A equals :: CQC_SIM1:def 10 min NBI p; end; theorem :: CQC_SIM1:20 index p = 0(A) iff p is closed; theorem :: CQC_SIM1:21 x.t in still_not-bound_in p implies t < index p; theorem :: CQC_SIM1:22 index VERUM(A) = 0(A); theorem :: CQC_SIM1:23 index ('not' p) = index p; theorem :: CQC_SIM1:24 index p <= index(p '&' q) & index q <= index(p '&' q); definition let A; let p; func SepVar(p) -> Element of CQC-WFF(A) equals :: CQC_SIM1:def 11 SepFunc(p, index p, id(bound_QC-variables(A))); end; theorem :: CQC_SIM1:25 SepVar VERUM(A) = VERUM(A); scheme :: CQC_SIM1:sch 5 CQCInd{ A() -> QC-alphabet, P[object] }: for r being Element of CQC-WFF(A()) holds P[r] provided P[VERUM(A())] and for k for l being CQC-variable_list of k,A() for P being QC-pred_symbol of k,A() holds P[P!l] and for r being Element of CQC-WFF(A()) st P[r] holds P['not' r] and for r,s being Element of CQC-WFF(A()) st P[r] & P[s] holds P[r '&' s] and for r being Element of CQC-WFF(A()), x being bound_QC-variable of A() st P[r] holds P[All(x, r)]; theorem :: CQC_SIM1:26 SepVar(P!ll) = P!ll; theorem :: CQC_SIM1:27 p is atomic implies SepVar p = p; theorem :: CQC_SIM1:28 SepVar 'not' p = 'not' SepVar p; theorem :: CQC_SIM1:29 p is negative & q = the_argument_of p implies SepVar p = 'not' SepVar q; definition let A; let p; let X be Subset of [:CQC-WFF(A),QC-symbols(A),Fin bound_QC-variables(A), Funcs(bound_QC-variables(A),bound_QC-variables(A)):]; pred X is_Sep-closed_on p means :: CQC_SIM1:def 12 [p,index p, {}.bound_QC-variables(A),id (bound_QC-variables(A))] in X & (for q,t,K,f holds ['not' q,t,K,f] in X implies [q,t,K,f] in X) & (for q,r,t,K,f holds [q '&' r,t,K,f] in X implies [q,t,K,f] in X & [r,t+QuantNbr(q),K,f] in X) & for q,x,t,K,f st [All(x,q),t,K,f] in X holds [q,t++,K \/ {x}, f+*(x .--> x.t)] in X; end; definition let A; let p; func SepQuadruples p -> Subset of [:CQC-WFF(A),QC-symbols(A),Fin bound_QC-variables(A), Funcs(bound_QC-variables(A),bound_QC-variables(A)):] means :: CQC_SIM1:def 13 it is_Sep-closed_on p & for D being Subset of [:CQC-WFF(A), QC-symbols(A), Fin bound_QC-variables(A),Funcs(bound_QC-variables(A), bound_QC-variables(A)):] st D is_Sep-closed_on p holds it c= D; end; theorem :: CQC_SIM1:30 [p,index p,{}.bound_QC-variables(A),id(bound_QC-variables(A))] in SepQuadruples(p); theorem :: CQC_SIM1:31 for q,t,K,f st ['not' q,t,K,f] in SepQuadruples p holds [q,t,K,f ] in SepQuadruples p; theorem :: CQC_SIM1:32 for q,r,t,K,f st [q '&' r,t,K,f] in SepQuadruples p holds [q,t,K ,f] in SepQuadruples p & [r,t+QuantNbr(q),K,f] in SepQuadruples p; theorem :: CQC_SIM1:33 for q,x,t,K,f st [All(x,q),t,K,f] in SepQuadruples p holds [q,t++,K \/ {x}, f+*(x .--> x.t)] in SepQuadruples p; theorem :: CQC_SIM1:34 [q,t,K,f] in SepQuadruples p implies [q,t,K,f] = [p,index p,{}. bound_QC-variables(A),id bound_QC-variables(A)] or ['not' q,t,K,f] in SepQuadruples p or (ex r st [q '&' r, t, K,f] in SepQuadruples p) or (ex r,u st t = u+QuantNbr r & [r '&' q,u,K,f] in SepQuadruples p) or ex x,u,h st u++ = t & h +*({x} --> x.u) = f & ([All(x,q),u,K,h] in SepQuadruples p or [All(x,q),u,K\{x},h] in SepQuadruples p); scheme :: CQC_SIM1:sch 6 Sepregression{A() -> QC-alphabet, p()-> Element of CQC-WFF(A()), P[object,object,object,object] }: for q being Element of CQC-WFF(A()), t being QC-symbol of A(), K being Element of Fin bound_QC-variables(A()), f being Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st [q,t,K,f] in SepQuadruples p() holds P[q,t,K,f] provided P[p(),index p(),{}.bound_QC-variables(A()),id bound_QC-variables(A())] and for q being Element of CQC-WFF(A()), t being QC-symbol of A(), K being Element of Fin bound_QC-variables(A()), f being Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st ['not' q,t,K,f] in SepQuadruples p() & P['not' q,t,K, f] holds P[q,t,K,f] and for q,r being Element of CQC-WFF(A()), t being QC-symbol of A(), K being Element of Fin bound_QC-variables(A()), f being Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st [q '&' r, t, K,f] in SepQuadruples p() & P[q '&' r, t, K,f] holds P[q,t,K,f] & P[r,t+QuantNbr(q),K,f] and for q being Element of CQC-WFF(A()), x being bound_QC-variable of A(), t being QC-symbol of A(), K being Element of Fin bound_QC-variables(A()), f being Element of Funcs(bound_QC-variables(A()),bound_QC-variables(A())) st [All(x,q),t,K,f] in SepQuadruples p() & P[All(x,q),t,K,f] holds P[q,t++,K \/ {x},f+*(x .--> x.t)]; theorem :: CQC_SIM1:35 for q,t,K,f holds [q,t,K,f] in SepQuadruples p implies q is_subformula_of p; theorem :: CQC_SIM1:36 SepQuadruples VERUM(A) = { [VERUM(A),0(A),{}.bound_QC-variables(A),id bound_QC-variables(A)] }; theorem :: CQC_SIM1:37 for k for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds SepQuadruples(P!l) = { [P!l,index(P!l),{}.bound_QC-variables(A), id bound_QC-variables(A)] }; theorem :: CQC_SIM1:38 for q,t,K,f st [q,t,K,f] in SepQuadruples p holds still_not-bound_in q c= still_not-bound_in p \/ K; theorem :: CQC_SIM1:39 [q,t,K,f] in SepQuadruples p & x.u in f.:K implies u < t; theorem :: CQC_SIM1:40 [q,t,K,f] in SepQuadruples p implies not x.t in f.:K; theorem :: CQC_SIM1:41 [q,t,K,f] in SepQuadruples p & x.u in f.:still_not-bound_in p implies u