:: SUBSTUT1 semantic presentation begin definition let A be QC-alphabet ; func vSUB A -> set equals :: SUBSTUT1:def 1 PFuncs ((bound_QC-variables A),(bound_QC-variables A)); coherence PFuncs ((bound_QC-variables A),(bound_QC-variables A)) is set ; end; :: deftheorem defines vSUB SUBSTUT1:def_1_:_ for A being QC-alphabet holds vSUB A = PFuncs ((bound_QC-variables A),(bound_QC-variables A)); registration let A be QC-alphabet ; cluster vSUB A -> non empty ; coherence not vSUB A is empty ; end; definition let A be QC-alphabet ; mode CQC_Substitution of A is Element of vSUB A; end; registration let A be QC-alphabet ; cluster vSUB A -> functional ; coherence vSUB A is functional ; end; definition let A be QC-alphabet ; let Sub be CQC_Substitution of A; func @ Sub -> PartFunc of (bound_QC-variables A),(bound_QC-variables A) equals :: SUBSTUT1:def 2 Sub; coherence Sub is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by PARTFUN1:47; end; :: deftheorem defines @ SUBSTUT1:def_2_:_ for A being QC-alphabet for Sub being CQC_Substitution of A holds @ Sub = Sub; theorem Th1: :: SUBSTUT1:1 for A being QC-alphabet for a being set for Sub being CQC_Substitution of A st a in dom Sub holds Sub . a in bound_QC-variables A proof let A be QC-alphabet ; ::_thesis: for a being set for Sub being CQC_Substitution of A st a in dom Sub holds Sub . a in bound_QC-variables A let a be set ; ::_thesis: for Sub being CQC_Substitution of A st a in dom Sub holds Sub . a in bound_QC-variables A let Sub be CQC_Substitution of A; ::_thesis: ( a in dom Sub implies Sub . a in bound_QC-variables A ) assume a in dom Sub ; ::_thesis: Sub . a in bound_QC-variables A then a in dom (@ Sub) ; hence Sub . a in bound_QC-variables A by PARTFUN1:4; ::_thesis: verum end; definition let A be QC-alphabet ; let l be FinSequence of QC-variables A; let Sub be CQC_Substitution of A; func CQC_Subst (l,Sub) -> FinSequence of QC-variables A means :Def3: :: SUBSTUT1:def 3 ( len it = len l & ( for k being Element of NAT 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 ) ) ) ); existence ex b1 being FinSequence of QC-variables A st ( len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b1 . k = l . k ) ) ) ) proof defpred S1[ set , set ] means ( ( l . \$1 in dom Sub implies \$2 = Sub . (l . \$1) ) & ( not l . \$1 in dom Sub implies \$2 = l . \$1 ) ); A1: for k being Nat st k in Seg (len l) holds ex y being set st S1[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len l) implies ex y being set st S1[k,y] ) assume k in Seg (len l) ; ::_thesis: ex y being set st S1[k,y] ( l . k in dom Sub implies ex y being set st S1[k,y] ) ; hence ex y being set st S1[k,y] ; ::_thesis: verum end; consider s being FinSequence such that A2: dom s = Seg (len l) and A3: for k being Nat st k in Seg (len l) holds S1[k,s . k] from FINSEQ_1:sch_1(A1); rng s c= QC-variables A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s or y in QC-variables A ) assume y in rng s ; ::_thesis: y in QC-variables A then consider x being set such that A4: x in dom s and A5: s . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A4; now__::_thesis:_(_(_l_._x_in_dom_Sub_&_s_._x_in_bound_QC-variables_A_)_or_(_not_l_._x_in_dom_Sub_&_s_._x_in_QC-variables_A_)_) percases ( l . x in dom Sub or not l . x in dom Sub ) ; caseA6: l . x in dom Sub ; ::_thesis: s . x in bound_QC-variables A then s . x = Sub . (l . x) by A2, A3, A4; hence s . x in bound_QC-variables A by A6, Th1; ::_thesis: verum end; caseA7: not l . x in dom Sub ; ::_thesis: s . x in QC-variables A x in dom l by A2, A4, FINSEQ_1:def_3; then A8: l . x in rng l by FUNCT_1:3; s . x = l . x by A2, A3, A4, A7; hence s . x in QC-variables A by A8; ::_thesis: verum end; end; end; hence y in QC-variables A by A5; ::_thesis: verum end; then reconsider s = s as FinSequence of QC-variables A by FINSEQ_1:def_4; take s ; ::_thesis: ( len s = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) ) ) thus len s = len l by A2, FINSEQ_1:def_3; ::_thesis: for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) thus for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) ::_thesis: verum proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len l implies ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) ) assume ( 1 <= k & k <= len l ) ; ::_thesis: ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) then k in dom l by FINSEQ_3:25; then k in Seg (len l) by FINSEQ_1:def_3; hence ( ( l . k in dom Sub implies s . k = Sub . (l . k) ) & ( not l . k in dom Sub implies s . k = l . k ) ) by A3; ::_thesis: verum end; end; uniqueness for b1, b2 being FinSequence of QC-variables A st len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies b1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b1 . k = l . k ) ) ) & len b2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies b2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b2 . k = l . k ) ) ) holds b1 = b2 proof let l1, l2 be FinSequence of QC-variables A; ::_thesis: ( len l1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l1 . k = l . k ) ) ) & len l2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies l2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l2 . k = l . k ) ) ) implies l1 = l2 ) assume that A9: len l1 = len l and A10: for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l1 . k = l . k ) ) and A11: len l2 = len l and A12: for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies l2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l2 . k = l . k ) ) ; ::_thesis: l1 = l2 now__::_thesis:_for_k_being_Nat_st_1_<=_k_&_k_<=_len_l_holds_ l1_._k_=_l2_._k let k be Nat; ::_thesis: ( 1 <= k & k <= len l implies l1 . k = l2 . k ) assume A13: ( 1 <= k & k <= len l ) ; ::_thesis: l1 . k = l2 . k A14: k in NAT by ORDINAL1:def_12; then A15: ( not l . k in dom Sub implies l1 . k = l . k ) by A10, A13; ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) by A10, A14, A13; hence l1 . k = l2 . k by A12, A14, A13, A15; ::_thesis: verum end; hence l1 = l2 by A9, A11, FINSEQ_1:14; ::_thesis: verum end; end; :: deftheorem Def3 defines CQC_Subst SUBSTUT1:def_3_:_ for A being QC-alphabet for l being FinSequence of QC-variables A for Sub being CQC_Substitution of A for b4 being FinSequence of QC-variables A holds ( b4 = CQC_Subst (l,Sub) iff ( len b4 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom Sub implies b4 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies b4 . k = l . k ) ) ) ) ); definition let A be QC-alphabet ; let l be FinSequence of bound_QC-variables A; func @ l -> FinSequence of QC-variables A equals :: SUBSTUT1:def 4 l; coherence l is FinSequence of QC-variables A proof rng l c= QC-variables A by XBOOLE_1:1; hence l is FinSequence of QC-variables A by FINSEQ_1:def_4; ::_thesis: verum end; end; :: deftheorem defines @ SUBSTUT1:def_4_:_ for A being QC-alphabet for l being FinSequence of bound_QC-variables A holds @ l = l; definition let A be QC-alphabet ; let l be FinSequence of bound_QC-variables A; let Sub be CQC_Substitution of A; func CQC_Subst (l,Sub) -> FinSequence of bound_QC-variables A equals :: SUBSTUT1:def 5 CQC_Subst ((@ l),Sub); coherence CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A proof len (CQC_Subst ((@ l),Sub)) = len (@ l) by Def3; then A1: dom (CQC_Subst ((@ l),Sub)) = Seg (len (@ l)) by FINSEQ_1:def_3; A2: for k being Element of NAT st k in Seg (len (@ l)) holds ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) ) proof let k be Element of NAT ; ::_thesis: ( k in Seg (len (@ l)) implies ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) ) ) assume k in Seg (len (@ l)) ; ::_thesis: ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) ) then ( 1 <= k & k <= len (@ l) ) by FINSEQ_1:1; hence ( ( (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst ((@ l),Sub)) . k = (@ l) . k ) ) by Def3; ::_thesis: verum end; rng (CQC_Subst ((@ l),Sub)) c= bound_QC-variables A proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (CQC_Subst ((@ l),Sub)) or y in bound_QC-variables A ) assume y in rng (CQC_Subst ((@ l),Sub)) ; ::_thesis: y in bound_QC-variables A then consider x being set such that A3: x in dom (CQC_Subst ((@ l),Sub)) and A4: (CQC_Subst ((@ l),Sub)) . x = y by FUNCT_1:def_3; reconsider x = x as Element of NAT by A3; now__::_thesis:_(_(_(@_l)_._x_in_dom_Sub_&_(CQC_Subst_((@_l),Sub))_._x_in_bound_QC-variables_A_)_or_(_not_(@_l)_._x_in_dom_Sub_&_(CQC_Subst_((@_l),Sub))_._x_in_bound_QC-variables_A_)_) percases ( (@ l) . x in dom Sub or not (@ l) . x in dom Sub ) ; caseA5: (@ l) . x in dom Sub ; ::_thesis: (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A then (CQC_Subst ((@ l),Sub)) . x = Sub . ((@ l) . x) by A1, A2, A3; hence (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A by A5, Th1; ::_thesis: verum end; caseA6: not (@ l) . x in dom Sub ; ::_thesis: (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A A7: rng l c= bound_QC-variables A ; x in dom (@ l) by A1, A3, FINSEQ_1:def_3; then A8: (@ l) . x in rng (@ l) by FUNCT_1:3; (CQC_Subst ((@ l),Sub)) . x = (@ l) . x by A1, A2, A3, A6; hence (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A by A8, A7; ::_thesis: verum end; end; end; hence y in bound_QC-variables A by A4; ::_thesis: verum end; hence CQC_Subst ((@ l),Sub) is FinSequence of bound_QC-variables A by FINSEQ_1:def_4; ::_thesis: verum end; end; :: deftheorem defines CQC_Subst SUBSTUT1:def_5_:_ for A being QC-alphabet for l being FinSequence of bound_QC-variables A for Sub being CQC_Substitution of A holds CQC_Subst (l,Sub) = CQC_Subst ((@ l),Sub); definition let A be QC-alphabet ; let Sub be CQC_Substitution of A; let X be set ; :: original: | redefine funcSub | X -> CQC_Substitution of A; coherence Sub | X is CQC_Substitution of A proof Sub | X = (@ Sub) | X ; hence Sub | X is CQC_Substitution of A by PARTFUN1:45; ::_thesis: verum end; end; registration let A be QC-alphabet ; cluster Relation-like Function-like finite for Element of vSUB A; existence ex b1 being CQC_Substitution of A st b1 is finite proof take L = {} ; ::_thesis: ( L is CQC_Substitution of A & L is finite ) L is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by RELSET_1:12; hence L is CQC_Substitution of A by PARTFUN1:45; ::_thesis: L is finite thus L is finite ; ::_thesis: verum end; end; definition let A be QC-alphabet ; let x be bound_QC-variable of A; let p be QC-formula of A; let Sub be CQC_Substitution of A; func RestrictSub (x,p,Sub) -> finite CQC_Substitution of A equals :: SUBSTUT1:def 6 Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; coherence Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution of A proof set Y = { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ; set X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; reconsider Z = still_not-bound_in p as finite set by CQC_SIM1:19; for a being set holds ( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } iff a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) proof let a be set ; ::_thesis: ( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } iff a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) thus ( a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ) ::_thesis: ( a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) proof assume a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; ::_thesis: a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } then consider y being bound_QC-variable of A such that A1: ( a = y & y in still_not-bound_in p ) and A2: ( y is Element of dom Sub & y <> x & y <> Sub . y ) ; y in { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by A2; hence a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by A1, XBOOLE_0:def_4; ::_thesis: verum end; thus ( a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } implies a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ) ::_thesis: verum proof assume A3: a in Z /\ { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } ; ::_thesis: a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } then a in { y where y is bound_QC-variable of A : ( y is Element of dom Sub & y <> x & y <> Sub . y ) } by XBOOLE_0:def_4; then A4: ex y being bound_QC-variable of A st ( a = y & y is Element of dom Sub & y <> x & y <> Sub . y ) ; a in Z by A3, XBOOLE_0:def_4; hence a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A4; ::_thesis: verum end; end; then reconsider X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } as finite set by TARSKI:1; Sub | X is finite ; hence Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } is finite CQC_Substitution of A ; ::_thesis: verum end; end; :: deftheorem defines RestrictSub SUBSTUT1:def_6_:_ for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A for Sub being CQC_Substitution of A holds RestrictSub (x,p,Sub) = Sub | { y where y is bound_QC-variable of A : ( y in still_not-bound_in p & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; definition let A be QC-alphabet ; let l1 be FinSequence of QC-variables A; func Bound_Vars l1 -> Subset of (bound_QC-variables A) equals :: SUBSTUT1:def 7 { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ; coherence { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A) proof set A2 = { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ; { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } c= bound_QC-variables A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } or x in bound_QC-variables A ) assume x in { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ; ::_thesis: x in bound_QC-variables A then ex k being Element of NAT st ( l1 . k = x & 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) ; hence x in bound_QC-variables A ; ::_thesis: verum end; hence { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A) ; ::_thesis: verum end; end; :: deftheorem defines Bound_Vars SUBSTUT1:def_7_:_ for A being QC-alphabet for l1 being FinSequence of QC-variables A holds Bound_Vars l1 = { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables A ) } ; definition let A be QC-alphabet ; let p be QC-formula of A; func Bound_Vars p -> Subset of (bound_QC-variables A) means :Def8: :: 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)} ) ) ) ); correctness existence ex b1 being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( b1 = 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)} ) ) ) ); uniqueness for b1, b2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( b1 = 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)} ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( b2 = 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)} ) ) ) ) holds b1 = b2; proof deffunc H1( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = Bound_Vars (the_arguments_of \$1); set V = bound_QC-variables A; deffunc H2( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = \$1; deffunc H3( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = \$1 \/ \$2; deffunc H4( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = \$2 \/ {(bound_in \$1)}; thus ( ex d being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H2(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H3(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H4(p,d1) ) ) ) ) & ( for x1, x2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( x1 = 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 = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H2(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H3(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H4(p,d1) ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( x2 = 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 = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H2(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H3(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H4(p,d1) ) ) ) ) holds x1 = x2 ) ) from QC_LANG3:sch_2(); ::_thesis: verum end; end; :: deftheorem Def8 defines Bound_Vars SUBSTUT1:def_8_:_ for A being QC-alphabet for p being QC-formula of A for b3 being Subset of (bound_QC-variables A) holds ( b3 = Bound_Vars p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( b3 = 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)} ) ) ) ) ); Lm1: for A being QC-alphabet for p being QC-formula of A holds ( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ) proof let A be QC-alphabet ; ::_thesis: for p being QC-formula of A holds ( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ) let p be QC-formula of A; ::_thesis: ( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ) deffunc H1( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = Bound_Vars (the_arguments_of \$1); deffunc H2( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = Bound_Vars \$1; set V = bound_QC-variables A; deffunc H3( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = \$1; deffunc H4( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = \$1 \/ \$2; deffunc H5( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = \$2 \/ {(bound_in \$1)}; A1: for p being QC-formula of A for X being Subset of (bound_QC-variables A) holds ( X = H2(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( X = 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 = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H4(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H5(p,d1) ) ) ) ) ) by Def8; H2( VERUM A) = {} (bound_QC-variables A) from QC_LANG3:sch_3(A1) .= {} ; hence Bound_Vars (VERUM A) = {} (bound_QC-variables A) ; ::_thesis: ( ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ) thus ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) ::_thesis: ( ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ) proof assume A2: p is atomic ; ::_thesis: Bound_Vars p = Bound_Vars (the_arguments_of p) thus H2(p) = H1(p) from QC_LANG3:sch_4(A1, A2); ::_thesis: verum end; thus ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) ::_thesis: ( ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ) proof assume A3: p is negative ; ::_thesis: Bound_Vars p = Bound_Vars (the_argument_of p) thus H2(p) = H3(H2( the_argument_of p)) from QC_LANG3:sch_5(A1, A3); ::_thesis: verum end; thus ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) ::_thesis: ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) proof assume A4: p is conjunctive ; ::_thesis: Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) for d1, d2 being Subset of (bound_QC-variables A) st d1 = H2( the_left_argument_of p) & d2 = H2( the_right_argument_of p) holds H2(p) = H4(d1,d2) from QC_LANG3:sch_6(A1, A4); hence Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ; ::_thesis: verum end; thus ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) ::_thesis: verum proof assume A5: p is universal ; ::_thesis: Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} thus H2(p) = H5(p,H2( the_scope_of p)) from QC_LANG3:sch_7(A1, A5); ::_thesis: verum end; end; theorem Th2: :: SUBSTUT1:2 for A being QC-alphabet holds Bound_Vars (VERUM A) = {} proof let A be QC-alphabet ; ::_thesis: Bound_Vars (VERUM A) = {} Bound_Vars (VERUM A) = {} (bound_QC-variables A) by Lm1; hence Bound_Vars (VERUM A) = {} ; ::_thesis: verum end; theorem :: SUBSTUT1:3 for A being QC-alphabet for p being QC-formula of A st p is atomic holds Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1; theorem :: SUBSTUT1:4 for A being QC-alphabet for p being QC-formula of A st p is negative holds Bound_Vars p = Bound_Vars (the_argument_of p) by Lm1; theorem :: SUBSTUT1:5 for A being QC-alphabet 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)) by Lm1; theorem :: SUBSTUT1:6 for A being QC-alphabet for p being QC-formula of A st p is universal holds Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by Lm1; registration let A be QC-alphabet ; let p be QC-formula of A; cluster Bound_Vars p -> finite ; coherence Bound_Vars p is finite proof defpred S1[ Element of QC-WFF A] means Bound_Vars A is finite ; A1: for p being Element of QC-WFF A holds ( ( p is atomic implies S1[p] ) & S1[ VERUM A] & ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) ) proof let p be Element of QC-WFF A; ::_thesis: ( ( p is atomic implies S1[p] ) & S1[ VERUM A] & ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) ) thus ( p is atomic implies Bound_Vars p is finite ) ::_thesis: ( S1[ VERUM A] & ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) ) proof deffunc H1( set ) -> set = (the_arguments_of p) . A; defpred S2[ Element of NAT ] means ( 1 <= A & A <= len (the_arguments_of p) ); defpred S3[ Element of NAT ] means ( 1 <= A & A <= len (the_arguments_of p) & (the_arguments_of p) . A in bound_QC-variables A ); A2: for k being Element of NAT st S3[k] holds S2[k] ; A3: { H1(k) where k is Element of NAT : S3[k] } c= { H1(n) where n is Element of NAT : S2[n] } from FRAENKEL:sch_1(A2); assume p is atomic ; ::_thesis: Bound_Vars p is finite then Bound_Vars p = Bound_Vars (the_arguments_of p) by Lm1 .= { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ; then Bound_Vars p c= rng (the_arguments_of p) by A3, CQC_SIM1:9; hence Bound_Vars p is finite ; ::_thesis: verum end; thus Bound_Vars (VERUM A) is finite by Th2; ::_thesis: ( ( p is negative & S1[ the_argument_of p] implies S1[p] ) & ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) ) thus ( p is negative & Bound_Vars (the_argument_of p) is finite implies Bound_Vars p is finite ) by Lm1; ::_thesis: ( ( p is conjunctive & S1[ the_left_argument_of p] & S1[ the_right_argument_of p] implies S1[p] ) & ( p is universal & S1[ the_scope_of p] implies S1[p] ) ) thus ( p is conjunctive & Bound_Vars (the_left_argument_of p) is finite & Bound_Vars (the_right_argument_of p) is finite implies Bound_Vars p is finite ) ::_thesis: ( p is universal & S1[ the_scope_of p] implies S1[p] ) proof assume that A4: p is conjunctive and A5: ( Bound_Vars (the_left_argument_of p) is finite & Bound_Vars (the_right_argument_of p) is finite ) ; ::_thesis: Bound_Vars p is finite Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) by A4, Lm1; hence Bound_Vars p is finite by A5; ::_thesis: verum end; assume that A6: p is universal and A7: Bound_Vars (the_scope_of p) is finite ; ::_thesis: S1[p] Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} by A6, Lm1; hence S1[p] by A7; ::_thesis: verum end; for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch_2(A1); hence Bound_Vars p is finite ; ::_thesis: verum end; end; definition let A be QC-alphabet ; let p be QC-formula of A; func Dom_Bound_Vars p -> finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 9 { s where s is QC-symbol of A : x. s in Bound_Vars p } ; coherence { s where s is QC-symbol of A : x. s in Bound_Vars p } is finite Subset of (QC-symbols A) proof defpred S1[ set , set ] means ex s being QC-symbol of A st ( s = \$1 & \$2 = x. s ); set X = { s where s is QC-symbol of A : x. s in Bound_Vars p } ; A1: { s where s is QC-symbol of A : x. s in Bound_Vars p } c= QC-symbols A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { s where s is QC-symbol of A : x. s in Bound_Vars p } or a in QC-symbols A ) assume a in { s where s is QC-symbol of A : x. s in Bound_Vars p } ; ::_thesis: a in QC-symbols A then ex s being QC-symbol of A st ( a = s & x. s in Bound_Vars p ) ; hence a in QC-symbols A ; ::_thesis: verum end; A2: for a being set st a in QC-symbols A holds ex b being set st S1[a,b] proof let a be set ; ::_thesis: ( a in QC-symbols A implies ex b being set st S1[a,b] ) assume a in QC-symbols A ; ::_thesis: ex b being set st S1[a,b] then reconsider s = a as QC-symbol of A ; take x. s ; ::_thesis: S1[a, x. s] take s ; ::_thesis: ( s = a & x. s = x. s ) thus ( s = a & x. s = x. s ) ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = QC-symbols A & ( for a being set st a in QC-symbols A holds S1[a,f . a] ) ) from CLASSES1:sch_1(A2); A4: rng (f | { s where s is QC-symbol of A : x. s in Bound_Vars p } ) c= Bound_Vars p proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (f | { s where s is QC-symbol of A : x. s in Bound_Vars p } ) or b in Bound_Vars p ) assume b in rng (f | { s where s is QC-symbol of A : x. s in Bound_Vars p } ) ; ::_thesis: b in Bound_Vars p then consider a being set such that A5: a in dom (f | { s where s is QC-symbol of A : x. s in Bound_Vars p } ) and A6: b = (f | { s where s is QC-symbol of A : x. s in Bound_Vars p } ) . a by FUNCT_1:def_3; a in { s where s is QC-symbol of A : x. s in Bound_Vars p } by A5, RELAT_1:57; then A7: ex s being QC-symbol of A st ( a = s & x. s in Bound_Vars p ) ; ( b = f . a & a in dom f ) by A5, A6, FUNCT_1:47, RELAT_1:57; then ex s being QC-symbol of A st ( s = a & b = x. s ) by A3; hence b in Bound_Vars p by A7; ::_thesis: verum end; f is one-to-one proof let a1, a2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a1 in proj1 f or not a2 in proj1 f or not f . a1 = f . a2 or a1 = a2 ) assume that A8: ( a1 in dom f & a2 in dom f ) and A9: f . a1 = f . a2 ; ::_thesis: a1 = a2 ( ex s being QC-symbol of A st ( s = a1 & f . a1 = x. s ) & ex t being QC-symbol of A st ( t = a2 & f . a2 = x. t ) ) by A3, A8; hence a1 = a2 by A9, XTUPLE_0:1; ::_thesis: verum end; then f | { s where s is QC-symbol of A : x. s in Bound_Vars p } is one-to-one by FUNCT_1:52; then A10: dom (f | { s where s is QC-symbol of A : x. s in Bound_Vars p } ) is finite by A4, CARD_1:59; reconsider X = { s where s is QC-symbol of A : x. s in Bound_Vars p } as Subset of (QC-symbols A) by A1; for a being set holds ( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:57; then dom (f | X) = X /\ (QC-symbols A) by A3, XBOOLE_0:def_4; hence { s where s is QC-symbol of A : x. s in Bound_Vars p } is finite Subset of (QC-symbols A) by A10, XBOOLE_1:28; ::_thesis: verum end; end; :: deftheorem defines Dom_Bound_Vars SUBSTUT1:def_9_:_ for A being QC-alphabet for p being QC-formula of A holds Dom_Bound_Vars p = { s where s is QC-symbol of A : x. s in Bound_Vars p } ; definition let A be QC-alphabet ; let finSub be finite CQC_Substitution of A; func Sub_Var finSub -> finite Subset of (QC-symbols A) equals :: SUBSTUT1:def 10 { s where s is QC-symbol of A : x. s in rng finSub } ; coherence { s where s is QC-symbol of A : x. s in rng finSub } is finite Subset of (QC-symbols A) proof defpred S1[ set , set ] means ex s being QC-symbol of A st ( s = \$1 & \$2 = x. s ); set X = { s where s is QC-symbol of A : x. s in rng finSub } ; A1: { s where s is QC-symbol of A : x. s in rng finSub } c= QC-symbols A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { s where s is QC-symbol of A : x. s in rng finSub } or a in QC-symbols A ) assume a in { s where s is QC-symbol of A : x. s in rng finSub } ; ::_thesis: a in QC-symbols A then ex s being QC-symbol of A st ( a = s & x. s in rng finSub ) ; hence a in QC-symbols A ; ::_thesis: verum end; A2: for a being set st a in QC-symbols A holds ex b being set st S1[a,b] proof let a be set ; ::_thesis: ( a in QC-symbols A implies ex b being set st S1[a,b] ) assume a in QC-symbols A ; ::_thesis: ex b being set st S1[a,b] then reconsider s = a as QC-symbol of A ; take x. s ; ::_thesis: S1[a, x. s] take s ; ::_thesis: ( s = a & x. s = x. s ) thus ( s = a & x. s = x. s ) ; ::_thesis: verum end; consider f being Function such that A3: ( dom f = QC-symbols A & ( for a being set st a in QC-symbols A holds S1[a,f . a] ) ) from CLASSES1:sch_1(A2); A4: rng (f | { s where s is QC-symbol of A : x. s in rng finSub } ) c= rng finSub proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng (f | { s where s is QC-symbol of A : x. s in rng finSub } ) or b in rng finSub ) assume b in rng (f | { s where s is QC-symbol of A : x. s in rng finSub } ) ; ::_thesis: b in rng finSub then consider a being set such that A5: a in dom (f | { s where s is QC-symbol of A : x. s in rng finSub } ) and A6: b = (f | { s where s is QC-symbol of A : x. s in rng finSub } ) . a by FUNCT_1:def_3; a in { s where s is QC-symbol of A : x. s in rng finSub } by A5, RELAT_1:57; then A7: ex s being QC-symbol of A st ( a = s & x. s in rng finSub ) ; ( b = f . a & a in dom f ) by A5, A6, FUNCT_1:47, RELAT_1:57; then ex s being QC-symbol of A st ( s = a & b = x. s ) by A3; hence b in rng finSub by A7; ::_thesis: verum end; f is one-to-one proof let a1, a2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a1 in proj1 f or not a2 in proj1 f or not f . a1 = f . a2 or a1 = a2 ) assume that A8: ( a1 in dom f & a2 in dom f ) and A9: f . a1 = f . a2 ; ::_thesis: a1 = a2 ( ex s being QC-symbol of A st ( s = a1 & f . a1 = x. s ) & ex t being QC-symbol of A st ( t = a2 & f . a2 = x. t ) ) by A3, A8; hence a1 = a2 by A9, XTUPLE_0:1; ::_thesis: verum end; then f | { s where s is QC-symbol of A : x. s in rng finSub } is one-to-one by FUNCT_1:52; then A10: dom (f | { s where s is QC-symbol of A : x. s in rng finSub } ) is finite by A4, CARD_1:59; reconsider X = { s where s is QC-symbol of A : x. s in rng finSub } as Subset of (QC-symbols A) by A1; for a being set holds ( a in dom (f | X) iff ( a in X & a in dom f ) ) by RELAT_1:57; then dom (f | X) = X /\ (QC-symbols A) by A3, XBOOLE_0:def_4; hence { s where s is QC-symbol of A : x. s in rng finSub } is finite Subset of (QC-symbols A) by A10, XBOOLE_1:28; ::_thesis: verum end; end; :: deftheorem defines Sub_Var SUBSTUT1:def_10_:_ for A being QC-alphabet for finSub being finite CQC_Substitution of A holds Sub_Var finSub = { s where s is QC-symbol of A : x. s in rng finSub } ; Lm2: for X, Y being set st card X in card Y holds Y \ X <> {} proof let X, Y be set ; ::_thesis: ( card X in card Y implies Y \ X <> {} ) assume that A1: card X in card Y and A2: Y \ X = {} ; ::_thesis: contradiction Y c= X by A2, XBOOLE_1:37; then card Y c= card X by CARD_1:11; hence contradiction by A1, CARD_1:4; ::_thesis: verum end; definition let A be QC-alphabet ; let p be QC-formula of A; let finSub be finite CQC_Substitution of A; func NSub (p,finSub) -> non empty Subset of (QC-symbols A) equals :: SUBSTUT1:def 11 NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)); coherence NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A) proof set X = (Dom_Bound_Vars p) \/ (Sub_Var finSub); card ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) in card NAT by CARD_3:42; hence NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)) is non empty Subset of (QC-symbols A) by Lm2, QC_LANG1:3, XBOOLE_1:109; ::_thesis: verum end; end; :: deftheorem defines NSub SUBSTUT1:def_11_:_ for A being QC-alphabet for p being QC-formula of A for finSub being finite CQC_Substitution of A holds NSub (p,finSub) = NAT \ ((Dom_Bound_Vars p) \/ (Sub_Var finSub)); definition let A be QC-alphabet ; let finSub be finite CQC_Substitution of A; let p be QC-formula of A; func upVar (finSub,p) -> QC-symbol of A equals :: SUBSTUT1:def 12 the Element of NSub (p,finSub); coherence the Element of NSub (p,finSub) is QC-symbol of A ; end; :: deftheorem defines upVar SUBSTUT1:def_12_:_ for A being QC-alphabet for finSub being finite CQC_Substitution of A for p being QC-formula of A holds upVar (finSub,p) = the Element of NSub (p,finSub); definition let A be QC-alphabet ; let x be bound_QC-variable of A; let p be QC-formula of A; let finSub be finite CQC_Substitution of A; assume A1: ex Sub being CQC_Substitution of A 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]}; coherence ( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) ) proof A2: now__::_thesis:_(_not_x_in_rng_finSub_implies_finSub_\/_{[x,x]}_is_CQC_Substitution_of_A_) reconsider Z = {[x,x]} as Relation-like set ; assume not x in rng finSub ; ::_thesis: finSub \/ {[x,x]} is CQC_Substitution of A A3: now__::_thesis:_for_a_being_set_holds_not_a_in_(dom_finSub)_/\_(dom_Z) consider Sub being CQC_Substitution of A such that A4: finSub = RestrictSub (x,(All (x,p)),Sub) by A1; set X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; A5: dom finSub c= { y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A4, RELAT_1:58; given a being set such that A6: a in (dom finSub) /\ (dom Z) ; ::_thesis: contradiction a in dom finSub by A6, XBOOLE_0:def_4; then a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A5; then A7: ( dom Z = {x} & ex y being bound_QC-variable of A st ( a = y & y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) ) by RELAT_1:9; a in dom Z by A6, XBOOLE_0:def_4; hence contradiction by A7, TARSKI:def_1; ::_thesis: verum end; reconsider Z = Z as Function ; for a being set st a in (dom (@ finSub)) /\ (dom Z) holds (@ finSub) . a = Z . a by A3; then consider h being Function such that A8: (@ finSub) \/ Z = h by PARTFUN1:1; reconsider Z = Z as Relation of (bound_QC-variables A),(bound_QC-variables A) ; (@ finSub) \/ Z = h by A8; hence finSub \/ {[x,x]} is CQC_Substitution of A by PARTFUN1:45; ::_thesis: verum end; now__::_thesis:_(_x_in_rng_finSub_implies_finSub_\/_{[x,(x._(upVar_(finSub,p)))]}_is_CQC_Substitution_of_A_) reconsider Z = {[x,(x. (upVar (finSub,p)))]} as Relation-like set ; assume x in rng finSub ; ::_thesis: finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A A9: now__::_thesis:_for_a_being_set_holds_not_a_in_(dom_finSub)_/\_(dom_Z) consider Sub being CQC_Substitution of A such that A10: finSub = RestrictSub (x,(All (x,p)),Sub) by A1; set X = { y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } ; A11: dom finSub c= { y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A10, RELAT_1:58; given a being set such that A12: a in (dom finSub) /\ (dom Z) ; ::_thesis: contradiction a in dom finSub by A12, XBOOLE_0:def_4; then a in { y where y is bound_QC-variable of A : ( y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) } by A11; then A13: ( dom Z = {x} & ex y being bound_QC-variable of A st ( a = y & y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) ) by RELAT_1:9; a in dom Z by A12, XBOOLE_0:def_4; hence contradiction by A13, TARSKI:def_1; ::_thesis: verum end; reconsider Z = Z as Function ; for a being set st a in (dom (@ finSub)) /\ (dom Z) holds (@ finSub) . a = Z . a by A9; then consider h being Function such that A14: (@ finSub) \/ Z = h by PARTFUN1:1; reconsider Z = Z as Relation of (bound_QC-variables A),(bound_QC-variables A) ; (@ finSub) \/ Z = h by A14; hence finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A by PARTFUN1:45; ::_thesis: verum end; hence ( ( x in rng finSub implies finSub \/ {[x,(x. (upVar (finSub,p)))]} is CQC_Substitution of A ) & ( not x in rng finSub implies finSub \/ {[x,x]} is CQC_Substitution of A ) ) by A2; ::_thesis: verum end; consistency for b1 being CQC_Substitution of A holds verum ; end; :: deftheorem defines ExpandSub SUBSTUT1:def_13_:_ for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A for finSub being finite CQC_Substitution of A st ex Sub being CQC_Substitution of A st finSub = RestrictSub (x,(All (x,p)),Sub) holds ( ( x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,(x. (upVar (finSub,p)))]} ) & ( not x in rng finSub implies ExpandSub (x,p,finSub) = finSub \/ {[x,x]} ) ); definition let A be QC-alphabet ; let p be QC-formula of A; let Sub be CQC_Substitution of A; let b be set ; predp,Sub PQSub b means :Def14: :: 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; :: deftheorem Def14 defines PQSub SUBSTUT1:def_14_:_ for A being QC-alphabet for p being QC-formula of A for Sub being CQC_Substitution of A for b being set holds ( p,Sub PQSub b iff ( ( 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 = {} ) ) ); definition let A be QC-alphabet ; func QSub A -> Function means :: SUBSTUT1:def 15 for a being set holds ( a in it iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ); existence ex b1 being Function st for a being set holds ( a in b1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) proof defpred S1[ set , set ] means ex p being QC-formula of A ex Sub being CQC_Substitution of A st ( \$1 = [p,Sub] & p,Sub PQSub \$2 ); A1: for a, b1, b2 being set st S1[a,b1] & S1[a,b2] holds b1 = b2 proof let a, b1, b2 be set ; ::_thesis: ( S1[a,b1] & S1[a,b2] implies b1 = b2 ) assume that A2: ex p being QC-formula of A ex Sub being CQC_Substitution of A st ( a = [p,Sub] & p,Sub PQSub b1 ) and A3: ex p being QC-formula of A ex Sub being CQC_Substitution of A st ( a = [p,Sub] & p,Sub PQSub b2 ) ; ::_thesis: b1 = b2 consider p1 being QC-formula of A, Sub1 being CQC_Substitution of A such that A4: a = [p1,Sub1] and A5: p1,Sub1 PQSub b1 by A2; consider p2 being QC-formula of A, Sub2 being CQC_Substitution of A such that A6: a = [p2,Sub2] and A7: p2,Sub2 PQSub b2 by A3; A8: p1 = p2 by A4, A6, XTUPLE_0:1; A9: Sub1 = Sub2 by A4, A6, XTUPLE_0:1; percases ( p1 is universal or not p1 is universal ) ; supposeA10: p1 is universal ; ::_thesis: b1 = b2 then b1 = ExpandSub ((bound_in p1),(the_scope_of p1),(RestrictSub ((bound_in p1),p1,Sub1))) by A5, Def14; hence b1 = b2 by A7, A8, A9, A10, Def14; ::_thesis: verum end; supposeA11: not p1 is universal ; ::_thesis: b1 = b2 then b1 = {} by A5, Def14; hence b1 = b2 by A7, A8, A11, Def14; ::_thesis: verum end; end; end; consider f being Function such that A12: for a, b being set holds ( [a,b] in f iff ( a in [:(QC-WFF A),(vSUB A):] & S1[a,b] ) ) from FUNCT_1:sch_1(A1); take f ; ::_thesis: for a being set holds ( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) for c being set holds ( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) ) proof let c be set ; ::_thesis: ( c in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) ) thus ( c in f implies ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) ) ::_thesis: ( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f ) proof assume A13: c in f ; ::_thesis: ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) then consider a, b being set such that A14: c = [a,b] by RELAT_1:def_1; ex p being QC-formula of A ex Sub being CQC_Substitution of A st ( a = [p,Sub] & p,Sub PQSub b ) by A12, A13, A14; hence ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) by A14; ::_thesis: verum end; thus ( ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( c = [[p,Sub],b] & p,Sub PQSub b ) implies c in f ) by A12; ::_thesis: verum end; hence for a being set holds ( a in f iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st ( for a being set holds ( a in b1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds ( a in b2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) holds b1 = b2 proof let F1, F2 be Function; ::_thesis: ( ( for a being set holds ( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) & ( for a being set holds ( a in F2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ) implies F1 = F2 ) assume that A15: for a being set holds ( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) and A16: for a being set holds ( a in F2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ; ::_thesis: F1 = F2 now__::_thesis:_for_a_being_set_holds_ (_a_in_F1_iff_a_in_F2_) let a be set ; ::_thesis: ( a in F1 iff a in F2 ) ( a in F1 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) by A15; hence ( a in F1 iff a in F2 ) by A16; ::_thesis: verum end; hence F1 = F2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines QSub SUBSTUT1:def_15_:_ for A being QC-alphabet for b2 being Function holds ( b2 = QSub A iff for a being set holds ( a in b2 iff ex p being QC-formula of A ex Sub being CQC_Substitution of A ex b being set st ( a = [[p,Sub],b] & p,Sub PQSub b ) ) ); begin theorem Th7: :: SUBSTUT1:7 for A being QC-alphabet holds ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) proof let A be QC-alphabet ; ::_thesis: ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) QC-WFF A is A -closed by QC_LANG1:7; then QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *) by QC_LANG1:def_10; hence [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:95; ::_thesis: ( ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) thus for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] ::_thesis: ( ( 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) proof let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] let ll be QC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] let e be Element of vSUB A; ::_thesis: [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] p ! ll = <*p*> ^ ll by QC_LANG1:8; hence [(<*p*> ^ ll),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum end; VERUM A in QC-WFF A ; hence for e being Element of vSUB A holds [<*[0,0]*>,e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) thus for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ::_thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) proof let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for 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):] let e be Element of vSUB A; ::_thesis: ( [p,e] in [:(QC-WFF A),(vSUB A):] implies [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] ) assume [p,e] in [:(QC-WFF A),(vSUB A):] ; ::_thesis: [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] then ex a, b being set st ( a in QC-WFF A & b in vSUB A & [p,e] = [a,b] ) by ZFMISC_1:def_2; then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1; 'not' p9 = <*[1,0]*> ^ (@ p9) ; hence [(<*[1,0]*> ^ p),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum end; thus for p, q being FinSequence of [:NAT,(QC-symbols A):] for 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):] ::_thesis: for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] proof let p, q be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for 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):] let e be Element of vSUB A; ::_thesis: ( [p,e] in [:(QC-WFF A),(vSUB A):] & [q,e] in [:(QC-WFF A),(vSUB A):] implies [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ) assume that A1: [p,e] in [:(QC-WFF A),(vSUB A):] and A2: [q,e] in [:(QC-WFF A),(vSUB A):] ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] ex c, d being set st ( c in QC-WFF A & d in vSUB A & [q,e] = [c,d] ) by A2, ZFMISC_1:def_2; then reconsider q9 = q as Element of QC-WFF A by XTUPLE_0:1; ex a, b being set st ( a in QC-WFF A & b in vSUB A & [p,e] = [a,b] ) by A1, ZFMISC_1:def_2; then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1; p9 '&' q9 = (<*[2,0]*> ^ (@ p9)) ^ (@ q9) ; hence [((<*[2,0]*> ^ p) ^ q),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum end; thus for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ::_thesis: verum proof let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for 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):] let e be Element of vSUB A; ::_thesis: ( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] ) assume [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in [:(QC-WFF A),(vSUB A):] ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] then ex a, b being set st ( a in QC-WFF A & b in vSUB A & [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] = [a,b] ) by ZFMISC_1:def_2; then reconsider p9 = p as Element of QC-WFF A by XTUPLE_0:1; All (x,p9) = (<*[3,0]*> ^ <*x*>) ^ (@ p9) ; hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:(QC-WFF A),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum end; end; definition let A be QC-alphabet ; let IT be set ; attrIT is A -Sub-closed means :Def16: :: SUBSTUT1:def 16 ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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; :: deftheorem Def16 defines -Sub-closed SUBSTUT1:def_16_:_ for A being QC-alphabet for IT being set holds ( IT is A -Sub-closed iff ( IT is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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 ) ) ); registration let A be QC-alphabet ; cluster non empty A -Sub-closed for set ; existence ex b1 being set st ( b1 is A -Sub-closed & not b1 is empty ) proof take [:(QC-WFF A),(vSUB A):] ; ::_thesis: ( [:(QC-WFF A),(vSUB A):] is A -Sub-closed & not [:(QC-WFF A),(vSUB A):] is empty ) ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) by Th7; hence ( [:(QC-WFF A),(vSUB A):] is A -Sub-closed & not [:(QC-WFF A),(vSUB A):] is empty ) by Def16; ::_thesis: verum end; end; Lm3: for A being QC-alphabet for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] proof let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] 0 in QC-symbols A by QC_LANG1:3; then [3,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87; then ( rng <*[3,0]*> = {[3,0]} & {[3,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31; then reconsider y = <*[3,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):] holds (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] QC-variables A c= [:NAT,(QC-symbols A):] by QC_LANG1:4; then bound_QC-variables A c= [:NAT,(QC-symbols A):] by XBOOLE_1:1; then rng <*x*> c= [:NAT,(QC-symbols A):] by XBOOLE_1:1; then reconsider z = <*x*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; (y ^ z) ^ p is FinSequence of [:NAT,(QC-symbols A):] ; hence (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] ; ::_thesis: verum end; Lm4: for A being QC-alphabet for k being Element of NAT for l being QC-symbol of A for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] proof let A be QC-alphabet ; ::_thesis: for k being Element of NAT for l being QC-symbol of A for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] let k be Element of NAT ; ::_thesis: for l being QC-symbol of A for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] let l be QC-symbol of A; ::_thesis: for e being Element of vSUB A holds [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] let e be Element of vSUB A; ::_thesis: [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] <*[k,l]*> in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11; hence [<*[k,l]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum end; Lm5: for A being QC-alphabet for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] proof let A be QC-alphabet ; ::_thesis: for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] let ll be QC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] QC-pred_symbols A c= [:NAT,(QC-symbols A):] by QC_LANG1:6; then k -ary_QC-pred_symbols A c= [:NAT,(QC-symbols A):] by XBOOLE_1:1; then A1: rng <*p*> c= [:NAT,(QC-symbols A):] by XBOOLE_1:1; QC-variables A c= [:NAT,(QC-symbols A):] by QC_LANG1:4; then rng ll c= [:NAT,(QC-symbols A):] by XBOOLE_1:1; then (rng <*p*>) \/ (rng ll) c= [:NAT,(QC-symbols A):] by A1, XBOOLE_1:8; then rng (<*p*> ^ ll) c= [:NAT,(QC-symbols A):] by FINSEQ_1:31; then <*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; then <*p*> ^ ll in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11; hence for e being Element of vSUB A holds [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; ::_thesis: verum end; definition let A be QC-alphabet ; func QC-Sub-WFF A -> non empty set means :Def17: :: SUBSTUT1:def 17 ( it is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds it c= D ) ); existence ex b1 being non empty set st ( b1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds b1 c= D ) ) proof set e = the Element of vSUB A; defpred S1[ set ] means for D being non empty set st D is A -Sub-closed holds \$1 in D; consider D0 being set such that A1: for x being set holds ( x in D0 iff ( x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & S1[x] ) ) from XBOOLE_0:sch_1(); 0 in QC-symbols A by QC_LANG1:3; then ( [<*[0,0]*>, the Element of vSUB A] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds [<*[0,0]*>, the Element of vSUB A] in D ) ) by Def16, Lm4; then reconsider D0 = D0 as non empty set by A1; take D0 ; ::_thesis: ( D0 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds D0 c= D ) ) D0 c= [:([:NAT,(QC-symbols A):] *),(vSUB A):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] ) thus ( not x in D0 or x in [:([:NAT,(QC-symbols A):] *),(vSUB A):] ) by A1; ::_thesis: verum end; hence D0 is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] ; :: according to SUBSTUT1:def_16 ::_thesis: ( ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 ) & ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 holds [(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds [((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds D0 c= D ) ) thus for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 ::_thesis: ( ( for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ) & ( for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 holds [(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds [((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds D0 c= D ) ) proof let k be Element of NAT ; ::_thesis: for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 let p be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 let ll be QC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds [(<*p*> ^ ll),e] in D0 let e be Element of vSUB A; ::_thesis: [(<*p*> ^ ll),e] in D0 ( [(<*p*> ^ ll),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds [(<*p*> ^ ll),e] in D ) ) by Def16, Lm5; hence [(<*p*> ^ ll),e] in D0 by A1; ::_thesis: verum end; thus for e being Element of vSUB A holds [<*[0,0]*>,e] in D0 ::_thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 holds [(<*[1,0]*> ^ p),e] in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds [((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds D0 c= D ) ) proof let e be Element of vSUB A; ::_thesis: [<*[0,0]*>,e] in D0 0 in QC-symbols A by QC_LANG1:3; then ( [<*[0,0]*>,e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for D being non empty set st D is A -Sub-closed holds [<*[0,0]*>,e] in D ) ) by Def16, Lm4; hence [<*[0,0]*>,e] in D0 by A1; ::_thesis: verum end; thus for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 holds [(<*[1,0]*> ^ p),e] in D0 ::_thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds [((<*[2,0]*> ^ p) ^ q),e] in D0 ) & ( for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds D0 c= D ) ) proof let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,e] in D0 holds [(<*[1,0]*> ^ p),e] in D0 let e be Element of vSUB A; ::_thesis: ( [p,e] in D0 implies [(<*[1,0]*> ^ p),e] in D0 ) assume A2: [p,e] in D0 ; ::_thesis: [(<*[1,0]*> ^ p),e] in D0 A3: for D being non empty set st D is A -Sub-closed holds [(<*[1,0]*> ^ p),e] in D proof let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies [(<*[1,0]*> ^ p),e] in D ) assume A4: D is A -Sub-closed ; ::_thesis: [(<*[1,0]*> ^ p),e] in D then [p,e] in D by A1, A2; hence [(<*[1,0]*> ^ p),e] in D by A4, Def16; ::_thesis: verum end; 0 in QC-symbols A by QC_LANG1:3; then [1,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87; then ( rng <*[1,0]*> = {[1,0]} & {[1,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31; then reconsider y = <*[1,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; y ^ p is FinSequence of [:NAT,(QC-symbols A):] ; then <*[1,0]*> ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11; then [(<*[1,0]*> ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; hence [(<*[1,0]*> ^ p),e] in D0 by A1, A3; ::_thesis: verum end; thus for p, q being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds [((<*[2,0]*> ^ p) ^ q),e] in D0 ::_thesis: ( ( for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) & ( for D being non empty set st D is A -Sub-closed holds D0 c= D ) ) proof let p, q be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,e] in D0 & [q,e] in D0 holds [((<*[2,0]*> ^ p) ^ q),e] in D0 let e be Element of vSUB A; ::_thesis: ( [p,e] in D0 & [q,e] in D0 implies [((<*[2,0]*> ^ p) ^ q),e] in D0 ) assume A5: ( [p,e] in D0 & [q,e] in D0 ) ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in D0 A6: for D being non empty set st D is A -Sub-closed holds [((<*[2,0]*> ^ p) ^ q),e] in D proof let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies [((<*[2,0]*> ^ p) ^ q),e] in D ) assume A7: D is A -Sub-closed ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in D then ( [p,e] in D & [q,e] in D ) by A1, A5; hence [((<*[2,0]*> ^ p) ^ q),e] in D by A7, Def16; ::_thesis: verum end; 0 in QC-symbols A by QC_LANG1:3; then [2,0] in [:NAT,(QC-symbols A):] by ZFMISC_1:87; then ( rng <*[2,0]*> = {[2,0]} & {[2,0]} c= [:NAT,(QC-symbols A):] ) by FINSEQ_1:39, ZFMISC_1:31; then reconsider y = <*[2,0]*> as FinSequence of [:NAT,(QC-symbols A):] by FINSEQ_1:def_4; (y ^ p) ^ q is FinSequence of [:NAT,(QC-symbols A):] ; then (<*[2,0]*> ^ p) ^ q in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11; then [((<*[2,0]*> ^ p) ^ q),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; hence [((<*[2,0]*> ^ p) ^ q),e] in D0 by A1, A6; ::_thesis: verum end; thus for x being bound_QC-variable of A for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ::_thesis: for D being non empty set st D is A -Sub-closed holds D0 c= D proof let x be bound_QC-variable of A; ::_thesis: for p being FinSequence of [:NAT,(QC-symbols A):] for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 let p be FinSequence of [:NAT,(QC-symbols A):]; ::_thesis: for e being Element of vSUB A st [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 let e be Element of vSUB A; ::_thesis: ( [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 ) assume A8: [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D0 ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 A9: for D being non empty set st D is A -Sub-closed holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in D proof let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in D ) assume A10: D is A -Sub-closed ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in D then [p,((QSub A) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in D by A1, A8; hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in D by A10, Def16; ::_thesis: verum end; (<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] by Lm3; then (<*[3,0]*> ^ <*x*>) ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def_11; then [((<*[3,0]*> ^ <*x*>) ^ p),e] in [:([:NAT,(QC-symbols A):] *),(vSUB A):] by ZFMISC_1:def_2; hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in D0 by A1, A9; ::_thesis: verum end; let D be non empty set ; ::_thesis: ( D is A -Sub-closed implies D0 c= D ) assume A11: D is A -Sub-closed ; ::_thesis: D0 c= D let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D ) assume x in D0 ; ::_thesis: x in D hence x in D by A1, A11; ::_thesis: verum end; uniqueness for b1, b2 being non empty set st b1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds b1 c= D ) & b2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds b2 c= D ) holds b1 = b2 proof let D1, D2 be non empty set ; ::_thesis: ( D1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds D1 c= D ) & D2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds D2 c= D ) implies D1 = D2 ) assume ( D1 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds D1 c= D ) & D2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds D2 c= D ) ) ; ::_thesis: D1 = D2 then ( D1 c= D2 & D2 c= D1 ) ; hence D1 = D2 by XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def_17_:_ for A being QC-alphabet for b2 being non empty set holds ( b2 = QC-Sub-WFF A iff ( b2 is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds b2 c= D ) ) ); theorem Th8: :: SUBSTUT1:8 for A being QC-alphabet for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] let S be Element of QC-Sub-WFF A; ::_thesis: ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] ( [:(QC-WFF A),(vSUB A):] is Subset of [:([:NAT,(QC-symbols A):] *),(vSUB A):] & ( for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for 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):] for 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):] for 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 for p being FinSequence of [:NAT,(QC-symbols A):] for 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):] ) ) by Th7; then [:(QC-WFF A),(vSUB A):] is A -Sub-closed by Def16; then QC-Sub-WFF A c= [:(QC-WFF A),(vSUB A):] by Def17; then S in [:(QC-WFF A),(vSUB A):] by TARSKI:def_3; then consider a, b being set such that A1: a in QC-WFF A and A2: b in vSUB A and A3: S = [a,b] by ZFMISC_1:def_2; reconsider e = b as Element of vSUB A by A2; reconsider p = a as Element of QC-WFF A by A1; take p ; ::_thesis: ex e being Element of vSUB A st S = [p,e] take e ; ::_thesis: S = [p,e] thus S = [p,e] by A3; ::_thesis: verum end; registration let A be QC-alphabet ; cluster QC-Sub-WFF A -> non empty A -Sub-closed ; coherence QC-Sub-WFF A is A -Sub-closed by Def17; end; definition let A be QC-alphabet ; let P be QC-pred_symbol of A; let l be FinSequence of QC-variables A; let e be Element of vSUB A; assume A1: the_arity_of P = len l ; func Sub_P (P,l,e) -> Element of QC-Sub-WFF A equals :Def18: :: SUBSTUT1:def 18 [(P ! l),e]; coherence [(P ! l),e] is Element of QC-Sub-WFF A proof set k = len l; set QCP = { QP where QP is QC-pred_symbol of A : the_arity_of QP = len l } ; P in { QP where QP is QC-pred_symbol of A : the_arity_of QP = len l } by A1; then reconsider P = P as QC-pred_symbol of (len l),A ; reconsider l = l as QC-variable_list of len l,A by CARD_1:def_7; P ! l = <*P*> ^ l by QC_LANG1:8; hence [(P ! l),e] is Element of QC-Sub-WFF A by Def16; ::_thesis: verum end; end; :: deftheorem Def18 defines Sub_P SUBSTUT1:def_18_:_ for A being QC-alphabet for P being QC-pred_symbol of A for l being FinSequence of QC-variables A for e being Element of vSUB A st the_arity_of P = len l holds Sub_P (P,l,e) = [(P ! l),e]; theorem Th9: :: SUBSTUT1:9 for A being QC-alphabet for e being Element of vSUB A for k being Element of NAT for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e] proof let A be QC-alphabet ; ::_thesis: for e being Element of vSUB A for k being Element of NAT for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e] let e be Element of vSUB A; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e] let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e] let P be QC-pred_symbol of k,A; ::_thesis: for ll being QC-variable_list of k,A holds Sub_P (P,ll,e) = [(P ! ll),e] let ll be QC-variable_list of k,A; ::_thesis: Sub_P (P,ll,e) = [(P ! ll),e] set QCP = { QP where QP is QC-pred_symbol of A : the_arity_of QP = k } ; P in { QP where QP is QC-pred_symbol of A : the_arity_of QP = k } ; then A1: ex Q being QC-pred_symbol of A st ( P = Q & the_arity_of Q = k ) ; len ll = k by CARD_1:def_7; hence Sub_P (P,ll,e) = [(P ! ll),e] by A1, Def18; ::_thesis: verum end; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; attrS is A -Sub_VERUM means :Def19: :: SUBSTUT1:def 19 ex e being Element of vSUB A st S = [(VERUM A),e]; end; :: deftheorem Def19 defines -Sub_VERUM SUBSTUT1:def_19_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( S is A -Sub_VERUM iff ex e being Element of vSUB A st S = [(VERUM A),e] ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; :: original: `1 redefine funcS `1 -> Element of QC-WFF A; coherence S `1 is Element of QC-WFF A proof ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8; hence S `1 is Element of QC-WFF A by MCART_1:7; ::_thesis: verum end; :: original: `2 redefine funcS `2 -> Element of vSUB A; coherence S `2 is Element of vSUB A proof ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8; hence S `2 is Element of vSUB A by MCART_1:7; ::_thesis: verum end; end; theorem Th10: :: SUBSTUT1:10 for A being QC-alphabet for S being Element of QC-Sub-WFF A holds S = [(S `1),(S `2)] proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds S = [(S `1),(S `2)] let S be Element of QC-Sub-WFF A; ::_thesis: S = [(S `1),(S `2)] ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8; hence S = [(S `1),(S `2)] by MCART_1:8; ::_thesis: verum end; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; func Sub_not S -> Element of QC-Sub-WFF A equals :: SUBSTUT1:def 20 [('not' (S `1)),(S `2)]; coherence [('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A proof [(S `1),(S `2)] is Element of QC-Sub-WFF A by Th10; hence [('not' (S `1)),(S `2)] is Element of QC-Sub-WFF A by Def16; ::_thesis: verum end; end; :: deftheorem defines Sub_not SUBSTUT1:def_20_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds Sub_not S = [('not' (S `1)),(S `2)]; definition let A be QC-alphabet ; let S, S9 be Element of QC-Sub-WFF A; assume A1: S `2 = S9 `2 ; func Sub_& (S,S9) -> Element of QC-Sub-WFF A equals :Def21: :: SUBSTUT1:def 21 [((S `1) '&' (S9 `1)),(S `2)]; coherence [((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A proof ( [(S `1),(S `2)] is Element of QC-Sub-WFF A & [(S9 `1),(S9 `2)] is Element of QC-Sub-WFF A ) by Th10; hence [((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF A by A1, Def16; ::_thesis: verum end; end; :: deftheorem Def21 defines Sub_& SUBSTUT1:def_21_:_ for A being QC-alphabet for S, S9 being Element of QC-Sub-WFF A st S `2 = S9 `2 holds Sub_& (S,S9) = [((S `1) '&' (S9 `1)),(S `2)]; definition let A be QC-alphabet ; let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; :: original: `1 redefine funcB `1 -> Element of QC-Sub-WFF A; coherence B `1 is Element of QC-Sub-WFF A by MCART_1:10; :: original: `2 redefine funcB `2 -> Element of bound_QC-variables A; coherence B `2 is Element of bound_QC-variables A by MCART_1:10; end; definition let A be QC-alphabet ; let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; attrB is quantifiable means :Def22: :: SUBSTUT1:def 22 ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e]; end; :: deftheorem Def22 defines quantifiable SUBSTUT1:def_22_:_ for A being QC-alphabet for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] holds ( B is quantifiable iff ex e being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),e] ); definition let A be QC-alphabet ; let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; assume A1: B is quantifiable ; mode second_Q_comp of B -> Element of vSUB A means :Def23: :: SUBSTUT1:def 23 (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),it]; existence ex b1 being Element of vSUB A st (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b1] by A1, Def22; end; :: deftheorem Def23 defines second_Q_comp SUBSTUT1:def_23_:_ for A being QC-alphabet for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] st B is quantifiable holds for b3 being Element of vSUB A holds ( b3 is second_Q_comp of B iff (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),b3] ); definition let A be QC-alphabet ; let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; let SQ be second_Q_comp of B; assume A1: B is quantifiable ; func Sub_All (B,SQ) -> Element of QC-Sub-WFF A equals :Def24: :: SUBSTUT1:def 24 [(All ((B `2),((B `1) `1))),SQ]; coherence [(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A proof (B `1) `2 = (QSub A) . [(All ((B `2),((B `1) `1))),SQ] by A1, Def23; then B `1 = [((B `1) `1),((QSub A) . [(All ((B `2),((B `1) `1))),SQ])] by Th10; hence [(All ((B `2),((B `1) `1))),SQ] is Element of QC-Sub-WFF A by Def16; ::_thesis: verum end; end; :: deftheorem Def24 defines Sub_All SUBSTUT1:def_24_:_ for A being QC-alphabet for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ being second_Q_comp of B st B is quantifiable holds Sub_All (B,SQ) = [(All ((B `2),((B `1) `1))),SQ]; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; let x be bound_QC-variable of A; :: original: [ redefine func[S,x] -> Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; coherence [S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] proof [S,x] in [:(QC-Sub-WFF A),(bound_QC-variables A):] ; hence [S,x] is Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ; ::_thesis: verum end; end; scheme :: SUBSTUT1:sch 1 SubQCInd{ F1() -> QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } : for S being Element of QC-Sub-WFF F1() holds P1[S] provided A1: for k being Element of NAT for P being QC-pred_symbol of k,F1() for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds P1[ Sub_P (P,ll,e)] and A2: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds P1[S] and A3: for S being Element of QC-Sub-WFF F1() st P1[S] holds P1[ Sub_not S] and A4: for S, S9 being Element of QC-Sub-WFF F1() st S `2 = S9 `2 & P1[S] & P1[S9] holds P1[ Sub_& (S,S9)] and A5: for x being bound_QC-variable of F1() for S being Element of QC-Sub-WFF F1() for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds P1[ Sub_All ([S,x],SQ)] proof set X = { S where S is Element of QC-Sub-WFF F1() : P1[S] } ; not { S where S is Element of QC-Sub-WFF F1() : P1[S] } is empty proof set e = the Element of vSUB F1(); reconsider V = [(VERUM F1()), the Element of vSUB F1()] as Element of QC-Sub-WFF F1() by Def16; V is F1() -Sub_VERUM by Def19; then P1[V] by A2; then V in { S where S is Element of QC-Sub-WFF F1() : P1[S] } ; hence not { S where S is Element of QC-Sub-WFF F1() : P1[S] } is empty ; ::_thesis: verum end; then reconsider X = { S where S is Element of QC-Sub-WFF F1() : P1[S] } as non empty set ; for e being Element of vSUB F1() holds [(VERUM F1()),e] in X proof let e be Element of vSUB F1(); ::_thesis: [(VERUM F1()),e] in X reconsider V = [(VERUM F1()),e] as Element of QC-Sub-WFF F1() by Def16; V is F1() -Sub_VERUM by Def19; then P1[V] by A2; hence [(VERUM F1()),e] in X ; ::_thesis: verum end; then A6: for e being Element of vSUB F1() holds [<*[0,0]*>,e] in X ; A7: for p being FinSequence of [:NAT,(QC-symbols F1()):] for e being Element of vSUB F1() st [p,e] in X holds [(<*[1,0]*> ^ p),e] in X proof let p be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: for e being Element of vSUB F1() st [p,e] in X holds [(<*[1,0]*> ^ p),e] in X let e be Element of vSUB F1(); ::_thesis: ( [p,e] in X implies [(<*[1,0]*> ^ p),e] in X ) assume [p,e] in X ; ::_thesis: [(<*[1,0]*> ^ p),e] in X then consider S being Element of QC-Sub-WFF F1() such that A8: S = [p,e] and A9: P1[S] ; P1[ Sub_not S] by A3, A9; then A10: Sub_not S in X ; consider p9 being Element of QC-WFF F1(), e9 being Element of vSUB F1() such that A11: S = [p9,e9] by Th8; A12: S `1 = p9 by A11, MCART_1:7; p = p9 by A8, A11, XTUPLE_0:1; hence [(<*[1,0]*> ^ p),e] in X by A8, A10, A12, MCART_1:7; ::_thesis: verum end; A13: for x being bound_QC-variable of F1() for p being FinSequence of [:NAT,(QC-symbols F1()):] for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in X proof let x be bound_QC-variable of F1(); ::_thesis: for p being FinSequence of [:NAT,(QC-symbols F1()):] for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in X let p be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: for e being Element of vSUB F1() st [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X holds [((<*[3,0]*> ^ <*x*>) ^ p),e] in X let e be Element of vSUB F1(); ::_thesis: ( [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X implies [((<*[3,0]*> ^ <*x*>) ^ p),e] in X ) assume [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] in X ; ::_thesis: [((<*[3,0]*> ^ <*x*>) ^ p),e] in X then consider S being Element of QC-Sub-WFF F1() such that A14: S = [p,((QSub F1()) . [((<*[3,0]*> ^ <*x*>) ^ p),e])] and A15: P1[S] ; consider B being set such that A16: B = [S,x] ; reconsider B = B as Element of [:(QC-Sub-WFF F1()),(bound_QC-variables F1()):] by A16; A17: ( B `1 = S & B `2 = x ) by A16, MCART_1:7; S `1 = p by A14, MCART_1:7; then A18: S `2 = (QSub F1()) . [(All (x,(S `1))),e] by A14, MCART_1:7; then A19: B is quantifiable by A17, Def22; then reconsider e = e as second_Q_comp of B by A18, A17, Def23; P1[ Sub_All (B,e)] by A5, A15, A16, A19; then Sub_All (B,e) in X ; then [(All ((B `2),((B `1) `1))),e] in X by A19, Def24; hence [((<*[3,0]*> ^ <*x*>) ^ p),e] in X by A14, A17, MCART_1:7; ::_thesis: verum end; let F be Element of QC-Sub-WFF F1(); ::_thesis: P1[F] A20: X c= [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] ) assume x in X ; ::_thesis: x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] then ex S being Element of QC-Sub-WFF F1() st ( x = S & P1[S] ) ; then consider p being Element of QC-WFF F1(), e being Element of vSUB F1() such that A21: x = [p,e] by Th8; p = @ p ; then p in [:NAT,(QC-symbols F1()):] * by FINSEQ_1:def_11; hence x in [:([:NAT,(QC-symbols F1()):] *),(vSUB F1()):] by A21, ZFMISC_1:def_2; ::_thesis: verum end; A22: for p, q being FinSequence of [:NAT,(QC-symbols F1()):] for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds [((<*[2,0]*> ^ p) ^ q),e] in X proof let p, q be FinSequence of [:NAT,(QC-symbols F1()):]; ::_thesis: for e being Element of vSUB F1() st [p,e] in X & [q,e] in X holds [((<*[2,0]*> ^ p) ^ q),e] in X let e be Element of vSUB F1(); ::_thesis: ( [p,e] in X & [q,e] in X implies [((<*[2,0]*> ^ p) ^ q),e] in X ) assume [p,e] in X ; ::_thesis: ( not [q,e] in X or [((<*[2,0]*> ^ p) ^ q),e] in X ) then consider S1 being Element of QC-Sub-WFF F1() such that A23: S1 = [p,e] and A24: P1[S1] ; assume [q,e] in X ; ::_thesis: [((<*[2,0]*> ^ p) ^ q),e] in X then consider S2 being Element of QC-Sub-WFF F1() such that A25: S2 = [q,e] and A26: P1[S2] ; consider p9 being Element of QC-WFF F1(), e1 being Element of vSUB F1() such that A27: [p,e] = [p9,e1] by A23, Th8; A28: e = e1 by A27, XTUPLE_0:1; A29: S1 `2 = e1 by A23, A27, MCART_1:7; then A30: S1 `2 = S2 `2 by A25, A28, MCART_1:7; then P1[ Sub_& (S1,S2)] by A4, A24, A26; then Sub_& (S1,S2) in X ; then A31: [((S1 `1) '&' (S2 `1)),(S1 `2)] in X by A30, Def21; A32: p = p9 by A27, XTUPLE_0:1; S1 `1 = p9 by A23, A27, MCART_1:7; hence [((<*[2,0]*> ^ p) ^ q),e] in X by A25, A32, A28, A29, A31, MCART_1:7; ::_thesis: verum end; for k being Element of NAT for P being QC-pred_symbol of k,F1() for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X proof let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1() for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X let P be QC-pred_symbol of k,F1(); ::_thesis: for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X let ll be QC-variable_list of k,F1(); ::_thesis: for e being Element of vSUB F1() holds [(<*P*> ^ ll),e] in X let e be Element of vSUB F1(); ::_thesis: [(<*P*> ^ ll),e] in X ( P1[ Sub_P (P,ll,e)] & [(P ! ll),e] = Sub_P (P,ll,e) ) by A1, Th9; then [(P ! ll),e] in X ; hence [(<*P*> ^ ll),e] in X by QC_LANG1:8; ::_thesis: verum end; then X is F1() -Sub-closed by A20, A6, A7, A22, A13, Def16; then QC-Sub-WFF F1() c= X by Def17; then F in X by TARSKI:def_3; then ex S being Element of QC-Sub-WFF F1() st ( S = F & P1[S] ) ; hence P1[F] ; ::_thesis: verum end; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; attrS is Sub_atomic means :Def25: :: SUBSTUT1:def 25 ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e); end; :: deftheorem Def25 defines Sub_atomic SUBSTUT1:def_25_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( S is Sub_atomic iff ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e) ); theorem Th11: :: SUBSTUT1:11 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_atomic holds S `1 is atomic proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_atomic holds S `1 is atomic let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_atomic implies S `1 is atomic ) assume S is Sub_atomic ; ::_thesis: S `1 is atomic then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that A1: S = Sub_P (P,ll,e) by Def25; S = [(P ! ll),e] by A1, Th9; then S `1 = P ! ll by MCART_1:7; hence S `1 is atomic by QC_LANG1:def_18; ::_thesis: verum end; registration let A be QC-alphabet ; let k be Element of NAT ; let P be QC-pred_symbol of k,A; let ll be QC-variable_list of k,A; let e be Element of vSUB A; cluster Sub_P (P,ll,e) -> Sub_atomic ; coherence Sub_P (P,ll,e) is Sub_atomic by Def25; end; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; attrS is Sub_negative means :Def26: :: SUBSTUT1:def 26 ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9; attrS is Sub_conjunctive means :Def27: :: SUBSTUT1:def 27 ex S1, S2 being Element of QC-Sub-WFF A st ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ); end; :: deftheorem Def26 defines Sub_negative SUBSTUT1:def_26_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( S is Sub_negative iff ex S9 being Element of QC-Sub-WFF A st S = Sub_not S9 ); :: deftheorem Def27 defines Sub_conjunctive SUBSTUT1:def_27_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( S is Sub_conjunctive iff ex S1, S2 being Element of QC-Sub-WFF A st ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; attrS is Sub_universal means :Def28: :: SUBSTUT1:def 28 ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B is quantifiable ); end; :: deftheorem Def28 defines Sub_universal SUBSTUT1:def_28_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( S is Sub_universal iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B is quantifiable ) ); theorem Th12: :: SUBSTUT1:12 for A being QC-alphabet for S being Element of QC-Sub-WFF A 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 ) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A 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 ) defpred S1[ Element of QC-Sub-WFF A] means ( \$1 is A -Sub_VERUM or \$1 is Sub_atomic or \$1 is Sub_negative or \$1 is Sub_conjunctive or \$1 is Sub_universal ); A1: for k being Element of NAT for p being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds S1[ Sub_P (p,ll,e)] ; A2: for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds S1[S] ; A3: for x being bound_QC-variable of A for S being Element of QC-Sub-WFF A for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] by Def28; A4: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds S1[ Sub_& (S1,S2)] by Def27; A5: for S being Element of QC-Sub-WFF A st S1[S] holds S1[ Sub_not S] by Def26; thus for S being Element of QC-Sub-WFF A holds S1[S] from SUBSTUT1:sch_1(A1, A2, A5, A4, A3); ::_thesis: verum end; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; assume B1: S is Sub_atomic ; func Sub_the_arguments_of S -> FinSequence of QC-variables A means :Def29: :: SUBSTUT1:def 29 ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( it = ll & S = Sub_P (P,ll,e) ); existence ex b1 being FinSequence of QC-variables A ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( b1 = ll & S = Sub_P (P,ll,e) ) proof consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that A1: S = Sub_P (P,ll,e) by B1, Def25; reconsider ll = ll as FinSequence of QC-variables A ; take ll ; ::_thesis: ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( ll = ll & S = Sub_P (P,ll,e) ) thus ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( ll = ll & S = Sub_P (P,ll,e) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of QC-variables A st ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( b1 = ll & S = Sub_P (P,ll,e) ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( b2 = ll & S = Sub_P (P,ll,e) ) holds b1 = b2 proof let ll1, ll2 be FinSequence of QC-variables A; ::_thesis: ( ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( ll1 = ll & S = Sub_P (P,ll,e) ) & ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( ll2 = ll & S = Sub_P (P,ll,e) ) implies ll1 = ll2 ) given k1 being Element of NAT , P1 being QC-pred_symbol of k1,A, ll19 being QC-variable_list of k1,A, e1 being Element of vSUB A such that A2: ll1 = ll19 and A3: S = Sub_P (P1,ll19,e1) ; ::_thesis: ( for k being Element of NAT for P being QC-pred_symbol of k,A for ll being QC-variable_list of k,A for e being Element of vSUB A holds ( not ll2 = ll or not S = Sub_P (P,ll,e) ) or ll1 = ll2 ) A4: S = [(P1 ! ll19),e1] by A3, Th9; given k2 being Element of NAT , P2 being QC-pred_symbol of k2,A, ll29 being QC-variable_list of k2,A, e2 being Element of vSUB A such that A5: ll2 = ll29 and A6: S = Sub_P (P2,ll29,e2) ; ::_thesis: ll1 = ll2 <*P1*> ^ ll19 = P1 ! ll19 by QC_LANG1:8; then A7: ( <*P2*> ^ ll29 = P2 ! ll29 & S `1 = <*P1*> ^ ll19 ) by A4, MCART_1:7, QC_LANG1:8; A8: S `1 is atomic by B1, Th11; A9: S = [(P2 ! ll29),e2] by A6, Th9; then A10: S `1 = P2 ! ll29 by MCART_1:7; S `1 = P1 ! ll19 by A4, MCART_1:7; then P1 = the_pred_symbol_of (S `1) by A8, QC_LANG1:def_22 .= P2 by A10, A8, QC_LANG1:def_22 ; hence ll1 = ll2 by A2, A5, A9, A7, FINSEQ_1:33, MCART_1:7; ::_thesis: verum end; end; :: deftheorem Def29 defines Sub_the_arguments_of SUBSTUT1:def_29_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_atomic holds for b3 being FinSequence of QC-variables A holds ( b3 = Sub_the_arguments_of S iff ex k being Element of NAT ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st ( b3 = ll & S = Sub_P (P,ll,e) ) ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; assume A1: S is Sub_negative ; func Sub_the_argument_of S -> Element of QC-Sub-WFF A means :Def30: :: SUBSTUT1:def 30 S = Sub_not it; existence ex b1 being Element of QC-Sub-WFF A st S = Sub_not b1 by A1, Def26; uniqueness for b1, b2 being Element of QC-Sub-WFF A st S = Sub_not b1 & S = Sub_not b2 holds b1 = b2 proof let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S = Sub_not S1 & S = Sub_not S2 implies S1 = S2 ) A1: ( S1 = [(S1 `1),(S1 `2)] & S2 = [(S2 `1),(S2 `2)] ) by Th10; assume A2: ( S = Sub_not S1 & S = Sub_not S2 ) ; ::_thesis: S1 = S2 then 'not' (S1 `1) = 'not' (S2 `1) by XTUPLE_0:1; then S1 `1 = S2 `1 by FINSEQ_1:33; hence S1 = S2 by A2, A1, XTUPLE_0:1; ::_thesis: verum end; end; :: deftheorem Def30 defines Sub_the_argument_of SUBSTUT1:def_30_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_negative holds for b3 being Element of QC-Sub-WFF A holds ( b3 = Sub_the_argument_of S iff S = Sub_not b3 ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; assume A1: S is Sub_conjunctive ; func Sub_the_left_argument_of S -> Element of QC-Sub-WFF A means :Def31: :: SUBSTUT1:def 31 ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (it,S9) & it `2 = S9 `2 ); existence ex b1, S9 being Element of QC-Sub-WFF A st ( S = Sub_& (b1,S9) & b1 `2 = S9 `2 ) by A1, Def27; uniqueness for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (b1,S9) & b1 `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (b2,S9) & b2 `2 = S9 `2 ) holds b1 = b2 proof let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S1,S9) & S1 `2 = S9 `2 ) & ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S2,S9) & S2 `2 = S9 `2 ) implies S1 = S2 ) given T1 being Element of QC-Sub-WFF A such that A1: ( S = Sub_& (S1,T1) & S1 `2 = T1 `2 ) ; ::_thesis: ( for S9 being Element of QC-Sub-WFF A holds ( not S = Sub_& (S2,S9) or not S2 `2 = S9 `2 ) or S1 = S2 ) given T2 being Element of QC-Sub-WFF A such that A2: ( S = Sub_& (S2,T2) & S2 `2 = T2 `2 ) ; ::_thesis: S1 = S2 A3: ( len (@ (S1 `1)) <= len (@ (S2 `1)) or len (@ (S2 `1)) <= len (@ (S1 `1)) ) ; A4: S = [((S2 `1) '&' (T2 `1)),(S2 `2)] by A2, Def21; A5: S = [((S1 `1) '&' (T1 `1)),(S1 `2)] by A1, Def21; then (S1 `1) '&' (T1 `1) = (S2 `1) '&' (T2 `1) by A4, XTUPLE_0:1; then <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (T1 `1))) = (S2 `1) '&' (T2 `1) by FINSEQ_1:32 .= <*[2,0]*> ^ ((@ (S2 `1)) ^ (@ (T2 `1))) by FINSEQ_1:32 ; then (@ (S1 `1)) ^ (@ (T1 `1)) = (@ (S2 `1)) ^ (@ (T2 `1)) by FINSEQ_1:33; then consider a, b, c, d being FinSequence such that A6: ( ( a = @ (S1 `1) & b = @ (S2 `1) ) or ( a = @ (S2 `1) & b = @ (S1 `1) ) ) and A7: ( len a <= len b & a ^ c = b ^ d ) by A3; A8: ( S1 = [(S1 `1),(S1 `2)] & S2 = [(S2 `1),(S2 `2)] ) by Th10; ex t being FinSequence st a ^ t = b by A7, FINSEQ_1:47; then S1 `1 = S2 `1 by A6, QC_LANG1:13; hence S1 = S2 by A5, A4, A8, XTUPLE_0:1; ::_thesis: verum end; end; :: deftheorem Def31 defines Sub_the_left_argument_of SUBSTUT1:def_31_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds for b3 being Element of QC-Sub-WFF A holds ( b3 = Sub_the_left_argument_of S iff ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (b3,S9) & b3 `2 = S9 `2 ) ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; assume B1: S is Sub_conjunctive ; func Sub_the_right_argument_of S -> Element of QC-Sub-WFF A means :Def32: :: SUBSTUT1:def 32 ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,it) & S9 `2 = it `2 ); existence ex b1, S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,b1) & S9 `2 = b1 `2 ) proof consider S1, S2 being Element of QC-Sub-WFF A such that A1: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by B1, Def27; take S2 ; ::_thesis: ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,S2) & S9 `2 = S2 `2 ) thus ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,S2) & S9 `2 = S2 `2 ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of QC-Sub-WFF A st ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,b1) & S9 `2 = b1 `2 ) & ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,b2) & S9 `2 = b2 `2 ) holds b1 = b2 proof let T1, T2 be Element of QC-Sub-WFF A; ::_thesis: ( ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,T1) & S9 `2 = T1 `2 ) & ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,T2) & S9 `2 = T2 `2 ) implies T1 = T2 ) given S1 being Element of QC-Sub-WFF A such that A2: ( S = Sub_& (S1,T1) & S1 `2 = T1 `2 ) ; ::_thesis: ( for S9 being Element of QC-Sub-WFF A holds ( not S = Sub_& (S9,T2) or not S9 `2 = T2 `2 ) or T1 = T2 ) A3: ( T1 = [(T1 `1),(T1 `2)] & T2 = [(T2 `1),(T2 `2)] ) by Th10; given S2 being Element of QC-Sub-WFF A such that A4: ( S = Sub_& (S2,T2) & S2 `2 = T2 `2 ) ; ::_thesis: T1 = T2 A5: S = [((S1 `1) '&' (T1 `1)),(T1 `2)] by A2, Def21; A6: S = [((S2 `1) '&' (T2 `1)),(T2 `2)] by A4, Def21; then (S1 `1) '&' (T1 `1) = (S2 `1) '&' (T2 `1) by A5, XTUPLE_0:1; then <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (T1 `1))) = (S2 `1) '&' (T2 `1) by FINSEQ_1:32 .= <*[2,0]*> ^ ((@ (S2 `1)) ^ (@ (T2 `1))) by FINSEQ_1:32 ; then A7: (@ (S1 `1)) ^ (@ (T1 `1)) = (@ (S2 `1)) ^ (@ (T2 `1)) by FINSEQ_1:33; S1 = Sub_the_left_argument_of S by B1, A2, Def31 .= S2 by B1, A4, Def31 ; then @ (T1 `1) = @ (T2 `1) by A7, FINSEQ_1:33; hence T1 = T2 by A5, A6, A3, XTUPLE_0:1; ::_thesis: verum end; end; :: deftheorem Def32 defines Sub_the_right_argument_of SUBSTUT1:def_32_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds for b3 being Element of QC-Sub-WFF A holds ( b3 = Sub_the_right_argument_of S iff ex S9 being Element of QC-Sub-WFF A st ( S = Sub_& (S9,b3) & S9 `2 = b3 `2 ) ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; assume B1: S is Sub_universal ; func Sub_the_bound_of S -> bound_QC-variable of A means :: SUBSTUT1:def 33 ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = it & B is quantifiable ); existence ex b1 being bound_QC-variable of A ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = b1 & B is quantifiable ) proof consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that A1: ( S = Sub_All (B,SQ) & B is quantifiable ) by B1, Def28; take B `2 ; ::_thesis: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = B `2 & B is quantifiable ) thus ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = B `2 & B is quantifiable ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being bound_QC-variable of A st ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = b1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = b2 & B is quantifiable ) holds b1 = b2 proof let x1, x2 be bound_QC-variable of A; ::_thesis: ( ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = x1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = x2 & B is quantifiable ) implies x1 = x2 ) assume that A2: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = x1 & B is quantifiable ) and A3: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = x2 & B is quantifiable ) ; ::_thesis: x1 = x2 consider B1 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ1 being second_Q_comp of B1 such that A4: S = Sub_All (B1,SQ1) and A5: B1 `2 = x1 and A6: B1 is quantifiable by A2; consider B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that A7: S = Sub_All (B2,SQ2) and A8: B2 `2 = x2 and A9: B2 is quantifiable by A3; A10: [(All ((B2 `2),((B2 `1) `1))),SQ2] = S by A7, A9, Def24; [(All ((B1 `2),((B1 `1) `1))),SQ1] = S by A4, A6, Def24; then All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A10, XTUPLE_0:1; hence x1 = x2 by A5, A8, QC_LANG2:5; ::_thesis: verum end; end; :: deftheorem defines Sub_the_bound_of SUBSTUT1:def_33_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_universal holds for b3 being bound_QC-variable of A holds ( b3 = Sub_the_bound_of S iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( S = Sub_All (B,SQ) & B `2 = b3 & B is quantifiable ) ); definition let A be QC-alphabet ; let A2 be Element of QC-Sub-WFF A; assume B1: A2 is Sub_universal ; func Sub_the_scope_of A2 -> Element of QC-Sub-WFF A means :Def34: :: SUBSTUT1:def 34 ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = it & B is quantifiable ); existence ex b1 being Element of QC-Sub-WFF A ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = b1 & B is quantifiable ) proof consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that A1: ( A2 = Sub_All (B,SQ) & B is quantifiable ) by B1, Def28; take B `1 ; ::_thesis: ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = B `1 & B is quantifiable ) thus ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = B `1 & B is quantifiable ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of QC-Sub-WFF A st ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = b1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = b2 & B is quantifiable ) holds b1 = b2 proof let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = S1 & B is quantifiable ) & ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = S2 & B is quantifiable ) implies S1 = S2 ) given B1 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ1 being second_Q_comp of B1 such that A2: A2 = Sub_All (B1,SQ1) and A3: B1 `1 = S1 and A4: B1 is quantifiable ; ::_thesis: ( for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ being second_Q_comp of B holds ( not A2 = Sub_All (B,SQ) or not B `1 = S2 or not B is quantifiable ) or S1 = S2 ) A5: A2 = [(All ((B1 `2),((B1 `1) `1))),SQ1] by A2, A4, Def24; A6: (B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A4, Def23; given B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ2 being second_Q_comp of B2 such that A7: A2 = Sub_All (B2,SQ2) and A8: B2 `1 = S2 and A9: B2 is quantifiable ; ::_thesis: S1 = S2 A10: ( B1 `1 = [((B1 `1) `1),((B1 `1) `2)] & B2 `1 = [((B2 `1) `1),((B2 `1) `2)] ) by Th10; A11: A2 = [(All ((B2 `2),((B2 `1) `1))),SQ2] by A7, A9, Def24; then All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A5, XTUPLE_0:1; then (B1 `1) `1 = (B2 `1) `1 by QC_LANG2:5; hence S1 = S2 by A3, A8, A9, A5, A11, A6, A10, Def23; ::_thesis: verum end; end; :: deftheorem Def34 defines Sub_the_scope_of SUBSTUT1:def_34_:_ for A being QC-alphabet for A2 being Element of QC-Sub-WFF A st A2 is Sub_universal holds for b3 being Element of QC-Sub-WFF A holds ( b3 = Sub_the_scope_of A2 iff ex B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] ex SQ being second_Q_comp of B st ( A2 = Sub_All (B,SQ) & B `1 = b3 & B is quantifiable ) ); registration let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; cluster Sub_not S -> Sub_negative ; coherence Sub_not S is Sub_negative proof take S ; :: according to SUBSTUT1:def_26 ::_thesis: Sub_not S = Sub_not S thus Sub_not S = Sub_not S ; ::_thesis: verum end; end; theorem Th13: :: SUBSTUT1:13 for A being QC-alphabet for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds Sub_& (S1,S2) is Sub_conjunctive proof let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds Sub_& (S1,S2) is Sub_conjunctive let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies Sub_& (S1,S2) is Sub_conjunctive ) assume A1: S1 `2 = S2 `2 ; ::_thesis: Sub_& (S1,S2) is Sub_conjunctive take S1 ; :: according to SUBSTUT1:def_27 ::_thesis: ex S2 being Element of QC-Sub-WFF A st ( Sub_& (S1,S2) = Sub_& (S1,S2) & S1 `2 = S2 `2 ) take S2 ; ::_thesis: ( Sub_& (S1,S2) = Sub_& (S1,S2) & S1 `2 = S2 `2 ) thus ( Sub_& (S1,S2) = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by A1; ::_thesis: verum end; theorem Th14: :: SUBSTUT1:14 for A being QC-alphabet for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ being second_Q_comp of B st B is quantifiable holds Sub_All (B,SQ) is Sub_universal proof let A be QC-alphabet ; ::_thesis: for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ being second_Q_comp of B st B is quantifiable holds Sub_All (B,SQ) is Sub_universal let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; ::_thesis: for SQ being second_Q_comp of B st B is quantifiable holds Sub_All (B,SQ) is Sub_universal let SQ be second_Q_comp of B; ::_thesis: ( B is quantifiable implies Sub_All (B,SQ) is Sub_universal ) assume A1: B is quantifiable ; ::_thesis: Sub_All (B,SQ) is Sub_universal take B ; :: according to SUBSTUT1:def_28 ::_thesis: ex SQ being second_Q_comp of B st ( Sub_All (B,SQ) = Sub_All (B,SQ) & B is quantifiable ) take SQ ; ::_thesis: ( Sub_All (B,SQ) = Sub_All (B,SQ) & B is quantifiable ) thus ( Sub_All (B,SQ) = Sub_All (B,SQ) & B is quantifiable ) by A1; ::_thesis: verum end; theorem :: SUBSTUT1:15 for A being QC-alphabet for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds S = S9 proof let A be QC-alphabet ; ::_thesis: for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds S = S9 let S, S9 be Element of QC-Sub-WFF A; ::_thesis: ( Sub_not S = Sub_not S9 implies S = S9 ) assume Sub_not S = Sub_not S9 ; ::_thesis: S = S9 then A1: ( 'not' (S `1) = 'not' (S9 `1) & S `2 = S9 `2 ) by XTUPLE_0:1; ( S = [(S `1),(S `2)] & S9 = [(S9 `1),(S9 `2)] ) by Th10; hence S = S9 by A1, FINSEQ_1:33; ::_thesis: verum end; theorem :: SUBSTUT1:16 for A being QC-alphabet for S being Element of QC-Sub-WFF A holds Sub_the_argument_of (Sub_not S) = S by Def30; theorem :: SUBSTUT1:17 for A being QC-alphabet for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds ( S1 = S19 & S2 = S29 ) proof let A be QC-alphabet ; ::_thesis: for S1, S2, S19, S29 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) holds ( S1 = S19 & S2 = S29 ) let S1, S2, S19, S29 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 & S19 `2 = S29 `2 & Sub_& (S1,S2) = Sub_& (S19,S29) implies ( S1 = S19 & S2 = S29 ) ) assume that A1: S1 `2 = S2 `2 and A2: S19 `2 = S29 `2 and A3: Sub_& (S1,S2) = Sub_& (S19,S29) ; ::_thesis: ( S1 = S19 & S2 = S29 ) Sub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, Def21; then [((S1 `1) '&' (S2 `1)),(S1 `2)] = [((S19 `1) '&' (S29 `1)),(S19 `2)] by A2, A3, Def21; then A4: ( (S1 `1) '&' (S2 `1) = (S19 `1) '&' (S29 `1) & S1 `2 = S19 `2 ) by XTUPLE_0:1; A5: ( S2 = [(S2 `1),(S2 `2)] & S29 = [(S29 `1),(S29 `2)] ) by Th10; ( S1 = [(S1 `1),(S1 `2)] & S19 = [(S19 `1),(S19 `2)] ) by Th10; hence ( S1 = S19 & S2 = S29 ) by A1, A2, A4, A5, QC_LANG2:2; ::_thesis: verum end; theorem Th18: :: SUBSTUT1:18 for A being QC-alphabet for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 proof let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 ) assume A1: S1 `2 = S2 `2 ; ::_thesis: Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 then Sub_& (S1,S2) is Sub_conjunctive by Th13; hence Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 by A1, Def31; ::_thesis: verum end; theorem Th19: :: SUBSTUT1:19 for A being QC-alphabet for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 proof let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 ) assume A1: S1 `2 = S2 `2 ; ::_thesis: Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 then Sub_& (S1,S2) is Sub_conjunctive by Th13; hence Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 by A1, Def32; ::_thesis: verum end; theorem :: SUBSTUT1:20 for A being QC-alphabet for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ1 being second_Q_comp of B1 for 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 proof let A be QC-alphabet ; ::_thesis: for B1, B2 being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ1 being second_Q_comp of B1 for 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 let B1, B2 be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; ::_thesis: for SQ1 being second_Q_comp of B1 for 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 let SQ1 be second_Q_comp of B1; ::_thesis: for 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 let SQ2 be second_Q_comp of B2; ::_thesis: ( B1 is quantifiable & B2 is quantifiable & Sub_All (B1,SQ1) = Sub_All (B2,SQ2) implies B1 = B2 ) assume that A1: B1 is quantifiable and A2: B2 is quantifiable and A3: Sub_All (B1,SQ1) = Sub_All (B2,SQ2) ; ::_thesis: B1 = B2 A4: ( Sub_All (B1,SQ1) = [(All ((B1 `2),((B1 `1) `1))),SQ1] & Sub_All (B2,SQ2) = [(All ((B2 `2),((B2 `1) `1))),SQ2] ) by A1, A2, Def24; then All ((B1 `2),((B1 `1) `1)) = All ((B2 `2),((B2 `1) `1)) by A3, XTUPLE_0:1; then A5: ( B1 `2 = B2 `2 & (B1 `1) `1 = (B2 `1) `1 ) by QC_LANG2:5; ex a, b being set st ( a in QC-Sub-WFF A & b in bound_QC-variables A & B2 = [a,b] ) by ZFMISC_1:def_2; then A6: B2 = [(B2 `1),(B2 `2)] by MCART_1:8; ex a, b being set st ( a in QC-Sub-WFF A & b in bound_QC-variables A & B1 = [a,b] ) by ZFMISC_1:def_2; then A7: B1 = [(B1 `1),(B1 `2)] by MCART_1:8; A8: ( B1 `1 = [((B1 `1) `1),((B1 `1) `2)] & B2 `1 = [((B2 `1) `1),((B2 `1) `2)] ) by Th10; (B1 `1) `2 = (QSub A) . [(All ((B1 `2),((B1 `1) `1))),SQ1] by A1, Def23; hence B1 = B2 by A2, A3, A4, A5, A8, A7, A6, Def23; ::_thesis: verum end; theorem Th21: :: SUBSTUT1:21 for A being QC-alphabet for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ being second_Q_comp of B st B is quantifiable holds Sub_the_scope_of (Sub_All (B,SQ)) = B `1 proof let A be QC-alphabet ; ::_thesis: for B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):] for SQ being second_Q_comp of B st B is quantifiable holds Sub_the_scope_of (Sub_All (B,SQ)) = B `1 let B be Element of [:(QC-Sub-WFF A),(bound_QC-variables A):]; ::_thesis: for SQ being second_Q_comp of B st B is quantifiable holds Sub_the_scope_of (Sub_All (B,SQ)) = B `1 let SQ be second_Q_comp of B; ::_thesis: ( B is quantifiable implies Sub_the_scope_of (Sub_All (B,SQ)) = B `1 ) assume A1: B is quantifiable ; ::_thesis: Sub_the_scope_of (Sub_All (B,SQ)) = B `1 then Sub_All (B,SQ) is Sub_universal by Th14; hence Sub_the_scope_of (Sub_All (B,SQ)) = B `1 by A1, Def34; ::_thesis: verum end; scheme :: SUBSTUT1:sch 2 SubQCInd2{ F1() -> QC-alphabet , P1[ Element of QC-Sub-WFF F1()] } : for S being Element of QC-Sub-WFF F1() holds P1[S] provided A1: for S being Element of QC-Sub-WFF F1() holds ( ( S is Sub_atomic implies P1[S] ) & ( S is F1() -Sub_VERUM implies P1[S] ) & ( S is Sub_negative & P1[ Sub_the_argument_of S] implies P1[S] ) & ( S is Sub_conjunctive & P1[ Sub_the_left_argument_of S] & P1[ Sub_the_right_argument_of S] implies P1[S] ) & ( S is Sub_universal & P1[ Sub_the_scope_of S] implies P1[S] ) ) proof A2: now__::_thesis:_for_x_being_bound_QC-variable_of_F1() for_S_being_Element_of_QC-Sub-WFF_F1() for_SQ_being_second_Q_comp_of_[S,x]_st_[S,x]_is_quantifiable_&_P1[S]_holds_ P1[_Sub_All_([S,x],SQ)] let x be bound_QC-variable of F1(); ::_thesis: for S being Element of QC-Sub-WFF F1() for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds P1[ Sub_All ([S,x],SQ)] let S be Element of QC-Sub-WFF F1(); ::_thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & P1[S] holds P1[ Sub_All ([S,x],SQ)] let SQ be second_Q_comp of [S,x]; ::_thesis: ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] ) assume that A3: [S,x] is quantifiable and A4: P1[S] ; ::_thesis: P1[ Sub_All ([S,x],SQ)] [S,x] `1 = Sub_the_scope_of (Sub_All ([S,x],SQ)) by A3, Th21; then A5: S = Sub_the_scope_of (Sub_All ([S,x],SQ)) ; Sub_All ([S,x],SQ) is Sub_universal by A3, Th14; hence P1[ Sub_All ([S,x],SQ)] by A1, A4, A5; ::_thesis: verum end; A6: now__::_thesis:_for_S1,_S2_being_Element_of_QC-Sub-WFF_F1()_st_S1_`2_=_S2_`2_&_P1[S1]_&_P1[S2]_holds_ P1[_Sub_&_(S1,S2)] let S1, S2 be Element of QC-Sub-WFF F1(); ::_thesis: ( S1 `2 = S2 `2 & P1[S1] & P1[S2] implies P1[ Sub_& (S1,S2)] ) assume that A7: S1 `2 = S2 `2 and A8: ( P1[S1] & P1[S2] ) ; ::_thesis: P1[ Sub_& (S1,S2)] A9: S2 = Sub_the_right_argument_of (Sub_& (S1,S2)) by A7, Th19; ( Sub_& (S1,S2) is Sub_conjunctive & S1 = Sub_the_left_argument_of (Sub_& (S1,S2)) ) by A7, Th13, Th18; hence P1[ Sub_& (S1,S2)] by A1, A8, A9; ::_thesis: verum end; A10: now__::_thesis:_for_S_being_Element_of_QC-Sub-WFF_F1()_st_P1[S]_holds_ P1[_Sub_not_S] let S be Element of QC-Sub-WFF F1(); ::_thesis: ( P1[S] implies P1[ Sub_not S] ) assume A11: P1[S] ; ::_thesis: P1[ Sub_not S] S = Sub_the_argument_of (Sub_not S) by Def30; hence P1[ Sub_not S] by A1, A11; ::_thesis: verum end; A12: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds P1[S] by A1; A13: for k being Element of NAT for P being QC-pred_symbol of k,F1() for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds P1[ Sub_P (P,ll,e)] by A1; thus for S being Element of QC-Sub-WFF F1() holds P1[S] from SUBSTUT1:sch_1(A13, A12, A10, A6, A2); ::_thesis: verum end; theorem Th22: :: SUBSTUT1:22 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_negative holds len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_negative holds len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_negative implies len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) ) assume S is Sub_negative ; ::_thesis: len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) then consider S9 being Element of QC-Sub-WFF A such that A1: S = Sub_not S9 by Def26; A2: 'not' (S9 `1) is negative by QC_LANG1:def_19; S `1 = 'not' (S9 `1) by A1, MCART_1:7; then A3: len (@ (the_argument_of ('not' (S9 `1)))) < len (@ (S `1)) by A2, QC_LANG1:14; (Sub_the_argument_of S) `1 = S9 `1 by A1, Def30; hence len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by A3, QC_LANG2:1; ::_thesis: verum end; theorem Th23: :: SUBSTUT1:23 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) let S be Element of QC-Sub-WFF A; ::_thesis: ( 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)) ) ) assume S is Sub_conjunctive ; ::_thesis: ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) then consider S1, S2 being Element of QC-Sub-WFF A such that A1: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by Def27; S = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, Def21; then A2: S `1 = (S1 `1) '&' (S2 `1) by MCART_1:7; (S1 `1) '&' (S2 `1) is conjunctive by QC_LANG1:def_20; then A3: ( len (@ (the_left_argument_of ((S1 `1) '&' (S2 `1)))) < len (@ (S `1)) & len (@ (the_right_argument_of ((S1 `1) '&' (S2 `1)))) < len (@ (S `1)) ) by A2, QC_LANG1:15; ( (Sub_the_right_argument_of S) `1 = S2 `1 & (Sub_the_left_argument_of S) `1 = S1 `1 ) by A1, Th18, Th19; hence ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) by A3, QC_LANG2:4; ::_thesis: verum end; theorem Th24: :: SUBSTUT1:24 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_universal holds len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_universal holds len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_universal implies len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) ) assume S is Sub_universal ; ::_thesis: len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) then consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that A1: ( S = Sub_All (B,SQ) & B is quantifiable ) by Def28; S = [(All ((B `2),((B `1) `1))),SQ] by A1, Def24; then A2: S `1 = All ((B `2),((B `1) `1)) by MCART_1:7; All ((B `2),((B `1) `1)) is universal by QC_LANG1:def_21; then A3: len (@ (the_scope_of (All ((B `2),((B `1) `1))))) < len (@ (S `1)) by A2, QC_LANG1:16; (Sub_the_scope_of S) `1 = (B `1) `1 by A1, Th21; hence len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by A3, QC_LANG2:7; ::_thesis: verum end; theorem Th25: :: SUBSTUT1:25 for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of 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 ) ) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of 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 ) ) let S be Element of QC-Sub-WFF A; ::_thesis: ( ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of 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 ) ) thus ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) ::_thesis: ( ( S is Sub_atomic implies ex k being Element of 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 ) ) proof assume S is A -Sub_VERUM ; ::_thesis: ((@ (S `1)) . 1) `1 = 0 then ex e being Element of vSUB A st S = [(VERUM A),e] by Def19; then S `1 = VERUM A by MCART_1:7; hence ((@ (S `1)) . 1) `1 = [0,0] `1 by FINSEQ_1:def_8 .= 0 ; ::_thesis: verum end; thus ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ) ::_thesis: ( ( 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 ) ) proof assume S is Sub_atomic ; ::_thesis: ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A then consider k being Element of NAT , P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A, e being Element of vSUB A such that A1: S = Sub_P (P,ll,e) by Def25; S = [(P ! ll),e] by A1, Th9; then S `1 = P ! ll by MCART_1:7; then @ (S `1) = <*P*> ^ ll by QC_LANG1:8; then (@ (S `1)) . 1 = P by FINSEQ_1:41; hence ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A ; ::_thesis: verum end; thus ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) ::_thesis: ( ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) ) proof assume S is Sub_negative ; ::_thesis: ((@ (S `1)) . 1) `1 = 1 then consider S9 being Element of QC-Sub-WFF A such that A2: S = Sub_not S9 by Def26; S `1 = 'not' (S9 `1) by A2, MCART_1:7; then (@ (S `1)) . 1 = [1,0] by FINSEQ_1:41; hence ((@ (S `1)) . 1) `1 = 1 by MCART_1:7; ::_thesis: verum end; thus ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) ::_thesis: ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) proof assume S is Sub_conjunctive ; ::_thesis: ((@ (S `1)) . 1) `1 = 2 then consider S1, S2 being Element of QC-Sub-WFF A such that A3: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by Def27; S = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A3, Def21; then S `1 = (S1 `1) '&' (S2 `1) by MCART_1:7; then @ (S `1) = <*[2,0]*> ^ ((@ (S1 `1)) ^ (@ (S2 `1))) by FINSEQ_1:32; then (@ (S `1)) . 1 = [2,0] by FINSEQ_1:41; hence ((@ (S `1)) . 1) `1 = 2 by MCART_1:7; ::_thesis: verum end; thus ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) ::_thesis: verum proof assume S is Sub_universal ; ::_thesis: ((@ (S `1)) . 1) `1 = 3 then consider B being Element of [:(QC-Sub-WFF A),(bound_QC-variables A):], SQ being second_Q_comp of B such that A4: ( S = Sub_All (B,SQ) & B is quantifiable ) by Def28; S = [(All ((B `2),((B `1) `1))),SQ] by A4, Def24; then S `1 = All ((B `2),((B `1) `1)) by MCART_1:7; then @ (S `1) = <*[3,0]*> ^ (<*(B `2)*> ^ (@ ((B `1) `1))) by FINSEQ_1:32; then (@ (S `1)) . 1 = [3,0] by FINSEQ_1:41; hence ((@ (S `1)) . 1) `1 = 3 by MCART_1:7; ::_thesis: verum end; end; theorem Th26: :: SUBSTUT1:26 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_atomic holds ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_atomic holds ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) let S be Element of QC-Sub-WFF A; ::_thesis: ( 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 ) ) assume S is Sub_atomic ; ::_thesis: ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) then ex k being Element of NAT st (@ (S `1)) . 1 is QC-pred_symbol of k,A by Th25; hence ( ((@ (S `1)) . 1) `1 <> 0 & ((@ (S `1)) . 1) `1 <> 1 & ((@ (S `1)) . 1) `1 <> 2 & ((@ (S `1)) . 1) `1 <> 3 ) by QC_LANG1:17; ::_thesis: verum end; theorem Th27: :: SUBSTUT1:27 for A being QC-alphabet for S being Element of QC-Sub-WFF A holds ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) ) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) ) let S be Element of QC-Sub-WFF A; ::_thesis: ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) ) A1: ( S is Sub_negative implies ((@ (S `1)) . 1) `1 = 1 ) by Th25; A2: ( S is Sub_conjunctive implies ((@ (S `1)) . 1) `1 = 2 ) by Th25; A3: ( S is Sub_universal implies ((@ (S `1)) . 1) `1 = 3 ) by Th25; ( S is A -Sub_VERUM implies ((@ (S `1)) . 1) `1 = 0 ) by Th25; hence ( not ( S is Sub_atomic & S is Sub_negative ) & not ( S is Sub_atomic & S is Sub_conjunctive ) & not ( S is Sub_atomic & S is Sub_universal ) & not ( S is Sub_negative & S is Sub_conjunctive ) & not ( S is Sub_negative & S is Sub_universal ) & not ( S is Sub_conjunctive & S is Sub_universal ) & not ( S is A -Sub_VERUM & S is Sub_atomic ) & not ( S is A -Sub_VERUM & S is Sub_negative ) & not ( S is A -Sub_VERUM & S is Sub_conjunctive ) & not ( S is A -Sub_VERUM & S is Sub_universal ) ) by A1, A2, A3, Th26; ::_thesis: verum end; scheme :: SUBSTUT1:sch 3 SubFuncEx{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( Element of QC-Sub-WFF F1()) -> Element of F2(), F5( Element of F2()) -> Element of F2(), F6( Element of F2(), Element of F2()) -> Element of F2(), F7( set , Element of QC-Sub-WFF F1(), Element of F2()) -> Element of F2() } : ex F being Function of (QC-Sub-WFF F1()),F2() st for S being Element of QC-Sub-WFF F1() for d1, d2 being Element of F2() holds ( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) proof defpred S1[ Function of (QC-Sub-WFF F1()),F2(), Element of NAT ] means for S being Element of QC-Sub-WFF F1() st len (@ (S `1)) <= \$2 holds ( ( S is F1() -Sub_VERUM implies \$1 . S = F3() ) & ( S is Sub_atomic implies \$1 . S = F4(S) ) & ( S is Sub_negative implies \$1 . S = F5((\$1 . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies \$1 . S = F6((\$1 . (Sub_the_left_argument_of S)),(\$1 . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies \$1 . S = F7(F1(),S,(\$1 . (Sub_the_scope_of S))) ) ); defpred S2[ Element of F2(), Function of (QC-Sub-WFF F1()),F2(), Element of QC-Sub-WFF F1()] means ( ( \$3 is F1() -Sub_VERUM implies \$1 = F3() ) & ( \$3 is Sub_atomic implies \$1 = F4(\$3) ) & ( \$3 is Sub_negative implies \$1 = F5((\$2 . (Sub_the_argument_of \$3))) ) & ( \$3 is Sub_conjunctive implies \$1 = F6((\$2 . (Sub_the_left_argument_of \$3)),(\$2 . (Sub_the_right_argument_of \$3))) ) & ( \$3 is Sub_universal implies \$1 = F7(F1(),\$3,(\$2 . (Sub_the_scope_of \$3))) ) ); defpred S3[ Element of NAT ] means ex F being Function of (QC-Sub-WFF F1()),F2() st S1[F,\$1]; defpred S4[ set , set ] means ex S being Element of QC-Sub-WFF F1() st ( S = \$1 & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S `1))] holds \$2 = g . S ) ); A1: for n being Element of NAT st S3[n] holds S3[n + 1] proof let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) given F being Function of (QC-Sub-WFF F1()),F2() such that A2: S1[F,n] ; ::_thesis: S3[n + 1] defpred S5[ Element of QC-Sub-WFF F1(), Element of F2()] means ( ( len (@ (\$1 `1)) <> n + 1 implies \$2 = F . \$1 ) & ( len (@ (\$1 `1)) = n + 1 implies S2[\$2,F,\$1] ) ); A3: for S being Element of QC-Sub-WFF F1() ex y being Element of F2() st S5[S,y] proof let S be Element of QC-Sub-WFF F1(); ::_thesis: ex y being Element of F2() st S5[S,y] now__::_thesis:_(_(_len_(@_(S_`1))_<>_n_+_1_&_ex_y_being_Element_of_F2()_st_y_=_F_._S_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_F1()_-Sub_VERUM_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_atomic_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_negative_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_conjunctive_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_or_(_len_(@_(S_`1))_=_n_+_1_&_S_is_Sub_universal_&_ex_y_being_Element_of_F2()_st_S2[y,F,S]_)_) percases ( len (@ (S `1)) <> n + 1 or ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM ) or ( len (@ (S `1)) = n + 1 & S is Sub_atomic ) or ( len (@ (S `1)) = n + 1 & S is Sub_negative ) or ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive ) or ( len (@ (S `1)) = n + 1 & S is Sub_universal ) ) by Th12; case len (@ (S `1)) <> n + 1 ; ::_thesis: ex y being Element of F2() st y = F . S take y = F . S; ::_thesis: y = F . S thus y = F . S ; ::_thesis: verum end; caseA4: ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S] take y = F3(); ::_thesis: S2[y,F,S] thus S2[y,F,S] by A4, Th27; ::_thesis: verum end; caseA5: ( len (@ (S `1)) = n + 1 & S is Sub_atomic ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S] take y = F4(S); ::_thesis: S2[y,F,S] thus S2[y,F,S] by A5, Th27; ::_thesis: verum end; caseA6: ( len (@ (S `1)) = n + 1 & S is Sub_negative ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S] take y = F5((F . (Sub_the_argument_of S))); ::_thesis: S2[y,F,S] thus S2[y,F,S] by A6, Th27; ::_thesis: verum end; caseA7: ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S] take y = F6((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))); ::_thesis: S2[y,F,S] thus S2[y,F,S] by A7, Th27; ::_thesis: verum end; caseA8: ( len (@ (S `1)) = n + 1 & S is Sub_universal ) ; ::_thesis: ex y being Element of F2() st S2[y,F,S] take y = F7(F1(),S,(F . (Sub_the_scope_of S))); ::_thesis: S2[y,F,S] thus S2[y,F,S] by A8, Th27; ::_thesis: verum end; end; end; hence ex y being Element of F2() st S5[S,y] ; ::_thesis: verum end; consider G being Function of (QC-Sub-WFF F1()),F2() such that A9: for S being Element of QC-Sub-WFF F1() holds S5[S,G . S] from FUNCT_2:sch_3(A3); take H = G; ::_thesis: S1[H,n + 1] thus S1[H,n + 1] ::_thesis: verum proof let S be Element of QC-Sub-WFF F1(); ::_thesis: ( len (@ (S `1)) <= n + 1 implies ( ( S is F1() -Sub_VERUM implies H . S = F3() ) & ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) ) assume A10: len (@ (S `1)) <= n + 1 ; ::_thesis: ( ( S is F1() -Sub_VERUM implies H . S = F3() ) & ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) thus ( S is F1() -Sub_VERUM implies H . S = F3() ) ::_thesis: ( ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) proof now__::_thesis:_(_S_is_F1()_-Sub_VERUM_implies_H_._S_=_F3()_) percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ; suppose len (@ (S `1)) <> n + 1 ; ::_thesis: ( S is F1() -Sub_VERUM implies H . S = F3() ) then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8; hence ( S is F1() -Sub_VERUM implies H . S = F3() ) by A2; ::_thesis: verum end; suppose len (@ (S `1)) = n + 1 ; ::_thesis: ( S is F1() -Sub_VERUM implies H . S = F3() ) hence ( S is F1() -Sub_VERUM implies H . S = F3() ) by A9; ::_thesis: verum end; end; end; hence ( S is F1() -Sub_VERUM implies H . S = F3() ) ; ::_thesis: verum end; thus ( S is Sub_atomic implies H . S = F4(S) ) ::_thesis: ( ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) proof now__::_thesis:_(_S_is_Sub_atomic_implies_H_._S_=_F4(S)_) percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ; suppose len (@ (S `1)) <> n + 1 ; ::_thesis: ( S is Sub_atomic implies H . S = F4(S) ) then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8; hence ( S is Sub_atomic implies H . S = F4(S) ) by A2; ::_thesis: verum end; suppose len (@ (S `1)) = n + 1 ; ::_thesis: ( S is Sub_atomic implies H . S = F4(S) ) hence ( S is Sub_atomic implies H . S = F4(S) ) by A9; ::_thesis: verum end; end; end; hence ( S is Sub_atomic implies H . S = F4(S) ) ; ::_thesis: verum end; thus ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) ::_thesis: ( ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) proof assume A11: S is Sub_negative ; ::_thesis: H . S = F5((H . (Sub_the_argument_of S))) then len (@ ((Sub_the_argument_of S) `1)) <> n + 1 by A10, Th22; then A12: H . (Sub_the_argument_of S) = F . (Sub_the_argument_of S) by A9; now__::_thesis:_H_._S_=_F5((H_._(Sub_the_argument_of_S))) percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ; suppose len (@ (S `1)) <> n + 1 ; ::_thesis: H . S = F5((H . (Sub_the_argument_of S))) then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8; hence H . S = F5((H . (Sub_the_argument_of S))) by A2, A11, A12; ::_thesis: verum end; suppose len (@ (S `1)) = n + 1 ; ::_thesis: H . S = F5((H . (Sub_the_argument_of S))) hence H . S = F5((H . (Sub_the_argument_of S))) by A9, A11, A12; ::_thesis: verum end; end; end; hence H . S = F5((H . (Sub_the_argument_of S))) ; ::_thesis: verum end; thus ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) ::_thesis: ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) proof assume A13: S is Sub_conjunctive ; ::_thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) then len (@ ((Sub_the_right_argument_of S) `1)) <> n + 1 by A10, Th23; then A14: H . (Sub_the_right_argument_of S) = F . (Sub_the_right_argument_of S) by A9; len (@ ((Sub_the_left_argument_of S) `1)) <> n + 1 by A10, A13, Th23; then A15: H . (Sub_the_left_argument_of S) = F . (Sub_the_left_argument_of S) by A9; now__::_thesis:_H_._S_=_F6((H_._(Sub_the_left_argument_of_S)),(H_._(Sub_the_right_argument_of_S))) percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ; suppose len (@ (S `1)) <> n + 1 ; ::_thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8; hence H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) by A2, A13, A15, A14; ::_thesis: verum end; suppose len (@ (S `1)) = n + 1 ; ::_thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) hence H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) by A9, A13, A15, A14; ::_thesis: verum end; end; end; hence H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ; ::_thesis: verum end; thus ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ::_thesis: verum proof assume A16: S is Sub_universal ; ::_thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) then len (@ ((Sub_the_scope_of S) `1)) <> n + 1 by A10, Th24; then A17: H . (Sub_the_scope_of S) = F . (Sub_the_scope_of S) by A9; now__::_thesis:_H_._S_=_F7(F1(),S,(H_._(Sub_the_scope_of_S))) percases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ; suppose len (@ (S `1)) <> n + 1 ; ::_thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8; hence H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) by A2, A16, A17; ::_thesis: verum end; suppose len (@ (S `1)) = n + 1 ; ::_thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) hence H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) by A9, A16, A17; ::_thesis: verum end; end; end; hence H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ; ::_thesis: verum end; end; end; A18: S3[ 0 ] proof set F = the Function of (QC-Sub-WFF F1()),F2(); take the Function of (QC-Sub-WFF F1()),F2() ; ::_thesis: S1[ the Function of (QC-Sub-WFF F1()),F2(), 0 ] let S be Element of QC-Sub-WFF F1(); ::_thesis: ( len (@ (S `1)) <= 0 implies ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) ) assume len (@ (S `1)) <= 0 ; ::_thesis: ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) hence ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) by QC_LANG1:10; ::_thesis: verum end; A19: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A18, A1); A20: for x being set st x in QC-Sub-WFF F1() holds ex y being set st S4[x,y] proof let x be set ; ::_thesis: ( x in QC-Sub-WFF F1() implies ex y being set st S4[x,y] ) assume x in QC-Sub-WFF F1() ; ::_thesis: ex y being set st S4[x,y] then reconsider x9 = x as Element of QC-Sub-WFF F1() ; consider F being Function of (QC-Sub-WFF F1()),F2() such that A21: S1[F, len (@ (x9 `1))] by A19; take F . x ; ::_thesis: S4[x,F . x] take x9 ; ::_thesis: ( x9 = x & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (x9 `1))] holds F . x = g . x9 ) ) thus x9 = x ; ::_thesis: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (x9 `1))] holds F . x = g . x9 let G be Function of (QC-Sub-WFF F1()),F2(); ::_thesis: ( S1[G, len (@ (x9 `1))] implies F . x = G . x9 ) assume A22: S1[G, len (@ (x9 `1))] ; ::_thesis: F . x = G . x9 defpred S5[ Element of QC-Sub-WFF F1()] means ( len (@ (\$1 `1)) <= len (@ (x9 `1)) implies F . \$1 = G . \$1 ); A23: now__::_thesis:_for_S_being_Element_of_QC-Sub-WFF_F1()_holds_ (_(_S_is_Sub_atomic_implies_S5[S]_)_&_(_S_is_F1()_-Sub_VERUM_implies_S5[S]_)_&_(_S_is_Sub_negative_&_S5[_Sub_the_argument_of_S]_implies_S5[S]_)_&_(_S_is_Sub_conjunctive_&_S5[_Sub_the_left_argument_of_S]_&_S5[_Sub_the_right_argument_of_S]_implies_S5[S]_)_&_(_S_is_Sub_universal_&_S5[_Sub_the_scope_of_S]_implies_S5[S]_)_) let S be Element of QC-Sub-WFF F1(); ::_thesis: ( ( S is Sub_atomic implies S5[S] ) & ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) ) thus ( S is Sub_atomic implies S5[S] ) ::_thesis: ( ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) ) proof assume A24: ( S is Sub_atomic & len (@ (S `1)) <= len (@ (x9 `1)) ) ; ::_thesis: F . S = G . S hence F . S = F4(S) by A21 .= G . S by A22, A24 ; ::_thesis: verum end; thus ( S is F1() -Sub_VERUM implies S5[S] ) ::_thesis: ( ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) ) proof assume A25: ( S is F1() -Sub_VERUM & len (@ (S `1)) <= len (@ (x9 `1)) ) ; ::_thesis: F . S = G . S hence F . S = F3() by A21 .= G . S by A22, A25 ; ::_thesis: verum end; thus ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) ::_thesis: ( ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) ) proof assume that A26: S is Sub_negative and A27: S5[ Sub_the_argument_of S] and A28: len (@ (S `1)) <= len (@ (x9 `1)) ; ::_thesis: F . S = G . S len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by A26, Th22; hence F . S = F5((G . (Sub_the_argument_of S))) by A21, A26, A27, A28, XXREAL_0:2 .= G . S by A22, A26, A28 ; ::_thesis: verum end; thus ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) ::_thesis: ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) proof assume that A29: S is Sub_conjunctive and A30: ( S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] ) and A31: len (@ (S `1)) <= len (@ (x9 `1)) ; ::_thesis: F . S = G . S ( len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) & len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) ) by A29, Th23; hence F . S = F6((G . (Sub_the_left_argument_of S)),(G . (Sub_the_right_argument_of S))) by A21, A29, A30, A31, XXREAL_0:2 .= G . S by A22, A29, A31 ; ::_thesis: verum end; thus ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) ::_thesis: verum proof assume that A32: S is Sub_universal and A33: S5[ Sub_the_scope_of S] and A34: len (@ (S `1)) <= len (@ (x9 `1)) ; ::_thesis: F . S = G . S len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by A32, Th24; hence F . S = F7(F1(),S,(G . (Sub_the_scope_of S))) by A21, A32, A33, A34, XXREAL_0:2 .= G . S by A22, A32, A34 ; ::_thesis: verum end; end; for S being Element of QC-Sub-WFF F1() holds S5[S] from SUBSTUT1:sch_2(A23); hence F . x = G . x9 ; ::_thesis: verum end; consider F being Function such that A35: dom F = QC-Sub-WFF F1() and A36: for x being set st x in QC-Sub-WFF F1() holds S4[x,F . x] from CLASSES1:sch_1(A20); rng F c= F2() proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in F2() ) assume y in rng F ; ::_thesis: y in F2() then consider x being set such that A37: ( x in QC-Sub-WFF F1() & y = F . x ) by A35, FUNCT_1:def_3; consider S being Element of QC-Sub-WFF F1() such that S = x and A38: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S `1))] holds y = g . S by A36, A37; consider G being Function of (QC-Sub-WFF F1()),F2() such that A39: S1[G, len (@ (S `1))] by A19; y = G . S by A38, A39; hence y in F2() ; ::_thesis: verum end; then reconsider F = F as Function of (QC-Sub-WFF F1()),F2() by A35, FUNCT_2:def_1, RELSET_1:4; take F ; ::_thesis: for S being Element of QC-Sub-WFF F1() for d1, d2 being Element of F2() holds ( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) let S be Element of QC-Sub-WFF F1(); ::_thesis: for d1, d2 being Element of F2() holds ( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) consider S1 being Element of QC-Sub-WFF F1() such that A40: S1 = S and A41: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds F . S = g . S1 by A36; let d1, d2 be Element of F2(); ::_thesis: ( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) consider G being Function of (QC-Sub-WFF F1()),F2() such that A42: S1[G, len (@ (S1 `1))] by A19; set S9 = Sub_the_scope_of S; A43: ex S1 being Element of QC-Sub-WFF F1() st ( S1 = Sub_the_scope_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds F . (Sub_the_scope_of S) = g . S1 ) ) by A36; A44: F . S = G . S by A40, A41, A42; hence ( S is F1() -Sub_VERUM implies F . S = F3() ) by A40, A42; ::_thesis: ( ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) thus ( S is Sub_atomic implies F . S = F4(S) ) by A40, A42, A44; ::_thesis: ( ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) A45: for k being Element of NAT st k < len (@ (S `1)) holds S1[G,k] proof let k be Element of NAT ; ::_thesis: ( k < len (@ (S `1)) implies S1[G,k] ) assume A46: k < len (@ (S `1)) ; ::_thesis: S1[G,k] let S9 be Element of QC-Sub-WFF F1(); ::_thesis: ( len (@ (S9 `1)) <= k implies ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) ) assume len (@ (S9 `1)) <= k ; ::_thesis: ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) then len (@ (S9 `1)) <= len (@ (S `1)) by A46, XXREAL_0:2; hence ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) by A40, A42; ::_thesis: verum end; thus ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) ::_thesis: ( ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) ) proof set S9 = Sub_the_argument_of S; set k = len (@ ((Sub_the_argument_of S) `1)); A47: ex S1 being Element of QC-Sub-WFF F1() st ( S1 = Sub_the_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds F . (Sub_the_argument_of S) = g . S1 ) ) by A36; assume A48: S is Sub_negative ; ::_thesis: ( not d1 = F . (Sub_the_argument_of S) or F . S = F5(d1) ) then len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by Th22; then S1[G, len (@ ((Sub_the_argument_of S) `1))] by A45; then F . (Sub_the_argument_of S) = G . (Sub_the_argument_of S) by A47; hence ( not d1 = F . (Sub_the_argument_of S) or F . S = F5(d1) ) by A40, A42, A44, A48; ::_thesis: verum end; thus ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) ::_thesis: ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) proof set S99 = Sub_the_right_argument_of S; set S9 = Sub_the_left_argument_of S; set k9 = len (@ ((Sub_the_left_argument_of S) `1)); set k99 = len (@ ((Sub_the_right_argument_of S) `1)); A49: ex S2 being Element of QC-Sub-WFF F1() st ( S2 = Sub_the_right_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S2 `1))] holds F . (Sub_the_right_argument_of S) = g . S2 ) ) by A36; assume A50: S is Sub_conjunctive ; ::_thesis: ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F6(d1,d2) ) then len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) by Th23; then A51: S1[G, len (@ ((Sub_the_left_argument_of S) `1))] by A45; len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) by A50, Th23; then S1[G, len (@ ((Sub_the_right_argument_of S) `1))] by A45; then A52: F . (Sub_the_right_argument_of S) = G . (Sub_the_right_argument_of S) by A49; ex S1 being Element of QC-Sub-WFF F1() st ( S1 = Sub_the_left_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds F . (Sub_the_left_argument_of S) = g . S1 ) ) by A36; then F . (Sub_the_left_argument_of S) = G . (Sub_the_left_argument_of S) by A51; hence ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F6(d1,d2) ) by A40, A42, A44, A50, A52; ::_thesis: verum end; set k = len (@ ((Sub_the_scope_of S) `1)); assume A53: S is Sub_universal ; ::_thesis: ( not d1 = F . (Sub_the_scope_of S) or F . S = F7(F1(),S,d1) ) then len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by Th24; then S1[G, len (@ ((Sub_the_scope_of S) `1))] by A45; then F . (Sub_the_scope_of S) = G . (Sub_the_scope_of S) by A43; hence ( not d1 = F . (Sub_the_scope_of S) or F . S = F7(F1(),S,d1) ) by A40, A42, A44, A53; ::_thesis: verum end; scheme :: SUBSTUT1:sch 4 SubQCFuncUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Function of (QC-Sub-WFF F1()),F2(), F4() -> Function of (QC-Sub-WFF F1()),F2(), F5() -> Element of F2(), F6( set ) -> Element of F2(), F7( set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9( set , set , set ) -> Element of F2() } : F3() = F4() provided A1: for S being Element of QC-Sub-WFF F1() for d1, d2 being Element of F2() holds ( ( S is F1() -Sub_VERUM implies F3() . S = F5() ) & ( S is Sub_atomic implies F3() . S = F6(S) ) & ( S is Sub_negative & d1 = F3() . (Sub_the_argument_of S) implies F3() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F3() . (Sub_the_left_argument_of S) & d2 = F3() . (Sub_the_right_argument_of S) implies F3() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F3() . (Sub_the_scope_of S) implies F3() . S = F9(F1(),S,d1) ) ) and A2: for S being Element of QC-Sub-WFF F1() for d1, d2 being Element of F2() holds ( ( S is F1() -Sub_VERUM implies F4() . S = F5() ) & ( S is Sub_atomic implies F4() . S = F6(S) ) & ( S is Sub_negative & d1 = F4() . (Sub_the_argument_of S) implies F4() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F4() . (Sub_the_left_argument_of S) & d2 = F4() . (Sub_the_right_argument_of S) implies F4() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F4() . (Sub_the_scope_of S) implies F4() . S = F9(F1(),S,d1) ) ) proof defpred S1[ Element of QC-Sub-WFF F1()] means F3() . \$1 = F4() . \$1; A3: for k being Element of NAT for P being QC-pred_symbol of k,F1() for l being QC-variable_list of k,F1() for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)] proof let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1() for l being QC-variable_list of k,F1() for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)] let P be QC-pred_symbol of k,F1(); ::_thesis: for l being QC-variable_list of k,F1() for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)] let l be QC-variable_list of k,F1(); ::_thesis: for e being Element of vSUB F1() holds S1[ Sub_P (P,l,e)] let e be Element of vSUB F1(); ::_thesis: S1[ Sub_P (P,l,e)] thus F3() . (Sub_P (P,l,e)) = F6((Sub_P (P,l,e))) by A1 .= F4() . (Sub_P (P,l,e)) by A2 ; ::_thesis: verum end; A4: for x being bound_QC-variable of F1() for S being Element of QC-Sub-WFF F1() for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] proof let x be bound_QC-variable of F1(); ::_thesis: for S being Element of QC-Sub-WFF F1() for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] let S be Element of QC-Sub-WFF F1(); ::_thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] let SQ be second_Q_comp of [S,x]; ::_thesis: ( [S,x] is quantifiable & S1[S] implies S1[ Sub_All ([S,x],SQ)] ) assume that A5: [S,x] is quantifiable and A6: F3() . S = F4() . S ; ::_thesis: S1[ Sub_All ([S,x],SQ)] A7: Sub_All ([S,x],SQ) is Sub_universal by A5, Th14; Sub_the_scope_of (Sub_All ([S,x],SQ)) = [S,x] `1 by A5, Th21; then Sub_the_scope_of (Sub_All ([S,x],SQ)) = S ; hence F3() . (Sub_All ([S,x],SQ)) = F9(F1(),(Sub_All ([S,x],SQ)),(F4() . (Sub_the_scope_of (Sub_All ([S,x],SQ))))) by A1, A6, A7 .= F4() . (Sub_All ([S,x],SQ)) by A2, A7 ; ::_thesis: verum end; A8: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds S1[S] proof let S be Element of QC-Sub-WFF F1(); ::_thesis: ( S is F1() -Sub_VERUM implies S1[S] ) assume A9: S is F1() -Sub_VERUM ; ::_thesis: S1[S] then F3() . S = F5() by A1; hence S1[S] by A2, A9; ::_thesis: verum end; A10: for S1, S2 being Element of QC-Sub-WFF F1() st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds S1[ Sub_& (S1,S2)] proof let S1, S2 be Element of QC-Sub-WFF F1(); ::_thesis: ( S1 `2 = S2 `2 & S1[S1] & S1[S2] implies S1[ Sub_& (S1,S2)] ) assume that A11: S1 `2 = S2 `2 and A12: ( F3() . S1 = F4() . S1 & F3() . S2 = F4() . S2 ) ; ::_thesis: S1[ Sub_& (S1,S2)] A13: Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 by A11, Th19; A14: ( Sub_& (S1,S2) is Sub_conjunctive & Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 ) by A11, Th13, Th18; hence F3() . (Sub_& (S1,S2)) = F8((F4() . S1),(F4() . S2)) by A1, A12, A13 .= F4() . (Sub_& (S1,S2)) by A2, A14, A13 ; ::_thesis: verum end; A15: for S being Element of QC-Sub-WFF F1() st S1[S] holds S1[ Sub_not S] proof let S be Element of QC-Sub-WFF F1(); ::_thesis: ( S1[S] implies S1[ Sub_not S] ) assume A16: F3() . S = F4() . S ; ::_thesis: S1[ Sub_not S] A17: Sub_the_argument_of (Sub_not S) = S by Def30; hence F3() . (Sub_not S) = F7((F4() . S)) by A1, A16 .= F4() . (Sub_not S) by A2, A17 ; ::_thesis: verum end; for S being Element of QC-Sub-WFF F1() holds S1[S] from SUBSTUT1:sch_1(A3, A8, A15, A10, A4); hence F3() = F4() by FUNCT_2:63; ::_thesis: verum end; definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; func @ S -> Element of [:(QC-WFF A),(vSUB A):] equals :: SUBSTUT1:def 35 S; coherence S is Element of [:(QC-WFF A),(vSUB A):] proof ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8; hence S is Element of [:(QC-WFF A),(vSUB A):] ; ::_thesis: verum end; end; :: deftheorem defines @ SUBSTUT1:def_35_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A holds @ S = S; definition let A be QC-alphabet ; let Z be Element of [:(QC-WFF A),(vSUB A):]; :: original: `1 redefine funcZ `1 -> Element of QC-WFF A; coherence Z `1 is Element of QC-WFF A proof ex a, b being set st ( a in QC-WFF A & b in vSUB A & [a,b] = Z ) by ZFMISC_1:def_2; hence Z `1 is Element of QC-WFF A by MCART_1:7; ::_thesis: verum end; :: original: `2 redefine funcZ `2 -> CQC_Substitution of A; coherence Z `2 is CQC_Substitution of A proof ex a, b being set st ( a in QC-WFF A & b in vSUB A & [a,b] = Z ) by ZFMISC_1:def_2; hence Z `2 is CQC_Substitution of A by MCART_1:7; ::_thesis: verum end; end; definition let A be QC-alphabet ; let Z be Element of [:(QC-WFF A),(vSUB A):]; 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); coherence ( ( bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) is bound_QC-variable of A ) & ( not bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies bound_in (Z `1) is bound_QC-variable of A ) ) ; consistency for b1 being bound_QC-variable of A holds verum ; end; :: deftheorem defines S_Bound SUBSTUT1:def_36_:_ for A being QC-alphabet for Z being Element of [:(QC-WFF A),(vSUB A):] holds ( ( bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies S_Bound Z = x. (upVar ((RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))),(the_scope_of (Z `1)))) ) & ( not bound_in (Z `1) in rng (RestrictSub ((bound_in (Z `1)),(Z `1),(Z `2))) implies S_Bound Z = bound_in (Z `1) ) ); definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; let p be QC-formula of A; func Quant (S,p) -> Element of QC-WFF A equals :: SUBSTUT1:def 37 All ((S_Bound (@ S)),p); coherence All ((S_Bound (@ S)),p) is Element of QC-WFF A ; end; :: deftheorem defines Quant SUBSTUT1:def_37_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A for p being QC-formula of A holds Quant (S,p) = All ((S_Bound (@ S)),p); Lm6: for A being QC-alphabet for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) & ( for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) holds F1 = F2 proof let A be QC-alphabet ; ::_thesis: for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) & ( for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) holds F1 = F2 let F1, F2 be Function of (QC-Sub-WFF A),(QC-WFF A); ::_thesis: ( ( for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F1 . S = 'not' (F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = (F1 . (Sub_the_left_argument_of S)) '&' (F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ) & ( for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ) implies F1 = F2 ) deffunc H1( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = \$1 '&' \$2; deffunc H2( Element of QC-WFF A) -> Element of QC-WFF A = 'not' \$1; deffunc H3( Element of QC-Sub-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of (\$1 `1)) ! (CQC_Subst ((Sub_the_arguments_of \$1),(\$1 `2))); assume for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = H3(S) ) & ( S is Sub_negative implies F1 . S = H2(F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = H1(F1 . (Sub_the_left_argument_of S),F1 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F1 . S = Quant (S,(F1 . (Sub_the_scope_of S))) ) ) ; ::_thesis: ( ex S being Element of QC-Sub-WFF A st ( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) & ( S is Sub_negative implies F2 . S = 'not' (F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = (F2 . (Sub_the_left_argument_of S)) '&' (F2 . (Sub_the_right_argument_of S)) ) implies ( S is Sub_universal & not F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) or F1 = F2 ) then A1: for S being Element of QC-Sub-WFF A for d1, d2 being Element of QC-WFF A holds ( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( S is Sub_atomic implies F1 . S = H3(S) ) & ( S is Sub_negative & d1 = F1 . (Sub_the_argument_of S) implies F1 . S = H2(d1) ) & ( S is Sub_conjunctive & d1 = F1 . (Sub_the_left_argument_of S) & d2 = F1 . (Sub_the_right_argument_of S) implies F1 . S = H1(d1,d2) ) & ( S is Sub_universal & d1 = F1 . (Sub_the_scope_of S) implies F1 . S = Quant (S,d1) ) ) ; assume for S being Element of QC-Sub-WFF A holds ( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = H3(S) ) & ( S is Sub_negative implies F2 . S = H2(F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = H1(F2 . (Sub_the_left_argument_of S),F2 . (Sub_the_right_argument_of S)) ) & ( S is Sub_universal implies F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) ; ::_thesis: F1 = F2 then A2: for S being Element of QC-Sub-WFF A for d1, d2 being Element of QC-WFF A holds ( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( S is Sub_atomic implies F2 . S = H3(S) ) & ( S is Sub_negative & d1 = F2 . (Sub_the_argument_of S) implies F2 . S = H2(d1) ) & ( S is Sub_conjunctive & d1 = F2 . (Sub_the_left_argument_of S) & d2 = F2 . (Sub_the_right_argument_of S) implies F2 . S = H1(d1,d2) ) & ( S is Sub_universal & d1 = F2 . (Sub_the_scope_of S) implies F2 . S = Quant (S,d1) ) ) ; thus F1 = F2 from SUBSTUT1:sch_4(A1, A2); ::_thesis: verum end; begin definition let A be QC-alphabet ; let S be Element of QC-Sub-WFF A; func CQC_Sub S -> Element of QC-WFF A means :Def38: :: 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))) ) ) ) ); existence ex b1 being Element of QC-WFF A ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( b1 = 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))) ) ) ) ) proof deffunc H1( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = \$1 '&' \$2; deffunc H2( Element of QC-WFF A) -> Element of QC-WFF A = 'not' \$1; deffunc H3( Element of QC-Sub-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of (\$1 `1)) ! (CQC_Subst ((Sub_the_arguments_of \$1),(\$1 `2))); consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that A1: for S being Element of QC-Sub-WFF A for d1, d2 being Element of QC-WFF A holds ( ( S is A -Sub_VERUM implies F . S = VERUM A ) & ( S is Sub_atomic implies F . S = H3(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = H2(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = H1(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = Quant (S,d1) ) ) from SUBSTUT1:sch_3(); take F . S ; ::_thesis: ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( F . S = 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))) ) ) ) ) take F ; ::_thesis: ( F . S = 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))) ) ) ) ) thus F . S = F . S ; ::_thesis: 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))) ) ) thus 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))) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of QC-WFF A st ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( b1 = 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))) ) ) ) ) & ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( b2 = 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))) ) ) ) ) holds b1 = b2 by Lm6; end; :: deftheorem Def38 defines CQC_Sub SUBSTUT1:def_38_:_ for A being QC-alphabet for S being Element of QC-Sub-WFF A for b3 being Element of QC-WFF A holds ( b3 = CQC_Sub S iff ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( b3 = 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))) ) ) ) ) ); theorem Th28: :: SUBSTUT1:28 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_negative holds CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S)) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_negative holds CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S)) let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_negative implies CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S)) ) consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that A1: CQC_Sub S = F . S and A2: 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))) ) ) by Def38; consider G being Function of (QC-Sub-WFF A),(QC-WFF A) such that A3: CQC_Sub (Sub_the_argument_of S) = G . (Sub_the_argument_of S) and A4: for S9 being Element of QC-Sub-WFF A holds ( ( S9 is A -Sub_VERUM implies G . S9 = VERUM A ) & ( S9 is Sub_atomic implies G . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies G . S9 = 'not' (G . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies G . S9 = (G . (Sub_the_left_argument_of S9)) '&' (G . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies G . S9 = Quant (S9,(G . (Sub_the_scope_of S9))) ) ) by Def38; F = G by A2, A4, Lm6; hence ( S is Sub_negative implies CQC_Sub S = 'not' (CQC_Sub (Sub_the_argument_of S)) ) by A1, A2, A3; ::_thesis: verum end; theorem Th29: :: SUBSTUT1:29 for A being QC-alphabet for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A holds CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) let S be Element of QC-Sub-WFF A; ::_thesis: CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) set 9S = Sub_not S; Sub_the_argument_of (Sub_not S) = S by Def30; hence CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) by Th28; ::_thesis: verum end; theorem Th30: :: SUBSTUT1:30 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_conjunctive holds CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_conjunctive implies CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) ) consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that A1: CQC_Sub S = F . S and A2: 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))) ) ) by Def38; consider F2 being Function of (QC-Sub-WFF A),(QC-WFF A) such that A3: CQC_Sub (Sub_the_right_argument_of S) = F2 . (Sub_the_right_argument_of S) and A4: for S9 being Element of QC-Sub-WFF A holds ( ( S9 is A -Sub_VERUM implies F2 . S9 = VERUM A ) & ( S9 is Sub_atomic implies F2 . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F2 . S9 = 'not' (F2 . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F2 . S9 = (F2 . (Sub_the_left_argument_of S9)) '&' (F2 . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F2 . S9 = Quant (S9,(F2 . (Sub_the_scope_of S9))) ) ) by Def38; A5: F2 = F by A2, A4, Lm6; consider F1 being Function of (QC-Sub-WFF A),(QC-WFF A) such that A6: CQC_Sub (Sub_the_left_argument_of S) = F1 . (Sub_the_left_argument_of S) and A7: for S9 being Element of QC-Sub-WFF A holds ( ( S9 is A -Sub_VERUM implies F1 . S9 = VERUM A ) & ( S9 is Sub_atomic implies F1 . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies F1 . S9 = 'not' (F1 . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies F1 . S9 = (F1 . (Sub_the_left_argument_of S9)) '&' (F1 . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies F1 . S9 = Quant (S9,(F1 . (Sub_the_scope_of S9))) ) ) by Def38; F1 = F by A2, A7, Lm6; hence ( S is Sub_conjunctive implies CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) ) by A1, A2, A6, A3, A5; ::_thesis: verum end; theorem Th31: :: SUBSTUT1:31 for A being QC-alphabet for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) proof let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( S1 `2 = S2 `2 implies CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) ) set S = Sub_& (S1,S2); assume A1: S1 `2 = S2 `2 ; ::_thesis: CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) then ( Sub_the_left_argument_of (Sub_& (S1,S2)) = S1 & Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 ) by Th18, Th19; hence CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) by A1, Th13, Th30; ::_thesis: verum end; theorem Th32: :: SUBSTUT1:32 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is Sub_universal holds CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is Sub_universal holds CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) let S be Element of QC-Sub-WFF A; ::_thesis: ( S is Sub_universal implies CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) ) consider F being Function of (QC-Sub-WFF A),(QC-WFF A) such that A1: CQC_Sub S = F . S and A2: 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))) ) ) by Def38; consider G being Function of (QC-Sub-WFF A),(QC-WFF A) such that A3: CQC_Sub (Sub_the_scope_of S) = G . (Sub_the_scope_of S) and A4: for S9 being Element of QC-Sub-WFF A holds ( ( S9 is A -Sub_VERUM implies G . S9 = VERUM A ) & ( S9 is Sub_atomic implies G . S9 = (the_pred_symbol_of (S9 `1)) ! (CQC_Subst ((Sub_the_arguments_of S9),(S9 `2))) ) & ( S9 is Sub_negative implies G . S9 = 'not' (G . (Sub_the_argument_of S9)) ) & ( S9 is Sub_conjunctive implies G . S9 = (G . (Sub_the_left_argument_of S9)) '&' (G . (Sub_the_right_argument_of S9)) ) & ( S9 is Sub_universal implies G . S9 = Quant (S9,(G . (Sub_the_scope_of S9))) ) ) by Def38; F = G by A2, A4, Lm6; hence ( S is Sub_universal implies CQC_Sub S = Quant (S,(CQC_Sub (Sub_the_scope_of S))) ) by A1, A2, A3; ::_thesis: verum end; definition let A be QC-alphabet ; func CQC-Sub-WFF A -> Subset of (QC-Sub-WFF A) equals :: SUBSTUT1:def 39 { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ; coherence { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } is Subset of (QC-Sub-WFF A) proof set X = { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ; { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } c= QC-Sub-WFF A proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } or a in QC-Sub-WFF A ) assume a in { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ; ::_thesis: a in QC-Sub-WFF A then ex S being Element of QC-Sub-WFF A st ( a = S & S `1 is Element of CQC-WFF A ) ; hence a in QC-Sub-WFF A ; ::_thesis: verum end; hence { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } is Subset of (QC-Sub-WFF A) ; ::_thesis: verum end; end; :: deftheorem defines CQC-Sub-WFF SUBSTUT1:def_39_:_ for A being QC-alphabet holds CQC-Sub-WFF A = { S where S is Element of QC-Sub-WFF A : S `1 is Element of CQC-WFF A } ; registration let A be QC-alphabet ; cluster CQC-Sub-WFF A -> non empty ; coherence not CQC-Sub-WFF A is empty proof set e = the Element of vSUB A; reconsider S = [(VERUM A), the Element of vSUB A] as Element of QC-Sub-WFF A by Def16; S `1 = VERUM A by MCART_1:7; then [(VERUM A), the Element of vSUB A] in CQC-Sub-WFF A ; hence not CQC-Sub-WFF A is empty ; ::_thesis: verum end; end; theorem Th33: :: SUBSTUT1:33 for A being QC-alphabet for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds CQC_Sub S is Element of CQC-WFF A proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st S is A -Sub_VERUM holds CQC_Sub S is Element of CQC-WFF A let S be Element of QC-Sub-WFF A; ::_thesis: ( S is A -Sub_VERUM implies CQC_Sub S is Element of CQC-WFF A ) assume A1: S is A -Sub_VERUM ; ::_thesis: CQC_Sub S is Element of CQC-WFF A ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( CQC_Sub S = 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))) ) ) ) ) by Def38; hence CQC_Sub S is Element of CQC-WFF A by A1; ::_thesis: verum end; Lm7: for A being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,A for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P proof let A be QC-alphabet ; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,A for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P let P be QC-pred_symbol of k,A; ::_thesis: for ll being CQC-variable_list of k,A holds the_pred_symbol_of (P ! ll) = P let ll be CQC-variable_list of k,A; ::_thesis: the_pred_symbol_of (P ! ll) = P A1: (<*P*> ^ ll) . 1 = P by FINSEQ_1:41; P ! ll is atomic by QC_LANG1:def_18; then consider k being Element of NAT , ll9 being QC-variable_list of k,A, P9 being QC-pred_symbol of k,A such that A2: ( the_pred_symbol_of (P ! ll) = P9 & P ! ll = P9 ! ll9 ) by QC_LANG1:def_22; ( P ! ll = <*P*> ^ ll & P9 ! ll9 = <*P9*> ^ ll9 ) by QC_LANG1:8; hence the_pred_symbol_of (P ! ll) = P by A2, A1, FINSEQ_1:41; ::_thesis: verum end; theorem Th34: :: SUBSTUT1:34 for A being QC-alphabet for k being Element of NAT 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 ) ) proof let A be QC-alphabet ; ::_thesis: for k being Element of NAT 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 ) ) let k be Element of NAT ; ::_thesis: 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 ) ) let h be FinSequence; ::_thesis: ( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) ) thus ( h is CQC-variable_list of k,A implies ( h is FinSequence of bound_QC-variables A & len h = k ) ) ::_thesis: ( h is FinSequence of bound_QC-variables A & len h = k implies h is CQC-variable_list of k,A ) proof assume A1: h is CQC-variable_list of k,A ; ::_thesis: ( h is FinSequence of bound_QC-variables A & len h = k ) then rng h c= bound_QC-variables A by RELAT_1:def_19; hence h is FinSequence of bound_QC-variables A by FINSEQ_1:def_4; ::_thesis: len h = k thus len h = k by A1, CARD_1:def_7; ::_thesis: verum end; thus ( h is FinSequence of bound_QC-variables A & len h = k implies h is CQC-variable_list of k,A ) ::_thesis: verum proof assume that A2: h is FinSequence of bound_QC-variables A and A3: len h = k ; ::_thesis: h is CQC-variable_list of k,A rng h c= bound_QC-variables A by A2, FINSEQ_1:def_4; then rng h c= QC-variables A by XBOOLE_1:1; hence h is CQC-variable_list of k,A by A2, A3, CARD_1:def_7, FINSEQ_1:def_4; ::_thesis: verum end; end; theorem Th35: :: SUBSTUT1:35 for A being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,A for ll being CQC-variable_list of k,A for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A proof let A be QC-alphabet ; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,A for ll being CQC-variable_list of k,A for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A for ll being CQC-variable_list of k,A for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A let P be QC-pred_symbol of k,A; ::_thesis: for ll being CQC-variable_list of k,A for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A let ll be CQC-variable_list of k,A; ::_thesis: for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A let e be Element of vSUB A; ::_thesis: CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A set l = Sub_the_arguments_of (Sub_P (P,ll,e)); A1: Sub_the_arguments_of (Sub_P (P,ll,e)) is CQC-variable_list of k,A by Def29; then reconsider l = Sub_the_arguments_of (Sub_P (P,ll,e)) as FinSequence of bound_QC-variables A by Th34; reconsider s = CQC_Subst (l,((Sub_P (P,ll,e)) `2)) as FinSequence of bound_QC-variables A ; len l = k by A1, CARD_1:def_7; then A2: len s = k by Def3; Sub_P (P,ll,e) = [(P ! ll),e] by Th9; then (Sub_P (P,ll,e)) `1 = P ! ll by MCART_1:7; then reconsider P9 = the_pred_symbol_of ((Sub_P (P,ll,e)) `1) as QC-pred_symbol of k,A by Lm7; reconsider s = s as CQC-variable_list of k,A by A2, Th34; ex F being Function of (QC-Sub-WFF A),(QC-WFF A) st ( CQC_Sub (Sub_P (P,ll,e)) = F . (Sub_P (P,ll,e)) & ( 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))) ) ) ) ) by Def38; then CQC_Sub (Sub_P (P,ll,e)) = P9 ! s ; hence CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A ; ::_thesis: verum end; theorem Th36: :: SUBSTUT1:36 for A being QC-alphabet for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds CQC_Sub (Sub_not S) is Element of CQC-WFF A proof let A be QC-alphabet ; ::_thesis: for S being Element of QC-Sub-WFF A st CQC_Sub S is Element of CQC-WFF A holds CQC_Sub (Sub_not S) is Element of CQC-WFF A let S be Element of QC-Sub-WFF A; ::_thesis: ( CQC_Sub S is Element of CQC-WFF A implies CQC_Sub (Sub_not S) is Element of CQC-WFF A ) set S9 = Sub_not S; assume A1: CQC_Sub S is Element of CQC-WFF A ; ::_thesis: CQC_Sub (Sub_not S) is Element of CQC-WFF A CQC_Sub (Sub_not S) = 'not' (CQC_Sub S) by Th29; hence CQC_Sub (Sub_not S) is Element of CQC-WFF A by A1, CQC_LANG:8; ::_thesis: verum end; theorem Th37: :: SUBSTUT1:37 for A being QC-alphabet for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A proof let A be QC-alphabet ; ::_thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A let S1, S2 be Element of QC-Sub-WFF A; ::_thesis: ( 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 ) assume A1: ( S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A ) ; ::_thesis: CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A ( S1 `2 = S2 `2 implies CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) ) by Th31; hence CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A by A1, CQC_LANG:9; ::_thesis: verum end; theorem Th38: :: SUBSTUT1:38 for A being QC-alphabet for x being bound_QC-variable of A for S being Element of QC-Sub-WFF A for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A proof let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A for S being Element of QC-Sub-WFF A for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A let x be bound_QC-variable of A; ::_thesis: for S being Element of QC-Sub-WFF A for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A let S be Element of QC-Sub-WFF A; ::_thesis: for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A let xSQ be second_Q_comp of [S,x]; ::_thesis: ( 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 ) set S9 = Sub_All ([S,x],xSQ); assume that A1: CQC_Sub S is Element of CQC-WFF A and A2: [S,x] is quantifiable ; ::_thesis: CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A Sub_the_scope_of (Sub_All ([S,x],xSQ)) = [S,x] `1 by A2, Th21; then Quant ((Sub_All ([S,x],xSQ)),(CQC_Sub (Sub_the_scope_of (Sub_All ([S,x],xSQ))))) = All ((S_Bound (@ (Sub_All ([S,x],xSQ)))),(CQC_Sub S)) ; then Quant ((Sub_All ([S,x],xSQ)),(CQC_Sub (Sub_the_scope_of (Sub_All ([S,x],xSQ))))) is Element of CQC-WFF A by A1, CQC_LANG:13; hence CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A by A2, Th14, Th32; ::_thesis: verum end; scheme :: SUBSTUT1:sch 5 SubCQCInd{ F1() -> QC-alphabet , P1[ set ] } : for S being Element of CQC-Sub-WFF F1() holds P1[S] provided A1: for S, S9 being Element of CQC-Sub-WFF F1() for x being bound_QC-variable of F1() for SQ being second_Q_comp of [S,x] for k being Element of NAT for ll being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() for e being Element of vSUB F1() holds ( P1[ Sub_P (P,ll,e)] & ( S is F1() -Sub_VERUM implies P1[S] ) & ( P1[S] implies P1[ Sub_not S] ) & ( S `2 = S9 `2 & P1[S] & P1[S9] implies P1[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & P1[S] implies P1[ Sub_All ([S,x],SQ)] ) ) proof defpred S1[ Element of QC-Sub-WFF F1()] means ( \$1 is Element of CQC-Sub-WFF F1() implies P1[\$1] ); A2: for S being Element of QC-Sub-WFF F1() st S1[S] holds S1[ Sub_not S] proof let S be Element of QC-Sub-WFF F1(); ::_thesis: ( S1[S] implies S1[ Sub_not S] ) assume A3: S1[S] ; ::_thesis: S1[ Sub_not S] assume Sub_not S is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_not S] then Sub_not S in CQC-Sub-WFF F1() ; then consider S9 being Element of QC-Sub-WFF F1() such that A4: Sub_not S = S9 and A5: S9 `1 is Element of CQC-WFF F1() ; S9 `1 = 'not' (S `1) by A4, MCART_1:7; then S `1 is Element of CQC-WFF F1() by A5, CQC_LANG:8; then S in CQC-Sub-WFF F1() ; hence P1[ Sub_not S] by A1, A3; ::_thesis: verum end; A6: for k being Element of NAT for P being QC-pred_symbol of k,F1() for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)] proof let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,F1() for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)] let P be QC-pred_symbol of k,F1(); ::_thesis: for ll being QC-variable_list of k,F1() for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)] let ll be QC-variable_list of k,F1(); ::_thesis: for e being Element of vSUB F1() holds S1[ Sub_P (P,ll,e)] let e be Element of vSUB F1(); ::_thesis: S1[ Sub_P (P,ll,e)] assume Sub_P (P,ll,e) is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_P (P,ll,e)] then Sub_P (P,ll,e) in CQC-Sub-WFF F1() ; then A7: ex S1 being Element of QC-Sub-WFF F1() st ( Sub_P (P,ll,e) = S1 & S1 `1 is Element of CQC-WFF F1() ) ; Sub_P (P,ll,e) = [(P ! ll),e] by Th9; then A8: P ! ll is Element of CQC-WFF F1() by A7, MCART_1:7; then A9: { (ll . j) where j is Element of NAT : ( 1 <= j & j <= len ll & ll . j in fixed_QC-variables F1() ) } = {} by CQC_LANG:7; { (ll . i) where i is Element of NAT : ( 1 <= i & i <= len ll & ll . i in free_QC-variables F1() ) } = {} by A8, CQC_LANG:7; then ll is CQC-variable_list of k,F1() by A9, CQC_LANG:5; hence P1[ Sub_P (P,ll,e)] by A1; ::_thesis: verum end; A10: for S1, S2 being Element of QC-Sub-WFF F1() st S1 `2 = S2 `2 & S1[S1] & S1[S2] holds S1[ Sub_& (S1,S2)] proof let S1, S2 be Element of QC-Sub-WFF F1(); ::_thesis: ( S1 `2 = S2 `2 & S1[S1] & S1[S2] implies S1[ Sub_& (S1,S2)] ) assume that A11: S1 `2 = S2 `2 and A12: ( S1[S1] & S1[S2] ) ; ::_thesis: S1[ Sub_& (S1,S2)] assume Sub_& (S1,S2) is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_& (S1,S2)] then Sub_& (S1,S2) in CQC-Sub-WFF F1() ; then consider S9 being Element of QC-Sub-WFF F1() such that A13: Sub_& (S1,S2) = S9 and A14: S9 `1 is Element of CQC-WFF F1() ; Sub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A11, Def21; then A15: S9 `1 = (S1 `1) '&' (S2 `1) by A13, MCART_1:7; then S2 `1 is Element of CQC-WFF F1() by A14, CQC_LANG:9; then A16: S2 in CQC-Sub-WFF F1() ; S1 `1 is Element of CQC-WFF F1() by A14, A15, CQC_LANG:9; then S1 in CQC-Sub-WFF F1() ; hence P1[ Sub_& (S1,S2)] by A1, A11, A12, A16; ::_thesis: verum end; A17: for x being bound_QC-variable of F1() for S being Element of QC-Sub-WFF F1() for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] proof let x be bound_QC-variable of F1(); ::_thesis: for S being Element of QC-Sub-WFF F1() for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] let S be Element of QC-Sub-WFF F1(); ::_thesis: for SQ being second_Q_comp of [S,x] st [S,x] is quantifiable & S1[S] holds S1[ Sub_All ([S,x],SQ)] let SQ be second_Q_comp of [S,x]; ::_thesis: ( [S,x] is quantifiable & S1[S] implies S1[ Sub_All ([S,x],SQ)] ) assume that A18: [S,x] is quantifiable and A19: S1[S] ; ::_thesis: S1[ Sub_All ([S,x],SQ)] assume Sub_All ([S,x],SQ) is Element of CQC-Sub-WFF F1() ; ::_thesis: P1[ Sub_All ([S,x],SQ)] then Sub_All ([S,x],SQ) in CQC-Sub-WFF F1() ; then consider S9 being Element of QC-Sub-WFF F1() such that A20: Sub_All ([S,x],SQ) = S9 and A21: S9 `1 is Element of CQC-WFF F1() ; Sub_All ([S,x],SQ) = [(All (([S,x] `2),(([S,x] `1) `1))),SQ] by A18, Def24; then S9 `1 = All (([S,x] `2),(([S,x] `1) `1)) by A20, MCART_1:7; then ([S,x] `1) `1 is Element of CQC-WFF F1() by A21, CQC_LANG:13; then S in CQC-Sub-WFF F1() ; hence P1[ Sub_All ([S,x],SQ)] by A1, A18, A19; ::_thesis: verum end; A22: for S being Element of QC-Sub-WFF F1() st S is F1() -Sub_VERUM holds S1[S] by A1; for S being Element of QC-Sub-WFF F1() holds S1[S] from SUBSTUT1:sch_1(A6, A22, A2, A10, A17); hence for S being Element of CQC-Sub-WFF F1() holds P1[S] ; ::_thesis: verum end; definition let A be QC-alphabet ; let S be Element of CQC-Sub-WFF A; :: original: CQC_Sub redefine func CQC_Sub S -> Element of CQC-WFF A; coherence CQC_Sub S is Element of CQC-WFF A proof defpred S1[ Element of QC-Sub-WFF A] means CQC_Sub \$1 is Element of CQC-WFF A; A1: for S, S9 being Element of CQC-Sub-WFF A for x being bound_QC-variable of A for SQ being second_Q_comp of [S,x] for k being Element of NAT for ll being CQC-variable_list of k,A for P being QC-pred_symbol of k,A for e being Element of vSUB A holds ( S1[ Sub_P (P,ll,e)] & ( S is A -Sub_VERUM implies S1[S] ) & ( S1[S] implies S1[ Sub_not S] ) & ( S `2 = S9 `2 & S1[S] & S1[S9] implies S1[ Sub_& (S,S9)] ) & ( [S,x] is quantifiable & S1[S] implies S1[ Sub_All ([S,x],SQ)] ) ) by Th33, Th35, Th36, Th37, Th38; for S being Element of CQC-Sub-WFF A holds S1[S] from SUBSTUT1:sch_5(A1); hence CQC_Sub S is Element of CQC-WFF A ; ::_thesis: verum end; end; theorem :: SUBSTUT1:39 for A being QC-alphabet for Sub being CQC_Substitution of A holds rng (@ Sub) c= bound_QC-variables A ;