:: Substitution in First-Order Formulas: Elementary Properties :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-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, SUBSET_1, QC_LANG1, CQC_LANG, FINSEQ_1, PARTFUN1, XBOOLE_0, FUNCT_1, RELAT_1, XXREAL_0, NAT_1, TARSKI, FINSET_1, ZFMISC_1, ZF_LANG, CLASSES2, CARD_1, BVFUNC_2, ORDINAL4, REALSET1, XBOOLEAN, MARGREL1, MCART_1, ARYTM_3, SUBSTUT1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, CARD_1, ORDINAL1, NUMBERS, FINSEQ_1, NAT_1, QC_LANG1, QC_LANG3, PARTFUN1, SEQ_4, CQC_LANG, FINSET_1, RELSET_1, FUNCT_2, DOMAIN_1, MCART_1, XXREAL_0, CARD_3; constructors PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, SEQ_4, QC_LANG3, CQC_SIM1, RELSET_1, ORDINAL1, CARD_3, ORDERS_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, FINSEQ_1, QC_LANG1, CQC_LANG, XXREAL_0, XTUPLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE; begin :: Preliminaries reserve A for QC-alphabet; reserve a,b,b1,b2,c,d for object, i,j,k,n for Nat, x,y,x1,x2 for bound_QC-variable of A, P for QC-pred_symbol of k,A, ll for CQC-variable_list of k,A, l1 ,l2 for FinSequence of QC-variables(A), p for QC-formula of A, s,t for QC-symbol of A; definition let A; func vSUB(A) -> set equals :: SUBSTUT1:def 1 PFuncs(bound_QC-variables(A),bound_QC-variables(A)); end; registration let A; cluster vSUB(A) -> non empty; end; definition let A; mode CQC_Substitution of A is Element of vSUB(A); end; registration let A; cluster vSUB(A) -> functional; end; reserve Sub for CQC_Substitution of A; definition let A; let Sub; func @Sub -> PartFunc of bound_QC-variables(A),bound_QC-variables(A) equals :: SUBSTUT1:def 2 Sub; end; theorem :: SUBSTUT1:1 a in dom Sub implies Sub.a in bound_QC-variables(A); definition let A; let l be FinSequence of QC-variables(A); let Sub; func CQC_Subst(l,Sub) -> FinSequence of QC-variables(A) means :: SUBSTUT1:def 3 len it = len l & for k st 1 <= k & k <= len l holds (l.k in dom Sub implies it.k = Sub.( l.k)) & (not l.k in dom Sub implies it.k = l.k); end; definition let A; let l be FinSequence of bound_QC-variables(A); func @l -> FinSequence of QC-variables(A) equals :: SUBSTUT1:def 4 l; end; definition let A; let l be FinSequence of bound_QC-variables(A); let Sub; func CQC_Subst(l,Sub) -> FinSequence of bound_QC-variables(A) equals :: SUBSTUT1:def 5 CQC_Subst( @l,Sub); end; definition let A; let Sub; let X be set; redefine func Sub|X -> CQC_Substitution of A; end; registration let A; cluster finite for CQC_Substitution of A; end; definition let A; let x, p, Sub; func RestrictSub(x,p,Sub) -> finite CQC_Substitution of A equals :: SUBSTUT1:def 6 Sub|{y : y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub.y}; end; definition let A; let l1; func Bound_Vars(l1) -> Subset of bound_QC-variables(A) equals :: SUBSTUT1:def 7 { l1.k : 1 <= k & k <= len l1 & l1.k in bound_QC-variables(A)}; end; definition let A; let p; func Bound_Vars(p) -> Subset of bound_QC-variables(A) means :: SUBSTUT1:def 8 ex F being Function of QC-WFF(A), bool bound_QC-variables(A) st it = F.p & for p being Element of QC-WFF(A) for d1,d2 being Subset of bound_QC-variables(A) holds (p = VERUM(A) implies F.p = {}(bound_QC-variables(A))) & (p is atomic implies F.p = Bound_Vars( the_arguments_of p)) & (p is negative & d1 = F.the_argument_of p implies F.p = d1) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F. the_right_argument_of p implies F.p = d1 \/ d2) & (p is universal & d1 = F. the_scope_of p implies F.p = (d1 \/ {bound_in p})); end; theorem :: SUBSTUT1:2 Bound_Vars(VERUM(A)) = {}; theorem :: SUBSTUT1:3 for p being QC-formula of A st p is atomic holds Bound_Vars(p) = Bound_Vars (the_arguments_of p); theorem :: SUBSTUT1:4 for p being QC-formula of A st p is negative holds Bound_Vars(p) = Bound_Vars(the_argument_of p); theorem :: SUBSTUT1:5 for p being QC-formula of A st p is conjunctive holds Bound_Vars(p) = ( Bound_Vars(the_left_argument_of p)) \/ ( Bound_Vars(the_right_argument_of p)) ; theorem :: SUBSTUT1:6 for p being QC-formula of A st p is universal holds Bound_Vars(p) = Bound_Vars(the_scope_of p) \/ {bound_in p}; registration let A; let p; cluster Bound_Vars(p) -> finite; end; definition let A; let p; func Dom_Bound_Vars(p) -> finite Subset of QC-symbols(A) equals :: SUBSTUT1:def 9 {s : x.s in Bound_Vars p}; end; reserve finSub for finite CQC_Substitution of A; definition let A; let finSub; func Sub_Var(finSub) -> finite Subset of QC-symbols(A) equals :: SUBSTUT1:def 10 {s : x.s in rng finSub}; end; definition let A; let p, finSub; func NSub(p,finSub) -> non empty Subset of QC-symbols(A) equals :: SUBSTUT1:def 11 NAT\(Dom_Bound_Vars(p)\/ Sub_Var(finSub)); end; definition let A; let finSub, p; func upVar(finSub,p) -> QC-symbol of A equals :: SUBSTUT1:def 12 the Element of NSub(p,finSub); end; definition let A; let x, p, finSub; assume ex Sub st finSub = RestrictSub(x,All(x,p),Sub); func ExpandSub(x,p,finSub) -> CQC_Substitution of A equals :: SUBSTUT1:def 13 finSub \/ {[x,x.upVar(finSub,p)]} if x in rng finSub otherwise finSub \/ {[x,x]}; end; definition let A; let p, Sub; let b be object; pred p,Sub PQSub b means :: SUBSTUT1:def 14 (p is universal implies b = ExpandSub( bound_in p,the_scope_of p, RestrictSub(bound_in p,p,Sub))) & (not p is universal implies b = {}); end; definition let A; func QSub(A) -> Function means :: SUBSTUT1:def 15 a in it iff ex p,Sub,b st a = [[p,Sub],b] & p, Sub PQSub b; end; begin :: Definition and Properties of the :: Formula - Substitution - Construction reserve e for Element of vSUB(A); theorem :: SUBSTUT1:7 [:QC-WFF(A),vSUB(A):] is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):] & (for k being Nat, p being (QC-pred_symbol of k,A), ll being QC-variable_list of k,A , e being Element of vSUB(A) holds [<*p*>^ll,e] in [:QC-WFF(A),vSUB(A):]) & (for e being Element of vSUB(A) holds [<*[0, 0]*>,e] in [:QC-WFF(A),vSUB(A):]) & (for p being FinSequence of [:NAT,QC-symbols(A):], e being Element of vSUB(A) st [p,e] in [:QC-WFF(A),vSUB(A):] holds [<*[1, 0]*>^p,e] in [:QC-WFF(A),vSUB(A):]) & (for p, q being FinSequence of [: NAT, QC-symbols(A):], e being Element of vSUB(A) st [p,e] in [:QC-WFF(A),vSUB(A):] & [q,e] in [: QC-WFF(A),vSUB(A):] holds [<*[2, 0]*>^p^q,e] in [:QC-WFF(A),vSUB(A):]) & (for x being bound_QC-variable of A, p being FinSequence of [:NAT, QC-symbols(A):], e being Element of vSUB(A) st [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in [:QC-WFF(A),vSUB(A):] holds [<*[3, 0]*>^<*x*>^p,e] in [:QC-WFF(A),vSUB(A):]); definition let A; let IT be set; attr IT is A-Sub-closed means :: SUBSTUT1:def 16 IT is Subset of [:[:NAT, QC-symbols(A):]*,vSUB(A):] & (for k being Nat, p being (QC-pred_symbol of k,A), ll being QC-variable_list of k,A, e being Element of vSUB(A) holds [<*p*>^ll,e] in IT) & (for e being Element of vSUB(A) holds [<*[0, 0]*>,e] in IT) & (for p being FinSequence of [:NAT,QC-symbols(A):], e being Element of vSUB(A) st [p,e] in IT holds [<*[1, 0]*>^p,e] in IT) & (for p, q being FinSequence of [:NAT, QC-symbols(A):], e being Element of vSUB(A) st [p,e] in IT & [q,e] in IT holds [<*[2, 0]*>^p^q,e] in IT) & (for x being bound_QC-variable of A, p being FinSequence of [:NAT, QC-symbols(A):], e being Element of vSUB(A) st [p,(QSub(A)).[<*[3, 0]*>^<*x*>^p,e]] in IT holds [<*[3, 0]*>^<*x*>^p,e] in IT); end; registration let A; cluster A-Sub-closed non empty for set; end; definition let A; func QC-Sub-WFF(A) -> non empty set means :: SUBSTUT1:def 17 it is A-Sub-closed & for D being non empty set st D is A-Sub-closed holds it c= D; end; reserve S,S9,S1,S2,S19,S29,T1,T2 for Element of QC-Sub-WFF(A); theorem :: SUBSTUT1:8 ex p,e st S = [p,e]; registration let A; cluster QC-Sub-WFF(A) -> A-Sub-closed; end; definition let A; let P be QC-pred_symbol of A; let l be FinSequence of QC-variables(A); let e; assume the_arity_of P = len l; func Sub_P(P,l,e) -> Element of QC-Sub-WFF(A) equals :: SUBSTUT1:def 18 [P!l,e]; end; theorem :: SUBSTUT1:9 for k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A holds Sub_P(P,ll,e) = [P!ll,e]; definition let A; let S; attr S is A-Sub_VERUM means :: SUBSTUT1:def 19 ex e st S = [VERUM(A),e]; end; definition let A; let S; redefine func S`1 -> Element of QC-WFF(A); redefine func S`2 -> Element of vSUB(A); end; theorem :: SUBSTUT1:10 S = [S`1,S`2]; definition let A; let S; func Sub_not S -> Element of QC-Sub-WFF(A) equals :: SUBSTUT1:def 20 ['not' S`1,S`2]; end; definition let A; let S, S9; assume S`2 = (S9)`2; func Sub_&(S,S9) -> Element of QC-Sub-WFF(A) equals :: SUBSTUT1:def 21 [(S`1) '&' ((S9)`1) ,S`2]; end; reserve B for Element of [:QC-Sub-WFF(A),bound_QC-variables(A):]; definition let A; let B; redefine func B`1 -> Element of QC-Sub-WFF(A); redefine func B`2 -> Element of bound_QC-variables(A); end; definition let A; let B; attr B is quantifiable means :: SUBSTUT1:def 22 ex e st (B`1)`2 = (QSub(A)).[All((B)`2,(B`1) `1),e]; end; definition let A; let B; assume B is quantifiable; mode second_Q_comp of B -> Element of vSUB(A) means :: SUBSTUT1:def 23 (B`1)`2 = (QSub(A)).[All (B`2,(B`1)`1),it]; end; reserve SQ for second_Q_comp of B; definition let A; let B, SQ; assume B is quantifiable; func Sub_All(B,SQ) -> Element of QC-Sub-WFF(A) equals :: SUBSTUT1:def 24 [All(B`2,(B`1)`1) ,SQ]; end; definition let A; let S, x; redefine func [S,x] -> Element of [:QC-Sub-WFF(A),bound_QC-variables(A):]; end; scheme :: SUBSTUT1:sch 1 SubQCInd { Al() -> QC-alphabet, Pro[Element of QC-Sub-WFF(Al())]}: for S being Element of QC-Sub-WFF(Al()) holds Pro[S] provided for k being Nat, P being (QC-pred_symbol of k,Al()), ll being QC-variable_list of k,Al(), e being Element of vSUB(Al()) holds Pro[Sub_P(P,ll,e)] and for S being Element of QC-Sub-WFF(Al()) st S is Al()-Sub_VERUM holds Pro[S] and for S being Element of QC-Sub-WFF(Al()) st Pro[S] holds Pro[Sub_not S] and for S,S9 being Element of QC-Sub-WFF(Al()) st S`2 = (S9)`2 & Pro[S] & Pro[S9] holds Pro[Sub_&(S,S9)] and for x being bound_QC-variable of Al(), S being Element of QC-Sub-WFF(Al()), SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & Pro[S] holds Pro[ Sub_All([S,x], SQ)]; definition let A; let S; attr S is Sub_atomic means :: SUBSTUT1:def 25 ex k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB(A) st S = Sub_P(P,ll,e); end; theorem :: SUBSTUT1:11 S is Sub_atomic implies S`1 is atomic; registration let A; let k be Nat; let P be (QC-pred_symbol of k,A), ll be QC-variable_list of k,A; let e be Element of vSUB(A); cluster Sub_P(P,ll,e) -> Sub_atomic; end; definition let A; let S; attr S is Sub_negative means :: SUBSTUT1:def 26 ex S9 st S = Sub_not S9; attr S is Sub_conjunctive means :: SUBSTUT1:def 27 ex S1,S2 st S = Sub_&(S1,S2) & S1`2 = S2`2; end; definition let A; let S; attr S is Sub_universal means :: SUBSTUT1:def 28 ex B,SQ st S = Sub_All(B,SQ) & B is quantifiable; end; theorem :: SUBSTUT1:12 for S holds S is A-Sub_VERUM or S is Sub_atomic or S is Sub_negative or S is Sub_conjunctive or S is Sub_universal; definition let A; let S such that S is Sub_atomic; func Sub_the_arguments_of S -> FinSequence of QC-variables(A) means :: SUBSTUT1:def 29 ex k being Nat, P being (QC-pred_symbol of k,A), ll being QC-variable_list of k,A, e being Element of vSUB(A) st it = ll & S = Sub_P(P,ll,e); end; definition let A; let S such that S is Sub_negative; func Sub_the_argument_of S -> Element of QC-Sub-WFF(A) means :: SUBSTUT1:def 30 S = Sub_not it; end; definition let A; let S such that S is Sub_conjunctive; func Sub_the_left_argument_of S -> Element of QC-Sub-WFF(A) means :: SUBSTUT1:def 31 ex S9 st S = Sub_&(it,S9) & it`2 = (S9)`2; end; definition let A; let S such that S is Sub_conjunctive; func Sub_the_right_argument_of S -> Element of QC-Sub-WFF(A) means :: SUBSTUT1:def 32 ex S9 st S = Sub_&(S9,it) & (S9)`2 = it`2; end; definition let A; let S such that S is Sub_universal; func Sub_the_bound_of S -> bound_QC-variable of A means :: SUBSTUT1:def 33 ex B,SQ st S = Sub_All(B, SQ) & B`2 = it & B is quantifiable; end; definition let A; let A2 be Element of QC-Sub-WFF(A) such that A2 is Sub_universal; func Sub_the_scope_of A2 -> Element of QC-Sub-WFF(A) means :: SUBSTUT1:def 34 ex B,SQ st A2 = Sub_All(B,SQ) & B`1 = it & B is quantifiable; end; registration let A; let S; cluster Sub_not S -> Sub_negative; end; theorem :: SUBSTUT1:13 S1`2 = S2`2 implies Sub_&(S1,S2) is Sub_conjunctive; theorem :: SUBSTUT1:14 B is quantifiable implies Sub_All(B,SQ) is Sub_universal; theorem :: SUBSTUT1:15 Sub_not(S) = Sub_not(S9) implies S = S9; theorem :: SUBSTUT1:16 Sub_the_argument_of(Sub_not(S)) = S; theorem :: SUBSTUT1:17 S1`2 = S2`2 & (S19)`2 = (S29)`2 & Sub_&(S1,S2) = Sub_&(S19,S29) implies S1 = S19 & S2 = S29; theorem :: SUBSTUT1:18 S1`2 = S2`2 implies Sub_the_left_argument_of(Sub_&(S1,S2)) = S1; theorem :: SUBSTUT1:19 S1`2 = S2`2 implies Sub_the_right_argument_of(Sub_&(S1,S2)) = S2; theorem :: SUBSTUT1:20 for B1,B2 being Element of [:QC-Sub-WFF(A),bound_QC-variables(A):], SQ1 being second_Q_comp of B1, SQ2 being second_Q_comp of B2 st B1 is quantifiable & B2 is quantifiable & Sub_All(B1,SQ1) = Sub_All(B2,SQ2) holds B1 = B2; theorem :: SUBSTUT1:21 B is quantifiable implies Sub_the_scope_of(Sub_All(B,SQ)) = B`1; scheme :: SUBSTUT1:sch 2 SubQCInd2 {Al() -> QC-alphabet, Pro[Element of QC-Sub-WFF(Al())]}: for S being Element of QC-Sub-WFF(Al()) holds Pro[S] provided for S being Element of QC-Sub-WFF(Al()) holds (S is Sub_atomic implies Pro [S]) & (S is Al()-Sub_VERUM implies Pro[S]) & (S is Sub_negative & Pro[ Sub_the_argument_of S] implies Pro[S]) & (S is Sub_conjunctive & Pro[ Sub_the_left_argument_of S] & Pro[Sub_the_right_argument_of S] implies Pro[S]) & (S is Sub_universal & Pro[Sub_the_scope_of S] implies Pro[S]); theorem :: SUBSTUT1:22 S is Sub_negative implies len @((Sub_the_argument_of(S))`1) < len @(S`1); theorem :: SUBSTUT1:23 S is Sub_conjunctive implies len @((Sub_the_left_argument_of(S)) `1) < len @(S`1) & len @((Sub_the_right_argument_of(S))`1) < len @(S`1); theorem :: SUBSTUT1:24 S is Sub_universal implies len@((Sub_the_scope_of(S))`1) < len @ (S`1); theorem :: SUBSTUT1:25 (S is A-Sub_VERUM implies ((@S`1).1)`1 = 0) & (S is Sub_atomic implies ex k being Nat st (@S`1).1 is QC-pred_symbol of k,A) & (S is Sub_negative implies ((@S`1).1)`1 = 1) & (S is Sub_conjunctive implies ((@S`1). 1)`1 = 2) & (S is Sub_universal implies ((@S`1).1)`1 = 3); theorem :: SUBSTUT1:26 S is Sub_atomic implies ((@S`1).1)`1 <> 0 & ((@S`1).1)`1 <> 1 & ((@S`1).1)`1 <> 2 & ((@S`1).1)`1 <> 3; theorem :: SUBSTUT1:27 not (ex S st S is Sub_atomic Sub_negative or S is Sub_atomic Sub_conjunctive or S is Sub_atomic Sub_universal or S is Sub_negative Sub_conjunctive or S is Sub_negative Sub_universal or S is Sub_conjunctive Sub_universal or S is A-Sub_VERUM Sub_atomic or S is A-Sub_VERUM Sub_negative or S is A-Sub_VERUM Sub_conjunctive or S is A-Sub_VERUM Sub_universal ); scheme :: SUBSTUT1:sch 3 SubFuncEx { Al() -> QC-alphabet, D()-> non empty set, V() -> (Element of D()), A(Element of QC-Sub-WFF(Al())) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()),(Element of D())) -> (Element of D()), R(set,Element of QC-Sub-WFF(Al()), Element of D()) -> Element of D()} : ex F being Function of QC-Sub-WFF(Al()), D() st for S being Element of QC-Sub-WFF(Al()) for d1,d2 being Element of D() holds (S is Al()-Sub_VERUM implies F.S = V()) & (S is Sub_atomic implies F.S = A(S)) & (S is Sub_negative & d1 = F.Sub_the_argument_of S implies F.S = N(d1)) & (S is Sub_conjunctive & d1 = F.Sub_the_left_argument_of S & d2 = F.Sub_the_right_argument_of S implies F.S = C(d1, d2)) & (S is Sub_universal & d1 = F.Sub_the_scope_of S implies F.S = R(Al(),S,d1)); scheme :: SUBSTUT1:sch 4 SubQCFuncUniq { Al() -> QC-alphabet, D() -> non empty set, F1() -> (Function of QC-Sub-WFF(Al()), D()), F2() -> (Function of QC-Sub-WFF(Al()), D()), V() -> (Element of D()), A(set) -> (Element of D()), N(set) -> (Element of D()), C(set,set) -> (Element of D()), R(set,set,set) -> Element of D()} : F1() = F2() provided for S being Element of QC-Sub-WFF(Al()) for d1,d2 being Element of D() holds (S is Al()-Sub_VERUM implies F1().S = V()) & (S is Sub_atomic implies F1().S = A(S)) & (S is Sub_negative & d1 = F1().Sub_the_argument_of S implies F1().S = N (d1)) & (S is Sub_conjunctive & d1 = F1().Sub_the_left_argument_of S & d2 = F1( ).Sub_the_right_argument_of S implies F1().S = C(d1, d2)) & (S is Sub_universal & d1 = F1().Sub_the_scope_of S implies F1().S = R(Al(),S, d1)) and for S being Element of QC-Sub-WFF(Al()) for d1,d2 being Element of D() holds (S is Al()-Sub_VERUM implies F2().S = V()) & (S is Sub_atomic implies F2().S = A(S)) & (S is Sub_negative & d1 = F2().Sub_the_argument_of S implies F2().S = N (d1)) & (S is Sub_conjunctive & d1 = F2().Sub_the_left_argument_of S & d2 = F2( ).Sub_the_right_argument_of S implies F2().S = C(d1, d2)) & (S is Sub_universal & d1 = F2().Sub_the_scope_of S implies F2().S = R(Al(),S, d1)); definition let A; let S; func @S -> Element of [:QC-WFF(A),vSUB(A):] equals :: SUBSTUT1:def 35 S; end; reserve Z for Element of [:QC-WFF(A),vSUB(A):]; definition let A; let Z; redefine func Z`1 -> Element of QC-WFF(A); redefine func Z`2 -> CQC_Substitution of A; end; definition let A; let Z; func S_Bound(Z) -> bound_QC-variable of A equals :: SUBSTUT1:def 36 x.upVar(RestrictSub(bound_in Z`1 ,Z`1,Z`2),(the_scope_of Z`1)) if bound_in(Z`1) in rng(RestrictSub(bound_in Z`1, Z`1,Z`2)) otherwise bound_in(Z`1); end; definition let A; let S, p; func Quant(S,p) -> Element of QC-WFF(A) equals :: SUBSTUT1:def 37 All(S_Bound(@S),p); end; begin :: Definition and Properties of Substitution :: (Ebb et al, Chapter III, Definition 8.1/8.2) definition let A; let S be Element of QC-Sub-WFF(A); func CQC_Sub(S) -> Element of QC-WFF(A) means :: SUBSTUT1:def 38 ex F being Function of QC-Sub-WFF(A),QC-WFF(A) st it = F.S & for S9 being Element of QC-Sub-WFF(A) holds (S9 is A-Sub_VERUM implies F.S9 = VERUM(A)) & ( S9 is Sub_atomic implies F.S9 = ( the_pred_symbol_of ((S9)`1))! CQC_Subst(Sub_the_arguments_of S9,(S9)`2)) & (S9 is Sub_negative implies F.S9 = 'not' (F.(Sub_the_argument_of S9))) & (S9 is Sub_conjunctive implies F.S9 = (F.Sub_the_left_argument_of S9) '&' (F. Sub_the_right_argument_of S9)) & (S9 is Sub_universal implies F.S9 = Quant(S9,F .Sub_the_scope_of S9)); end; theorem :: SUBSTUT1:28 S is Sub_negative implies CQC_Sub(S) = 'not' CQC_Sub( Sub_the_argument_of S); theorem :: SUBSTUT1:29 CQC_Sub(Sub_not S) = 'not' CQC_Sub(S); theorem :: SUBSTUT1:30 S is Sub_conjunctive implies CQC_Sub(S) = (CQC_Sub( Sub_the_left_argument_of S)) '&' (CQC_Sub(Sub_the_right_argument_of S)); theorem :: SUBSTUT1:31 S1`2 = S2`2 implies CQC_Sub(Sub_&(S1,S2)) = (CQC_Sub(S1)) '&' ( CQC_Sub(S2)); theorem :: SUBSTUT1:32 S is Sub_universal implies CQC_Sub(S) = Quant(S,CQC_Sub( Sub_the_scope_of S)) ; definition let A; func CQC-Sub-WFF(A) -> Subset of QC-Sub-WFF(A) equals :: SUBSTUT1:def 39 {S : S`1 is Element of CQC-WFF(A)}; end; registration let A; cluster CQC-Sub-WFF(A) -> non empty; end; theorem :: SUBSTUT1:33 S is A-Sub_VERUM implies CQC_Sub(S) is Element of CQC-WFF(A); theorem :: SUBSTUT1:34 for h being FinSequence holds h is CQC-variable_list of k,A iff h is FinSequence of bound_QC-variables(A) & len h = k; theorem :: SUBSTUT1:35 CQC_Sub(Sub_P(P,ll,e)) is Element of CQC-WFF(A); theorem :: SUBSTUT1:36 CQC_Sub(S) is Element of CQC-WFF(A) implies CQC_Sub(Sub_not S) is Element of CQC-WFF(A); theorem :: SUBSTUT1:37 S1`2 = S2`2 & CQC_Sub(S1) is Element of CQC-WFF(A) & CQC_Sub(S2) is Element of CQC-WFF(A) implies CQC_Sub(Sub_&(S1,S2)) is Element of CQC-WFF(A); reserve xSQ for second_Q_comp of [S,x]; theorem :: SUBSTUT1:38 CQC_Sub(S) is Element of CQC-WFF(A) & [S,x] is quantifiable implies CQC_Sub(Sub_All([S,x],xSQ)) is Element of CQC-WFF(A); reserve S for Element of CQC-Sub-WFF(A); scheme :: SUBSTUT1:sch 5 SubCQCInd { Al() -> QC-alphabet, Pro[set] } : for S being Element of CQC-Sub-WFF(Al()) holds Pro[S] provided for S,S9 being Element of CQC-Sub-WFF(Al()), x being bound_QC-variable of Al(), SQ being second_Q_comp of [S,x], k being Nat, ll being CQC-variable_list of k,Al(), P being (QC-pred_symbol of k,Al()), e being Element of vSUB(Al()) holds Pro[Sub_P(P,ll,e)] & (S is Al()-Sub_VERUM implies Pro[S]) & (Pro[S] implies Pro[Sub_not S]) & (S`2 = (S9)`2 & Pro[S] & Pro[S9] implies Pro[Sub_&(S,S9)]) & ([S,x] is quantifiable & Pro[S] implies Pro[Sub_All([S,x], SQ)]); definition let A; let S; redefine func CQC_Sub(S) -> Element of CQC-WFF(A); end; theorem :: SUBSTUT1:39 rng @Sub c= bound_QC-variables(A);