:: SUBSTUT2 semantic presentation begin theorem Th1: :: SUBSTUT2:1 for Al being QC-alphabet for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = VERUM Al & S `2 = Sub ) proof let Al be QC-alphabet ; ::_thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = VERUM Al & S `2 = Sub ) let Sub be CQC_Substitution of Al; ::_thesis: ex S being Element of CQC-Sub-WFF Al st ( S `1 = VERUM Al & S `2 = Sub ) VERUM Al = <*[0,0]*> by QC_LANG1:def_14; then reconsider S = [(VERUM Al),Sub] as Element of QC-Sub-WFF Al by SUBSTUT1:def_16; take S ; ::_thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = VERUM Al & S `2 = Sub ) set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ; { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def_39; then A1: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds G in CQC-Sub-WFF Al ; S `1 = VERUM Al by MCART_1:7; then reconsider S = S as Element of CQC-Sub-WFF Al by A1; S `2 = Sub by MCART_1:7; hence ( S is Element of CQC-Sub-WFF Al & S `1 = VERUM Al & S `2 = Sub ) by MCART_1:7; ::_thesis: verum end; Lm1: for Al being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,Al for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds k = l proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,Al for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds k = l let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,Al for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds k = l let P be QC-pred_symbol of k,Al; ::_thesis: for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds k = l let k, l be Element of NAT ; ::_thesis: ( P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al implies k = l ) assume A1: ( P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al ) ; ::_thesis: k = l then P in l -ary_QC-pred_symbols Al ; then P in { P2 where P2 is Element of QC-pred_symbols Al : the_arity_of P2 = l } by QC_LANG1:def_9; then A2: ex P2 being Element of QC-pred_symbols Al st ( P2 = P & the_arity_of P2 = l ) ; P in k -ary_QC-pred_symbols Al by A1; then P in { P1 where P1 is Element of QC-pred_symbols Al : the_arity_of P1 = k } by QC_LANG1:def_9; then ex P1 being Element of QC-pred_symbols Al st ( P1 = P & the_arity_of P1 = k ) ; hence k = l by A2; ::_thesis: verum end; theorem Th2: :: SUBSTUT2:2 for Al being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,Al for ll being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = P ! ll & S `2 = Sub ) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,Al for ll being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = P ! ll & S `2 = Sub ) let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,Al for ll being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = P ! ll & S `2 = Sub ) let P be QC-pred_symbol of k,Al; ::_thesis: for ll being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = P ! ll & S `2 = Sub ) let ll be CQC-variable_list of k,Al; ::_thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = P ! ll & S `2 = Sub ) let Sub be CQC_Substitution of Al; ::_thesis: ex S being Element of CQC-Sub-WFF Al st ( S `1 = P ! ll & S `2 = Sub ) P is QC-pred_symbol of (the_arity_of P),Al by QC_LANG3:1; then k = the_arity_of P by Lm1; then ( [(<*P*> ^ ll),Sub] in QC-Sub-WFF Al & len ll = the_arity_of P ) by CARD_1:def_7, SUBSTUT1:def_16; then reconsider S = [(P ! ll),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def_12; set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ; { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def_39; then A1: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds G in CQC-Sub-WFF Al ; take S ; ::_thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = P ! ll & S `2 = Sub ) S `1 = P ! ll by MCART_1:7; then reconsider S = S as Element of CQC-Sub-WFF Al by A1; S `2 = Sub by MCART_1:7; hence ( S is Element of CQC-Sub-WFF Al & S `1 = P ! ll & S `2 = Sub ) by MCART_1:7; ::_thesis: verum end; theorem :: SUBSTUT2:3 for Al being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,Al for k, l being Element of NAT st P is QC-pred_symbol of k,Al & P is QC-pred_symbol of l,Al holds k = l by Lm1; theorem Th4: :: SUBSTUT2:4 for Al being QC-alphabet for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = 'not' p & S `2 = Sub ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = 'not' p & S `2 = Sub ) let p be Element of CQC-WFF Al; ::_thesis: ( ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = 'not' p & S `2 = Sub ) ) assume A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ; ::_thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = 'not' p & S `2 = Sub ) let Sub be CQC_Substitution of Al; ::_thesis: ex S being Element of CQC-Sub-WFF Al st ( S `1 = 'not' p & S `2 = Sub ) consider S being Element of CQC-Sub-WFF Al such that A2: ( S `1 = p & S `2 = Sub ) by A1; S = [p,Sub] by A2, SUBSTUT1:10; then [p,Sub] in QC-Sub-WFF Al ; then [(@ p),Sub] in QC-Sub-WFF Al by QC_LANG1:def_13; then [(<*[1,0]*> ^ (@ p)),Sub] in QC-Sub-WFF Al by SUBSTUT1:def_16; then reconsider S = [('not' p),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def_15; set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ; { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def_39; then A3: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds G in CQC-Sub-WFF Al ; take S ; ::_thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = 'not' p & S `2 = Sub ) S `1 = 'not' p by MCART_1:7; then reconsider S = S as Element of CQC-Sub-WFF Al by A3; S `2 = Sub by MCART_1:7; hence ( S is Element of CQC-Sub-WFF Al & S `1 = 'not' p & S `2 = Sub ) by MCART_1:7; ::_thesis: verum end; theorem Th5: :: SUBSTUT2:5 for Al being QC-alphabet for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = q & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p '&' q & S `2 = Sub ) proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = q & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p '&' q & S `2 = Sub ) let p, q be Element of CQC-WFF Al; ::_thesis: ( ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = q & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p '&' q & S `2 = Sub ) ) assume that A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) and A2: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = q & S `2 = Sub ) ; ::_thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p '&' q & S `2 = Sub ) let Sub be CQC_Substitution of Al; ::_thesis: ex S being Element of CQC-Sub-WFF Al st ( S `1 = p '&' q & S `2 = Sub ) consider S1 being Element of CQC-Sub-WFF Al such that A3: ( S1 `1 = p & S1 `2 = Sub ) by A1; consider S2 being Element of CQC-Sub-WFF Al such that A4: ( S2 `1 = q & S2 `2 = Sub ) by A2; S2 = [q,Sub] by A4, SUBSTUT1:10; then [q,Sub] in QC-Sub-WFF Al ; then A5: [(@ q),Sub] in QC-Sub-WFF Al by QC_LANG1:def_13; S1 = [p,Sub] by A3, SUBSTUT1:10; then [p,Sub] in QC-Sub-WFF Al ; then [(@ p),Sub] in QC-Sub-WFF Al by QC_LANG1:def_13; then [((<*[2,0]*> ^ (@ p)) ^ (@ q)),Sub] in QC-Sub-WFF Al by A5, SUBSTUT1:def_16; then reconsider S = [(p '&' q),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def_16; set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ; { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def_39; then A6: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds G in CQC-Sub-WFF Al ; take S ; ::_thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = p '&' q & S `2 = Sub ) S `1 = p '&' q by MCART_1:7; then reconsider S = S as Element of CQC-Sub-WFF Al by A6; S `2 = Sub by MCART_1:7; hence ( S is Element of CQC-Sub-WFF Al & S `1 = p '&' q & S `2 = Sub ) by MCART_1:7; ::_thesis: verum end; definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; let Sub be CQC_Substitution of Al; :: original: [ redefine func[p,Sub] -> Element of [:(QC-WFF Al),(vSUB Al):]; coherence [p,Sub] is Element of [:(QC-WFF Al),(vSUB Al):] by ZFMISC_1:def_2; end; theorem Th6: :: SUBSTUT2:6 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x} proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x} let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x} let x be bound_QC-variable of Al; ::_thesis: for Sub being CQC_Substitution of Al holds dom (RestrictSub (x,(All (x,p)),Sub)) misses {x} let Sub be CQC_Substitution of Al; ::_thesis: dom (RestrictSub (x,(All (x,p)),Sub)) misses {x} set finSub = RestrictSub (x,(All (x,p)),Sub); now__::_thesis:_not_dom_(RestrictSub_(x,(All_(x,p)),Sub))_meets_{x} set q = All (x,p); set X = { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } ; assume dom (RestrictSub (x,(All (x,p)),Sub)) meets {x} ; ::_thesis: contradiction then consider b being set such that A1: b in dom (RestrictSub (x,(All (x,p)),Sub)) and A2: b in {x} by XBOOLE_0:3; RestrictSub (x,(All (x,p)),Sub) = Sub | { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by SUBSTUT1:def_6; then RestrictSub (x,(All (x,p)),Sub) = (@ Sub) | { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by SUBSTUT1:def_2; then @ (RestrictSub (x,(All (x,p)),Sub)) = (@ Sub) | { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by SUBSTUT1:def_2; then dom (@ (RestrictSub (x,(All (x,p)),Sub))) = (dom (@ Sub)) /\ { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by RELAT_1:61; then A3: dom (@ (RestrictSub (x,(All (x,p)),Sub))) c= { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by XBOOLE_1:17; b in dom (@ (RestrictSub (x,(All (x,p)),Sub))) by A1, SUBSTUT1:def_2; then b in { y1 where y1 is bound_QC-variable of Al : ( y1 in still_not-bound_in (All (x,p)) & y1 is Element of dom Sub & y1 <> x & y1 <> Sub . y1 ) } by A3; then ex y being bound_QC-variable of Al st ( y = b & y in still_not-bound_in (All (x,p)) & y is Element of dom Sub & y <> x & y <> Sub . y ) ; hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; hence dom (RestrictSub (x,(All (x,p)),Sub)) misses {x} ; ::_thesis: verum end; theorem Th7: :: SUBSTUT2:7 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) let x be bound_QC-variable of Al; ::_thesis: for Sub being CQC_Substitution of Al st x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) let Sub be CQC_Substitution of Al; ::_thesis: ( x in rng (RestrictSub (x,(All (x,p)),Sub)) implies S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) ) set finSub = RestrictSub (x,(All (x,p)),Sub); set S = [(All (x,p)),Sub]; assume A1: x in rng (RestrictSub (x,(All (x,p)),Sub)) ; ::_thesis: S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) reconsider q = [(All (x,p)),Sub] `1 as Element of CQC-WFF Al ; A2: [(All (x,p)),Sub] `2 = Sub ; ( bound_in q = x & the_scope_of q = p ) by QC_LANG2:7; hence S_Bound [(All (x,p)),Sub] = x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)) by A1, A2, SUBSTUT1:def_36; ::_thesis: verum end; theorem Th8: :: SUBSTUT2:8 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x let x be bound_QC-variable of Al; ::_thesis: for Sub being CQC_Substitution of Al st not x in rng (RestrictSub (x,(All (x,p)),Sub)) holds S_Bound [(All (x,p)),Sub] = x let Sub be CQC_Substitution of Al; ::_thesis: ( not x in rng (RestrictSub (x,(All (x,p)),Sub)) implies S_Bound [(All (x,p)),Sub] = x ) set finSub = RestrictSub (x,(All (x,p)),Sub); set S = [(All (x,p)),Sub]; assume A1: not x in rng (RestrictSub (x,(All (x,p)),Sub)) ; ::_thesis: S_Bound [(All (x,p)),Sub] = x reconsider q = [(All (x,p)),Sub] `1 as Element of CQC-WFF Al ; ( [(All (x,p)),Sub] `2 = Sub & bound_in q = x ) by QC_LANG2:7; hence S_Bound [(All (x,p)),Sub] = x by A1, SUBSTUT1:def_36; ::_thesis: verum end; theorem Th9: :: SUBSTUT2:9 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) let x be bound_QC-variable of Al; ::_thesis: for Sub being CQC_Substitution of Al holds ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) let Sub be CQC_Substitution of Al; ::_thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) set finSub = RestrictSub (x,(All (x,p)),Sub); A1: now__::_thesis:_(_x_in_rng_(RestrictSub_(x,(All_(x,p)),Sub))_implies_ExpandSub_(x,p,(RestrictSub_(x,(All_(x,p)),Sub)))_=_(@_(RestrictSub_(x,(All_(x,p)),Sub)))_+*_(x_|_(S_Bound_[(All_(x,p)),Sub]))_) reconsider F = {[x,(x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)))]} as Function ; dom F = {x} by RELAT_1:9; then dom (RestrictSub (x,(All (x,p)),Sub)) misses dom F by Th6; then dom (@ (RestrictSub (x,(All (x,p)),Sub))) misses dom F by SUBSTUT1:def_2; then A2: (@ (RestrictSub (x,(All (x,p)),Sub))) \/ F = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F by FUNCT_4:31; assume A3: x in rng (RestrictSub (x,(All (x,p)),Sub)) ; ::_thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) then ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (RestrictSub (x,(All (x,p)),Sub)) \/ F by SUBSTUT1:def_13; then ( {[x,(x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p)))]} = x .--> (x. (upVar ((RestrictSub (x,(All (x,p)),Sub)),p))) & ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F ) by A2, FUNCT_4:82, SUBSTUT1:def_2; hence ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A3, Th7; ::_thesis: verum end; now__::_thesis:_(_not_x_in_rng_(RestrictSub_(x,(All_(x,p)),Sub))_implies_ExpandSub_(x,p,(RestrictSub_(x,(All_(x,p)),Sub)))_=_(@_(RestrictSub_(x,(All_(x,p)),Sub)))_+*_(x_|_(S_Bound_[(All_(x,p)),Sub]))_) reconsider F = {[x,x]} as Function ; dom F = {x} by RELAT_1:9; then dom (RestrictSub (x,(All (x,p)),Sub)) misses dom F by Th6; then dom (@ (RestrictSub (x,(All (x,p)),Sub))) misses dom F by SUBSTUT1:def_2; then A4: (@ (RestrictSub (x,(All (x,p)),Sub))) \/ F = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F by FUNCT_4:31; assume A5: not x in rng (RestrictSub (x,(All (x,p)),Sub)) ; ::_thesis: ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) then ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (RestrictSub (x,(All (x,p)),Sub)) \/ F by SUBSTUT1:def_13; then ( {[x,x]} = x .--> x & ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* F ) by A4, FUNCT_4:82, SUBSTUT1:def_2; hence ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A5, Th8; ::_thesis: verum end; hence ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A1; ::_thesis: verum end; theorem Th10: :: SUBSTUT2:10 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) let x be bound_QC-variable of Al; ::_thesis: for Sub being CQC_Substitution of Al for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) let Sub be CQC_Substitution of Al; ::_thesis: for S being Element of CQC-Sub-WFF Al st S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p holds ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) let S be Element of CQC-Sub-WFF Al; ::_thesis: ( S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) & S `1 = p implies ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) ) set Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])); reconsider Sub = Sub as CQC_Substitution of Al ; assume that A1: S `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) and A2: S `1 = p ; ::_thesis: ( [S,x] is quantifiable & ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] ) A3: ( [S,x] `2 = x & ([S,x] `1) `1 = p ) by A2; A4: ( the_scope_of (All (x,p)) = p & All (x,p) is universal ) by QC_LANG1:def_21, QC_LANG2:7; ( (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) = ExpandSub (x,p,(RestrictSub (x,(All (x,p)),Sub))) & bound_in (All (x,p)) = x ) by Th9, QC_LANG2:7; then All (x,p),Sub PQSub (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A4, SUBSTUT1:def_14; then consider a being set such that A5: a = [[(All (x,p)),Sub],((@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])))] and A6: All (x,p),Sub PQSub (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) ; a in QSub Al by A5, A6, SUBSTUT1:def_15; then A7: (QSub Al) . [(All (x,p)),Sub] = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A5, FUNCT_1:1; A8: ([S,x] `1) `2 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) by A1; hence [S,x] is quantifiable by A7, A3, SUBSTUT1:def_22; ::_thesis: ex S1 being Element of CQC-Sub-WFF Al st S1 = [(All (x,p)),Sub] A9: [S,x] is quantifiable by A7, A8, A3, SUBSTUT1:def_22; then reconsider Sub = Sub as second_Q_comp of [S,x] by A7, A8, A3, SUBSTUT1:def_23; take S1 = CQCSub_All ([S,x],Sub); ::_thesis: S1 = [(All (x,p)),Sub] S1 = Sub_All ([S,x],Sub) by A9, SUBLEMMA:def_5; hence S1 = [(All (x,p)),Sub] by A3, A9, SUBSTUT1:def_24; ::_thesis: verum end; theorem Th11: :: SUBSTUT2:11 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = All (x,p) & S `2 = Sub ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = All (x,p) & S `2 = Sub ) let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) holds for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = All (x,p) & S `2 = Sub ) let x be bound_QC-variable of Al; ::_thesis: ( ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = All (x,p) & S `2 = Sub ) ) assume A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) ; ::_thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = All (x,p) & S `2 = Sub ) let Sub be CQC_Substitution of Al; ::_thesis: ex S being Element of CQC-Sub-WFF Al st ( S `1 = All (x,p) & S `2 = Sub ) set Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])); ( (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) is CQC_Substitution of Al iff (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) ) by SUBSTUT1:def_1; then reconsider Sub1 = (@ (RestrictSub (x,(All (x,p)),Sub))) +* (x | (S_Bound [(All (x,p)),Sub])) as CQC_Substitution of Al by PARTFUN1:45; ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub1 ) by A1; then consider S1 being Element of CQC-Sub-WFF Al such that A2: S1 = [(All (x,p)),Sub] by Th10; take S1 ; ::_thesis: ( S1 `1 = All (x,p) & S1 `2 = Sub ) thus ( S1 `1 = All (x,p) & S1 `2 = Sub ) by A2, MCART_1:7; ::_thesis: verum end; theorem Th12: :: SUBSTUT2:12 for Al being QC-alphabet for p being Element of CQC-WFF Al for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) defpred S1[ Element of CQC-WFF Al] means for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st ( S `1 = $1 & S `2 = Sub ); A1: for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! ll] & ( S1[p] implies S1[ 'not' p] ) & ( S1[p] & S1[q] implies S1[p '&' q] ) & ( S1[p] implies S1[ All (x,p)] ) ) by Th1, Th2, Th4, Th5, Th11; thus for p being Element of CQC-WFF Al holds S1[p] from CQC_LANG:sch_1(A1); ::_thesis: verum end; definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; let Sub be CQC_Substitution of Al; :: original: [ redefine func[p,Sub] -> Element of CQC-Sub-WFF Al; coherence [p,Sub] is Element of CQC-Sub-WFF Al proof ex S being Element of CQC-Sub-WFF Al st ( S `1 = p & S `2 = Sub ) by Th12; hence [p,Sub] is Element of CQC-Sub-WFF Al by SUBSTUT1:10; ::_thesis: verum end; end; notation let Al be QC-alphabet ; let x, y be bound_QC-variable of Al; synonym Sbst (x,y) for Al .--> x; end; definition let Al be QC-alphabet ; let x, y be bound_QC-variable of Al; :: original: Sbst redefine func Sbst (x,y) -> CQC_Substitution of Al; coherence Sbst (y,) is CQC_Substitution of Al proof A1: ( x .--> y is CQC_Substitution of Al iff x .--> y is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) ) by SUBSTUT1:def_1; ( dom (x .--> y) = {x} & rng (x .--> y) = {y} ) by FUNCOP_1:8, FUNCOP_1:13; then x .--> y is PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) by RELSET_1:4; hence Sbst (y,) is CQC_Substitution of Al by A1, PARTFUN1:45; ::_thesis: verum end; end; begin definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; let x, y be bound_QC-variable of Al; funcp . (x,y) -> Element of CQC-WFF Al equals :: SUBSTUT2:def 1 CQC_Sub [p,(Sbst (x,y))]; coherence CQC_Sub [p,(Sbst (x,y))] is Element of CQC-WFF Al ; end; :: deftheorem defines . SUBSTUT2:def_1_:_ for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al holds p . (x,y) = CQC_Sub [p,(Sbst (x,y))]; scheme :: SUBSTUT2:sch 1 CQCInd1{ F1() -> QC-alphabet , P1[ set ] } : for p being Element of CQC-WFF F1() holds P1[p] provided A1: for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds P1[p] and A2: for k being Element of NAT st ( for p being Element of CQC-WFF F1() st QuantNbr p = k holds P1[p] ) holds for p being Element of CQC-WFF F1() st QuantNbr p = k + 1 holds P1[p] proof let p be Element of CQC-WFF F1(); ::_thesis: P1[p] defpred S1[ Element of NAT ] means for p being Element of CQC-WFF F1() st QuantNbr p = $1 holds P1[p]; A3: for k being Element of NAT st S1[k] holds S1[k + 1] by A2; A4: S1[ 0 ] by A1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A3); then S1[ QuantNbr p] ; hence P1[p] ; ::_thesis: verum end; scheme :: SUBSTUT2:sch 2 CQCInd2{ F1() -> QC-alphabet , P1[ set ] } : for p being Element of CQC-WFF F1() holds P1[p] provided A1: for p being Element of CQC-WFF F1() st QuantNbr p <= 0 holds P1[p] and A2: for k being Element of NAT st ( for p being Element of CQC-WFF F1() st QuantNbr p <= k holds P1[p] ) holds for p being Element of CQC-WFF F1() st QuantNbr p <= k + 1 holds P1[p] proof let p be Element of CQC-WFF F1(); ::_thesis: P1[p] defpred S1[ Element of NAT ] means for p being Element of CQC-WFF F1() st QuantNbr p <= $1 holds P1[p]; A3: for k being Element of NAT st S1[k] holds S1[k + 1] by A2; A4: S1[ 0 ] by A1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A3); then S1[ QuantNbr p] ; hence P1[p] ; ::_thesis: verum end; theorem :: SUBSTUT2:13 for Al being QC-alphabet for x, y being bound_QC-variable of Al holds (VERUM Al) . (x,y) = VERUM Al proof let Al be QC-alphabet ; ::_thesis: for x, y being bound_QC-variable of Al holds (VERUM Al) . (x,y) = VERUM Al let x, y be bound_QC-variable of Al; ::_thesis: (VERUM Al) . (x,y) = VERUM Al set S = [(VERUM Al),(Sbst (x,y))]; [(VERUM Al),(Sbst (x,y))] is Al -Sub_VERUM by SUBSTUT1:def_19; hence (VERUM Al) . (x,y) = VERUM Al by SUBLEMMA:3; ::_thesis: verum end; theorem :: SUBSTUT2:14 for Al being QC-alphabet for k being Element of NAT for x, y being bound_QC-variable of Al for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al holds ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for x, y being bound_QC-variable of Al for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al holds ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) let k be Element of NAT ; ::_thesis: for x, y being bound_QC-variable of Al for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al holds ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) let x, y be bound_QC-variable of Al; ::_thesis: for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al holds ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) let P be QC-pred_symbol of k,Al; ::_thesis: for l being CQC-variable_list of k,Al holds ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) let l be CQC-variable_list of k,Al; ::_thesis: ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) set S = [(P ! l),(Sbst (x,y))]; [(P ! l),(Sbst (x,y))] = Sub_P (P,l,(Sbst (x,y))) by SUBSTUT1:9; then A1: (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) by SUBLEMMA:8; QuantNbr (P ! (CQC_Subst (l,(Sbst (x,y))))) = 0 by CQC_SIM1:15; hence ( (P ! l) . (x,y) = P ! (CQC_Subst (l,(Sbst (x,y)))) & QuantNbr (P ! l) = QuantNbr ((P ! l) . (x,y)) ) by A1, CQC_SIM1:15; ::_thesis: verum end; theorem Th15: :: SUBSTUT2:15 for Al being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,Al for l being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) let P be QC-pred_symbol of k,Al; ::_thesis: for l being CQC-variable_list of k,Al for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) let l be CQC-variable_list of k,Al; ::_thesis: for Sub being CQC_Substitution of Al holds QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) let Sub be CQC_Substitution of Al; ::_thesis: QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) set S = [(P ! l),Sub]; [(P ! l),Sub] = Sub_P (P,l,Sub) by SUBSTUT1:9; then A1: CQC_Sub [(P ! l),Sub] = P ! (CQC_Subst (l,Sub)) by SUBLEMMA:8; QuantNbr (P ! (CQC_Subst (l,Sub))) = 0 by CQC_SIM1:15; hence QuantNbr (P ! l) = QuantNbr (CQC_Sub [(P ! l),Sub]) by A1, CQC_SIM1:15; ::_thesis: verum end; definition let Al be QC-alphabet ; let S be Element of QC-Sub-WFF Al; :: original: `2 redefine funcS `2 -> CQC_Substitution of Al; coherence S `2 is CQC_Substitution of Al proof ex p being Element of QC-WFF Al ex Sub being CQC_Substitution of Al st S = [p,Sub] by SUBSTUT1:8; hence S `2 is CQC_Substitution of Al by MCART_1:7; ::_thesis: verum end; end; theorem Th16: :: SUBSTUT2:16 for Al being QC-alphabet for p being Element of CQC-WFF Al for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub] proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub] let p be Element of CQC-WFF Al; ::_thesis: for Sub being CQC_Substitution of Al holds [('not' p),Sub] = Sub_not [p,Sub] let Sub be CQC_Substitution of Al; ::_thesis: [('not' p),Sub] = Sub_not [p,Sub] set S = [p,Sub]; Sub_not [p,Sub] = [('not' ([p,Sub] `1)),([p,Sub] `2)] by SUBSTUT1:def_20; hence [('not' p),Sub] = Sub_not [p,Sub] ; ::_thesis: verum end; theorem :: SUBSTUT2:17 for Al being QC-alphabet for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al holds ( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x, y being bound_QC-variable of Al holds ( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) ) let p be Element of CQC-WFF Al; ::_thesis: for x, y being bound_QC-variable of Al holds ( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) ) let x, y be bound_QC-variable of Al; ::_thesis: ( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) ) set S = [('not' p),(Sbst (x,y))]; A1: [('not' p),(Sbst (x,y))] = Sub_not [p,(Sbst (x,y))] by Th16; then A2: ('not' p) . (x,y) = 'not' (CQC_Sub [p,(Sbst (x,y))]) by SUBSTUT1:29; ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr (('not' p) . (x,y)) ) proof assume A3: QuantNbr p = QuantNbr (p . (x,y)) ; ::_thesis: QuantNbr ('not' p) = QuantNbr (('not' p) . (x,y)) QuantNbr (('not' p) . (x,y)) = QuantNbr (p . (x,y)) by A2, CQC_SIM1:16; hence QuantNbr ('not' p) = QuantNbr (('not' p) . (x,y)) by A3, CQC_SIM1:16; ::_thesis: verum end; hence ( 'not' (p . (x,y)) = 'not' (p . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) implies QuantNbr ('not' p) = QuantNbr ('not' (p . (x,y))) ) ) by A1, SUBSTUT1:29; ::_thesis: verum end; theorem Th18: :: SUBSTUT2:18 for Al being QC-alphabet for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) let p be Element of CQC-WFF Al; ::_thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) ) assume A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; ::_thesis: for Sub being CQC_Substitution of Al holds QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) let Sub be CQC_Substitution of Al; ::_thesis: QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) set S = [('not' p),Sub]; [('not' p),Sub] = Sub_not [p,Sub] by Th16; then QuantNbr (CQC_Sub [('not' p),Sub]) = QuantNbr ('not' (CQC_Sub [p,Sub])) by SUBSTUT1:29 .= QuantNbr (CQC_Sub [p,Sub]) by CQC_SIM1:16 .= QuantNbr p by A1 ; hence QuantNbr ('not' p) = QuantNbr (CQC_Sub [('not' p),Sub]) by CQC_SIM1:16; ::_thesis: verum end; theorem Th19: :: SUBSTUT2:19 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) let p, q be Element of CQC-WFF Al; ::_thesis: for Sub being CQC_Substitution of Al holds [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) let Sub be CQC_Substitution of Al; ::_thesis: [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) set S1 = [p,Sub]; set S2 = [q,Sub]; A1: ( [p,Sub] `1 = p & [q,Sub] `1 = q ) ; A2: ( [p,Sub] `2 = Sub & [q,Sub] `2 = Sub ) ; then CQCSub_& ([p,Sub],[q,Sub]) = Sub_& ([p,Sub],[q,Sub]) by SUBLEMMA:def_3; hence [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) by A2, A1, SUBSTUT1:def_21; ::_thesis: verum end; theorem :: SUBSTUT2:20 for Al being QC-alphabet for p, q being Element of CQC-WFF Al for x, y being bound_QC-variable of Al holds ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) ) proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al for x, y being bound_QC-variable of Al holds ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) ) let p, q be Element of CQC-WFF Al; ::_thesis: for x, y being bound_QC-variable of Al holds ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) ) let x, y be bound_QC-variable of Al; ::_thesis: ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) ) set S = [(p '&' q),(Sbst (x,y))]; set S1 = [p,(Sbst (x,y))]; set S2 = [q,(Sbst (x,y))]; A1: ( [p,(Sbst (x,y))] `2 = Sbst (x,y) & [q,(Sbst (x,y))] `2 = Sbst (x,y) ) ; [(p '&' q),(Sbst (x,y))] = CQCSub_& ([p,(Sbst (x,y))],[q,(Sbst (x,y))]) by Th19; then A2: [(p '&' q),(Sbst (x,y))] = Sub_& ([p,(Sbst (x,y))],[q,(Sbst (x,y))]) by A1, SUBLEMMA:def_3; then A3: (p '&' q) . (x,y) = (CQC_Sub [p,(Sbst (x,y))]) '&' (CQC_Sub [q,(Sbst (x,y))]) by A1, SUBSTUT1:31; ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) proof assume A4: ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) ) ; ::_thesis: QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) QuantNbr ((p '&' q) . (x,y)) = (QuantNbr (p . (x,y))) + (QuantNbr (q . (x,y))) by A3, CQC_SIM1:17; hence QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) by A4, CQC_SIM1:17; ::_thesis: verum end; hence ( (p '&' q) . (x,y) = (p . (x,y)) '&' (q . (x,y)) & ( QuantNbr p = QuantNbr (p . (x,y)) & QuantNbr q = QuantNbr (q . (x,y)) implies QuantNbr (p '&' q) = QuantNbr ((p '&' q) . (x,y)) ) ) by A1, A2, SUBSTUT1:31; ::_thesis: verum end; theorem Th21: :: SUBSTUT2:21 for Al being QC-alphabet for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) proof let Al be QC-alphabet ; ::_thesis: for p, q being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) let p, q be Element of CQC-WFF Al; ::_thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) & ( for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) ) assume that A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) and A2: for Sub being CQC_Substitution of Al holds QuantNbr q = QuantNbr (CQC_Sub [q,Sub]) ; ::_thesis: for Sub being CQC_Substitution of Al holds QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) let Sub be CQC_Substitution of Al; ::_thesis: QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) set S = [(p '&' q),Sub]; set S1 = [p,Sub]; set S2 = [q,Sub]; A3: ( [p,Sub] `2 = Sub & [q,Sub] `2 = Sub ) ; [(p '&' q),Sub] = CQCSub_& ([p,Sub],[q,Sub]) by Th19; then [(p '&' q),Sub] = Sub_& ([p,Sub],[q,Sub]) by A3, SUBLEMMA:def_3; then CQC_Sub [(p '&' q),Sub] = (CQC_Sub [p,Sub]) '&' (CQC_Sub [q,Sub]) by A3, SUBSTUT1:31; then QuantNbr (CQC_Sub [(p '&' q),Sub]) = (QuantNbr (CQC_Sub [p,Sub])) + (QuantNbr (CQC_Sub [q,Sub])) by CQC_SIM1:17 .= (QuantNbr p) + (QuantNbr (CQC_Sub [q,Sub])) by A1 .= (QuantNbr p) + (QuantNbr q) by A2 ; hence QuantNbr (p '&' q) = QuantNbr (CQC_Sub [(p '&' q),Sub]) by CQC_SIM1:17; ::_thesis: verum end; definition let Al be QC-alphabet ; func CFQ Al -> Function of (CQC-Sub-WFF Al),(vSUB Al) equals :: SUBSTUT2:def 2 (QSub Al) | (CQC-Sub-WFF Al); coherence (QSub Al) | (CQC-Sub-WFF Al) is Function of (CQC-Sub-WFF Al),(vSUB Al) proof now__::_thesis:_for_a_being_set_st_a_in_CQC-Sub-WFF_Al_holds_ a_in_dom_(QSub_Al) let a be set ; ::_thesis: ( a in CQC-Sub-WFF Al implies a in dom (QSub Al) ) assume a in CQC-Sub-WFF Al ; ::_thesis: a in dom (QSub Al) then consider p being Element of QC-WFF Al, Sub being CQC_Substitution of Al such that A1: a = [p,Sub] by SUBSTUT1:8; A2: now__::_thesis:_(_not_p_is_universal_implies_a_in_dom_(QSub_Al)_) set b = {} ; assume not p is universal ; ::_thesis: a in dom (QSub Al) then p,Sub PQSub {} by SUBSTUT1:def_14; then [[p,Sub],{}] in QSub Al by SUBSTUT1:def_15; hence a in dom (QSub Al) by A1, FUNCT_1:1; ::_thesis: verum end; now__::_thesis:_(_p_is_universal_implies_a_in_dom_(QSub_Al)_) set b = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))); assume p is universal ; ::_thesis: a in dom (QSub Al) then p,Sub PQSub ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) by SUBSTUT1:def_14; then [[p,Sub],(ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))))] in QSub Al by SUBSTUT1:def_15; hence a in dom (QSub Al) by A1, FUNCT_1:1; ::_thesis: verum end; hence a in dom (QSub Al) by A2; ::_thesis: verum end; then CQC-Sub-WFF Al c= dom (QSub Al) by TARSKI:def_3; then A3: dom ((QSub Al) | (CQC-Sub-WFF Al)) = CQC-Sub-WFF Al by RELAT_1:62; rng ((QSub Al) | (CQC-Sub-WFF Al)) c= vSUB Al proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng ((QSub Al) | (CQC-Sub-WFF Al)) or b in vSUB Al ) assume b in rng ((QSub Al) | (CQC-Sub-WFF Al)) ; ::_thesis: b in vSUB Al then consider a being set such that A4: ( a in dom ((QSub Al) | (CQC-Sub-WFF Al)) & ((QSub Al) | (CQC-Sub-WFF Al)) . a = b ) by FUNCT_1:def_3; A5: (QSub Al) | (CQC-Sub-WFF Al) c= QSub Al by RELAT_1:59; [a,b] in (QSub Al) | (CQC-Sub-WFF Al) by A4, FUNCT_1:1; then consider p being Element of QC-WFF Al, Sub being CQC_Substitution of Al, b1 being set such that A6: [a,b] = [[p,Sub],b1] and A7: p,Sub PQSub b1 by A5, SUBSTUT1:def_15; A8: now__::_thesis:_(_not_p_is_universal_implies_b_is_CQC_Substitution_of_Al_) A9: ( b1 is CQC_Substitution of Al iff b1 is Element of PFuncs ((bound_QC-variables Al),(bound_QC-variables Al)) ) by SUBSTUT1:def_1; assume not p is universal ; ::_thesis: b is CQC_Substitution of Al then b1 = {} by A7, SUBSTUT1:def_14; then b1 is PartFunc of (bound_QC-variables Al),(bound_QC-variables Al) by RELSET_1:12; hence b is CQC_Substitution of Al by A9, A6, PARTFUN1:45, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_(_p_is_universal_implies_b_is_CQC_Substitution_of_Al_) assume p is universal ; ::_thesis: b is CQC_Substitution of Al then b1 = ExpandSub ((bound_in p),(the_scope_of p),(RestrictSub ((bound_in p),p,Sub))) by A7, SUBSTUT1:def_14; hence b is CQC_Substitution of Al by A6, XTUPLE_0:1; ::_thesis: verum end; hence b in vSUB Al by A8; ::_thesis: verum end; hence (QSub Al) | (CQC-Sub-WFF Al) is Function of (CQC-Sub-WFF Al),(vSUB Al) by A3, FUNCT_2:2; ::_thesis: verum end; end; :: deftheorem defines CFQ SUBSTUT2:def_2_:_ for Al being QC-alphabet holds CFQ Al = (QSub Al) | (CQC-Sub-WFF Al); definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; let x be bound_QC-variable of Al; let Sub be CQC_Substitution of Al; func QScope (p,x,Sub) -> CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] equals :: SUBSTUT2:def 3 [[p,((CFQ Al) . [(All (x,p)),Sub])],x]; coherence [[p,((CFQ Al) . [(All (x,p)),Sub])],x] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] ; end; :: deftheorem defines QScope SUBSTUT2:def_3_:_ for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds QScope (p,x,Sub) = [[p,((CFQ Al) . [(All (x,p)),Sub])],x]; definition let Al be QC-alphabet ; let p be Element of CQC-WFF Al; let x be bound_QC-variable of Al; let Sub be CQC_Substitution of Al; func Qsc (p,x,Sub) -> second_Q_comp of QScope (p,x,Sub) equals :: SUBSTUT2:def 4 Sub; coherence Sub is second_Q_comp of QScope (p,x,Sub) proof A1: (QScope (p,x,Sub)) `1 = [p,((CFQ Al) . [(All (x,p)),Sub])] by MCART_1:7; then ((QScope (p,x,Sub)) `1) `2 = ((QSub Al) | (CQC-Sub-WFF Al)) . [(All (x,p)),Sub] by MCART_1:7; then A2: ((QScope (p,x,Sub)) `1) `2 = (QSub Al) . [(All (x,p)),Sub] by FUNCT_1:49; A3: ( (QScope (p,x,Sub)) `2 = x & ((QScope (p,x,Sub)) `1) `1 = p ) by A1, MCART_1:7; then QScope (p,x,Sub) is quantifiable by A2, SUBSTUT1:def_22; hence Sub is second_Q_comp of QScope (p,x,Sub) by A3, A2, SUBSTUT1:def_23; ::_thesis: verum end; end; :: deftheorem defines Qsc SUBSTUT2:def_4_:_ for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds Qsc (p,x,Sub) = Sub; theorem Th22: :: SUBSTUT2:22 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for Sub being CQC_Substitution of Al holds ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) let x be bound_QC-variable of Al; ::_thesis: for Sub being CQC_Substitution of Al holds ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) let Sub be CQC_Substitution of Al; ::_thesis: ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) set S = [p,((CFQ Al) . [(All (x,p)),Sub])]; set B = [[p,((CFQ Al) . [(All (x,p)),Sub])],x]; A1: ( [[p,((CFQ Al) . [(All (x,p)),Sub])],x] `2 = x & ([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `1 = p ) ; [(All (x,p)),Sub] in CQC-Sub-WFF Al ; then A2: [(All (x,p)),Sub] in dom (CFQ Al) by FUNCT_2:def_1; ([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `2 = (QSub Al) . [(All (([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `2),(([[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1) `1))),Sub] by A2, FUNCT_1:47; then A3: [[p,((CFQ Al) . [(All (x,p)),Sub])],x] is quantifiable by SUBSTUT1:def_22; then CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) = Sub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) by SUBLEMMA:def_5; hence ( [(All (x,p)),Sub] = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) & QScope (p,x,Sub) is quantifiable ) by A1, A3, SUBSTUT1:def_24; ::_thesis: verum end; theorem Th23: :: SUBSTUT2:23 for Al being QC-alphabet for p being Element of CQC-WFF Al for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) let p be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al st ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) holds for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) let x be bound_QC-variable of Al; ::_thesis: ( ( for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ) implies for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) ) assume A1: for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) ; ::_thesis: for Sub being CQC_Substitution of Al holds QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) let Sub be CQC_Substitution of Al; ::_thesis: QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) set S1 = [(All (x,p)),Sub]; set S = [p,((CFQ Al) . [(All (x,p)),Sub])]; set y = S_Bound (@ (CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))))); A2: QScope (p,x,Sub) is quantifiable by Th22; A3: Sub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) = CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub))) by Th22, SUBLEMMA:def_5 .= [(All (x,p)),Sub] by Th22 ; then A4: [(All (x,p)),Sub] is Sub_universal by A2, SUBSTUT1:def_28; then A5: CQC_Sub [(All (x,p)),Sub] = CQCQuant ([(All (x,p)),Sub],(CQC_Sub (CQCSub_the_scope_of [(All (x,p)),Sub]))) by SUBLEMMA:28; CQCSub_the_scope_of [(All (x,p)),Sub] = Sub_the_scope_of (Sub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub)))) by A3, A4, SUBLEMMA:def_6 .= [[p,((CFQ Al) . [(All (x,p)),Sub])],x] `1 by A2, SUBSTUT1:21 .= [p,((CFQ Al) . [(All (x,p)),Sub])] ; then CQC_Sub [(All (x,p)),Sub] = CQCQuant ((CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub)))),(CQC_Sub [p,((CFQ Al) . [(All (x,p)),Sub])])) by A5, Th22; then QuantNbr (CQC_Sub [(All (x,p)),Sub]) = QuantNbr (All ((S_Bound (@ (CQCSub_All ((QScope (p,x,Sub)),(Qsc (p,x,Sub)))))),(CQC_Sub [p,((CFQ Al) . [(All (x,p)),Sub])]))) by Th22, SUBLEMMA:31 .= (QuantNbr (CQC_Sub [p,((CFQ Al) . [(All (x,p)),Sub])])) + 1 by CQC_SIM1:18 .= (QuantNbr p) + 1 by A1 ; hence QuantNbr (All (x,p)) = QuantNbr (CQC_Sub [(All (x,p)),Sub]) by CQC_SIM1:18; ::_thesis: verum end; theorem Th24: :: SUBSTUT2:24 for Al being QC-alphabet for Sub being CQC_Substitution of Al holds QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub]) proof let Al be QC-alphabet ; ::_thesis: for Sub being CQC_Substitution of Al holds QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub]) let Sub be CQC_Substitution of Al; ::_thesis: QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub]) [(VERUM Al),Sub] is Al -Sub_VERUM by SUBSTUT1:def_19; hence QuantNbr (VERUM Al) = QuantNbr (CQC_Sub [(VERUM Al),Sub]) by SUBLEMMA:3; ::_thesis: verum end; theorem :: SUBSTUT2:25 for Al being QC-alphabet for p being Element of CQC-WFF Al for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for Sub being CQC_Substitution of Al holds QuantNbr p = QuantNbr (CQC_Sub [p,Sub]) defpred S1[ Element of CQC-WFF Al] means for Sub being CQC_Substitution of Al holds QuantNbr $1 = QuantNbr (CQC_Sub [$1,Sub]); A1: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by Th15, Th18, Th21, Th23, Th24; thus for r being Element of CQC-WFF Al holds S1[r] from CQC_LANG:sch_1(A1); ::_thesis: verum end; theorem :: SUBSTUT2:26 for Al being QC-alphabet for p being Element of CQC-WFF Al st p is atomic holds ex k being Element of NAT ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al st p is atomic holds ex k being Element of NAT ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll let p be Element of CQC-WFF Al; ::_thesis: ( p is atomic implies ex k being Element of NAT ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll ) assume p is atomic ; ::_thesis: ex k being Element of NAT ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll then consider k being Element of NAT , P being QC-pred_symbol of k,Al, l being QC-variable_list of k,Al such that A1: p = P ! l by QC_LANG1:def_18; A2: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables Al ) } = {} by A1, CQC_LANG:7; { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables Al ) } = {} by A1, CQC_LANG:7; then reconsider l = l as CQC-variable_list of k,Al by A2, CQC_LANG:5; take k ; ::_thesis: ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll take P ; ::_thesis: ex ll being CQC-variable_list of k,Al st p = P ! ll take l ; ::_thesis: p = P ! l thus p = P ! l by A1; ::_thesis: verum end; scheme :: SUBSTUT2:sch 3 CQCInd3{ F1() -> QC-alphabet , P1[ set ] } : for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds P1[p] provided A1: for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( P1[ VERUM F1()] & P1[P ! l] & ( P1[r] implies P1[ 'not' r] ) & ( P1[r] & P1[s] implies P1[r '&' s] ) ) proof defpred S1[ Element of CQC-WFF F1()] means ( QuantNbr $1 = 0 implies P1[$1] ); A2: for x being bound_QC-variable of F1() for p being Element of CQC-WFF F1() st S1[p] holds S1[ All (x,p)] proof let x be bound_QC-variable of F1(); ::_thesis: for p being Element of CQC-WFF F1() st S1[p] holds S1[ All (x,p)] let p be Element of CQC-WFF F1(); ::_thesis: ( S1[p] implies S1[ All (x,p)] ) assume S1[p] ; ::_thesis: S1[ All (x,p)] assume QuantNbr (All (x,p)) = 0 ; ::_thesis: P1[ All (x,p)] then (QuantNbr p) + 1 = 0 by CQC_SIM1:18; hence P1[ All (x,p)] ; ::_thesis: verum end; for p, q being Element of CQC-WFF F1() st S1[p] & S1[q] holds S1[p '&' q] proof let p, q be Element of CQC-WFF F1(); ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] ) assume A3: ( S1[p] & S1[q] ) ; ::_thesis: S1[p '&' q] assume QuantNbr (p '&' q) = 0 ; ::_thesis: P1[p '&' q] then (QuantNbr p) + (QuantNbr q) = 0 by CQC_SIM1:17; hence P1[p '&' q] by A1, A3; ::_thesis: verum end; then A4: for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( S1[ VERUM F1()] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A1, A2, CQC_SIM1:16; for p being Element of CQC-WFF F1() holds S1[p] from CQC_LANG:sch_1(A4); hence for p being Element of CQC-WFF F1() st QuantNbr p = 0 holds P1[p] ; ::_thesis: verum end; begin definition let Al be QC-alphabet ; let G, H be QC-formula of Al; assume A1: G is_subformula_of H ; mode PATH of G,H -> FinSequence means :Def5: :: SUBSTUT2:def 5 ( 1 <= len it & it . 1 = G & it . (len it) = H & ( for k being Element of NAT st 1 <= k & k < len it holds ex G1, H1 being Element of QC-WFF Al st ( it . k = G1 & it . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ); existence ex b1 being FinSequence st ( 1 <= len b1 & b1 . 1 = G & b1 . (len b1) = H & ( for k being Element of NAT st 1 <= k & k < len b1 holds ex G1, H1 being Element of QC-WFF Al st ( b1 . k = G1 & b1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) proof ex n being Element of NAT ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds ex G1, H1 being Element of QC-WFF Al st ( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by A1, QC_LANG2:def_20; then consider L being FinSequence such that A2: ex n being Element of NAT st ( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds ex G1, H1 being Element of QC-WFF Al st ( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) ; take L ; ::_thesis: ( 1 <= len L & L . 1 = G & L . (len L) = H & ( for k being Element of NAT st 1 <= k & k < len L holds ex G1, H1 being Element of QC-WFF Al st ( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) thus ( 1 <= len L & L . 1 = G & L . (len L) = H & ( for k being Element of NAT st 1 <= k & k < len L holds ex G1, H1 being Element of QC-WFF Al st ( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by A2; ::_thesis: verum end; end; :: deftheorem Def5 defines PATH SUBSTUT2:def_5_:_ for Al being QC-alphabet for G, H being QC-formula of Al st G is_subformula_of H holds for b4 being FinSequence holds ( b4 is PATH of G,H iff ( 1 <= len b4 & b4 . 1 = G & b4 . (len b4) = H & ( for k being Element of NAT st 1 <= k & k < len b4 holds ex G1, H1 being Element of QC-WFF Al st ( b4 . k = G1 & b4 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) ); theorem :: SUBSTUT2:27 for Al being QC-alphabet for i being Element of NAT for F1, F2 being QC-formula of Al for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) proof let Al be QC-alphabet ; ::_thesis: for i being Element of NAT for F1, F2 being QC-formula of Al for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) let i be Element of NAT ; ::_thesis: for F1, F2 being QC-formula of Al for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) let F1, F2 be QC-formula of Al; ::_thesis: for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <= len L holds ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) let L be PATH of F1,F2; ::_thesis: ( F1 is_subformula_of F2 & 1 <= i & i <= len L implies ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) ) set n = len L; assume that A1: F1 is_subformula_of F2 and A2: 1 <= i and A3: i <= len L ; ::_thesis: ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) (len L) + 1 <= (len L) + i by A2, XREAL_1:6; then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6; then A4: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6; i + (- i) <= (len L) + (- i) by A3, XREAL_1:6; then reconsider l = (len L) - i as Element of NAT by INT_1:3; defpred S1[ Element of NAT ] means ( $1 <= (len L) - 1 implies ex F3 being QC-formula of Al st ( F3 = L . ((len L) - $1) & F3 is_subformula_of F2 ) ); A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] assume A7: k + 1 <= (len L) - 1 ; ::_thesis: ex F3 being QC-formula of Al st ( F3 = L . ((len L) - (k + 1)) & F3 is_subformula_of F2 ) then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6; then A8: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6; then reconsider j = (len L) - k as Element of NAT by INT_1:3; len L <= (len L) + k by NAT_1:11; then (len L) + (- k) <= ((len L) + k) + (- k) by XREAL_1:6; then A9: j - 1 < len L by XREAL_1:146, XXREAL_0:2; A10: (1 + 1) + (- 1) <= j + (- 1) by A8, XREAL_1:6; then reconsider j1 = j - 1 as Element of NAT by INT_1:3; j1 + 1 = j ; then A11: ex G1, H1 being Element of QC-WFF Al st ( L . j1 = G1 & L . j = H1 & G1 is_immediate_constituent_of H1 ) by A1, A10, A9, Def5; then reconsider F3 = L . j1 as QC-formula of Al ; take F3 ; ::_thesis: ( F3 = L . ((len L) - (k + 1)) & F3 is_subformula_of F2 ) k < k + 1 by NAT_1:13; then F3 is_proper_subformula_of F2 by A6, A7, A11, QC_LANG2:63, XXREAL_0:2; hence ( F3 = L . ((len L) - (k + 1)) & F3 is_subformula_of F2 ) by QC_LANG2:def_21; ::_thesis: verum end; L . (len L) = F2 by A1, Def5; then A12: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A12, A5); then ex F3 being QC-formula of Al st ( F3 = L . ((len L) - l) & F3 is_subformula_of F2 ) by A4; hence ex F3 being QC-formula of Al st ( F3 = L . i & F3 is_subformula_of F2 ) ; ::_thesis: verum end; theorem Th28: :: SUBSTUT2:28 for Al being QC-alphabet for i being Element of NAT for p being Element of CQC-WFF Al for F1 being QC-formula of Al for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds L . i is Element of CQC-WFF Al proof let Al be QC-alphabet ; ::_thesis: for i being Element of NAT for p being Element of CQC-WFF Al for F1 being QC-formula of Al for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds L . i is Element of CQC-WFF Al let i be Element of NAT ; ::_thesis: for p being Element of CQC-WFF Al for F1 being QC-formula of Al for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds L . i is Element of CQC-WFF Al let p be Element of CQC-WFF Al; ::_thesis: for F1 being QC-formula of Al for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds L . i is Element of CQC-WFF Al let F1 be QC-formula of Al; ::_thesis: for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i <= len L holds L . i is Element of CQC-WFF Al let L be PATH of F1,p; ::_thesis: ( F1 is_subformula_of p & 1 <= i & i <= len L implies L . i is Element of CQC-WFF Al ) set n = len L; assume that A1: F1 is_subformula_of p and A2: 1 <= i and A3: i <= len L ; ::_thesis: L . i is Element of CQC-WFF Al (len L) + 1 <= (len L) + i by A2, XREAL_1:6; then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6; then A4: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6; i + (- i) <= (len L) + (- i) by A3, XREAL_1:6; then reconsider l = (len L) - i as Element of NAT by INT_1:3; defpred S1[ Element of NAT ] means ( $1 <= (len L) - 1 implies L . ((len L) - $1) is Element of CQC-WFF Al ); A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] assume A7: k + 1 <= (len L) - 1 ; ::_thesis: L . ((len L) - (k + 1)) is Element of CQC-WFF Al then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6; then A8: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6; then reconsider j = (len L) - k as Element of NAT by INT_1:3; k < k + 1 by NAT_1:13; then reconsider q = L . j as Element of CQC-WFF Al by A6, A7, XXREAL_0:2; len L <= (len L) + k by NAT_1:11; then (len L) + (- k) <= ((len L) + k) + (- k) by XREAL_1:6; then A9: j - 1 < len L by XREAL_1:146, XXREAL_0:2; A10: (1 + 1) + (- 1) <= j + (- 1) by A8, XREAL_1:6; then reconsider j1 = j - 1 as Element of NAT by INT_1:3; j1 + 1 = j ; then consider G1, H1 being Element of QC-WFF Al such that A11: L . j1 = G1 and A12: ( q = H1 & G1 is_immediate_constituent_of H1 ) by A1, A10, A9, Def5; A13: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:9; A14: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:13; A15: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:9; ( q = 'not' G1 implies L . ((len L) - (k + 1)) is Element of CQC-WFF Al ) by A11, CQC_LANG:8; hence L . ((len L) - (k + 1)) is Element of CQC-WFF Al by A12, A13, A15, A14, QC_LANG2:def_19; ::_thesis: verum end; A16: S1[ 0 ] by A1, Def5; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A16, A5); then L . ((len L) - l) is Element of CQC-WFF Al by A4; hence L . i is Element of CQC-WFF Al ; ::_thesis: verum end; theorem Th29: :: SUBSTUT2:29 for Al being QC-alphabet for n, i being Element of NAT for q, p being Element of CQC-WFF Al for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) proof let Al be QC-alphabet ; ::_thesis: for n, i being Element of NAT for q, p being Element of CQC-WFF Al for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) let n, i be Element of NAT ; ::_thesis: for q, p being Element of CQC-WFF Al for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) let q, p be Element of CQC-WFF Al; ::_thesis: for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) let L be PATH of q,p; ::_thesis: ( QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L implies ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) ) set m = len L; assume that A1: QuantNbr p <= n and A2: q is_subformula_of p and A3: 1 <= i and A4: i <= len L ; ::_thesis: ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) i + (- i) <= (len L) + (- i) by A4, XREAL_1:6; then reconsider l = (len L) - i as Element of NAT by INT_1:3; (len L) + 1 <= (len L) + i by A3, XREAL_1:6; then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6; then A5: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6; defpred S1[ Element of NAT ] means ( $1 <= (len L) - 1 implies ex r being Element of CQC-WFF Al st ( r = L . ((len L) - $1) & QuantNbr r <= n ) ); A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: S1[k] ; ::_thesis: S1[k + 1] assume A8: k + 1 <= (len L) - 1 ; ::_thesis: ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6; then A9: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6; then reconsider j = (len L) - k as Element of NAT by INT_1:3; A10: (1 + 1) + (- 1) <= j + (- 1) by A9, XREAL_1:6; then reconsider j1 = j - 1 as Element of NAT by INT_1:3; len L <= (len L) + k by NAT_1:11; then (len L) + (- k) <= ((len L) + k) + (- k) by XREAL_1:6; then A11: j - 1 < len L by XREAL_1:146, XXREAL_0:2; j1 + 1 = j ; then consider G1, H1 being Element of QC-WFF Al such that A12: L . j1 = G1 and A13: ( L . j = H1 & G1 is_immediate_constituent_of H1 ) by A2, A10, A11, Def5; reconsider r = G1 as Element of CQC-WFF Al by A2, A10, A11, A12, Th28; k < k + 1 by NAT_1:13; then consider q being Element of CQC-WFF Al such that A14: q = L . j and A15: QuantNbr q <= n by A7, A8, XXREAL_0:2; A16: now__::_thesis:_(_ex_x_being_bound_QC-variable_of_Al_st_q_=_All_(x,G1)_implies_ex_r,_r_being_Element_of_CQC-WFF_Al_st_ (_r_=_L_._((len_L)_-_(k_+_1))_&_QuantNbr_r_<=_n_)_) given x being bound_QC-variable of Al such that A17: q = All (x,G1) ; ::_thesis: ex r, r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) take r = r; ::_thesis: ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) (QuantNbr r) + 1 <= n by A15, A17, CQC_SIM1:18; then QuantNbr r <= n by NAT_1:13; hence ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; ::_thesis: verum end; A18: now__::_thesis:_(_ex_F_being_Element_of_QC-WFF_Al_st_q_=_F_'&'_G1_implies_ex_r,_r_being_Element_of_CQC-WFF_Al_st_ (_r_=_L_._((len_L)_-_(k_+_1))_&_QuantNbr_r_<=_n_)_) given F being Element of QC-WFF Al such that A19: q = F '&' G1 ; ::_thesis: ex r, r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) reconsider F = F as Element of CQC-WFF Al by A19, CQC_LANG:9; take r = r; ::_thesis: ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) n <= n + (QuantNbr F) by NAT_1:11; then A20: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6; (QuantNbr r) + (QuantNbr F) <= n by A15, A19, CQC_SIM1:17; then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6; hence ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A20, XXREAL_0:2; ::_thesis: verum end; A21: now__::_thesis:_(_ex_F_being_Element_of_QC-WFF_Al_st_q_=_G1_'&'_F_implies_ex_r,_r_being_Element_of_CQC-WFF_Al_st_ (_r_=_L_._((len_L)_-_(k_+_1))_&_QuantNbr_r_<=_n_)_) given F being Element of QC-WFF Al such that A22: q = G1 '&' F ; ::_thesis: ex r, r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) reconsider F = F as Element of CQC-WFF Al by A22, CQC_LANG:9; take r = r; ::_thesis: ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) n <= n + (QuantNbr F) by NAT_1:11; then A23: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6; (QuantNbr r) + (QuantNbr F) <= n by A15, A22, CQC_SIM1:17; then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6; hence ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A23, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_(_q_=_'not'_G1_implies_ex_r,_r_being_Element_of_CQC-WFF_Al_st_ (_r_=_L_._((len_L)_-_(k_+_1))_&_QuantNbr_r_<=_n_)_) assume A24: q = 'not' G1 ; ::_thesis: ex r, r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) take r = r; ::_thesis: ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) QuantNbr r <= n by A15, A24, CQC_SIM1:16; hence ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; ::_thesis: verum end; hence ex r being Element of CQC-WFF Al st ( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A14, A13, A21, A18, A16, QC_LANG2:def_19; ::_thesis: verum end; L . (len L) = p by A2, Def5; then A25: S1[ 0 ] by A1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A25, A6); then ex r being Element of CQC-WFF Al st ( r = L . ((len L) - l) & QuantNbr r <= n ) by A5; hence ex r being Element of CQC-WFF Al st ( r = L . i & QuantNbr r <= n ) ; ::_thesis: verum end; theorem :: SUBSTUT2:30 for Al being QC-alphabet for n being Element of NAT for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds QuantNbr q <= n proof let Al be QC-alphabet ; ::_thesis: for n being Element of NAT for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds QuantNbr q <= n let n be Element of NAT ; ::_thesis: for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds QuantNbr q <= n let p, q be Element of CQC-WFF Al; ::_thesis: ( QuantNbr p = n & q is_subformula_of p implies QuantNbr q <= n ) set L = the PATH of q,p; set m = len the PATH of q,p; assume that A1: QuantNbr p = n and A2: q is_subformula_of p ; ::_thesis: QuantNbr q <= n 1 <= len the PATH of q,p by A2, Def5; then ex r being Element of CQC-WFF Al st ( r = the PATH of q,p . 1 & QuantNbr r <= n ) by A1, A2, Th29; hence QuantNbr q <= n by A2, Def5; ::_thesis: verum end; theorem :: SUBSTUT2:31 for Al being QC-alphabet for n being Element of NAT for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q = n ) holds n = 0 proof let Al be QC-alphabet ; ::_thesis: for n being Element of NAT for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q = n ) holds n = 0 let n be Element of NAT ; ::_thesis: for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q = n ) holds n = 0 let p be Element of CQC-WFF Al; ::_thesis: ( ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q = n ) implies n = 0 ) assume A1: for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q = n ; ::_thesis: n = 0 defpred S1[ Element of CQC-WFF Al] means ( $1 is_subformula_of p implies QuantNbr $1 = 0 ); A2: for x being bound_QC-variable of Al for r being Element of CQC-WFF Al st S1[r] holds S1[ All (x,r)] proof let x be bound_QC-variable of Al; ::_thesis: for r being Element of CQC-WFF Al st S1[r] holds S1[ All (x,r)] let r be Element of CQC-WFF Al; ::_thesis: ( S1[r] implies S1[ All (x,r)] ) assume S1[r] ; ::_thesis: S1[ All (x,r)] now__::_thesis:_not_All_(x,r)_is_subformula_of_p assume A3: All (x,r) is_subformula_of p ; ::_thesis: contradiction r is_immediate_constituent_of All (x,r) by QC_LANG2:46; then r is_proper_subformula_of p by A3, QC_LANG2:63; then r is_subformula_of p by QC_LANG2:def_21; then A4: QuantNbr r = n by A1; QuantNbr (All (x,r)) = n by A1, A3; then n + (- n) = (1 + n) + (- n) by A4, CQC_SIM1:18; hence contradiction ; ::_thesis: verum end; hence S1[ All (x,r)] ; ::_thesis: verum end; A5: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds S1[r '&' s] proof let r, s be Element of CQC-WFF Al; ::_thesis: ( S1[r] & S1[s] implies S1[r '&' s] ) assume A6: ( S1[r] & S1[s] ) ; ::_thesis: S1[r '&' s] assume A7: r '&' s is_subformula_of p ; ::_thesis: QuantNbr (r '&' s) = 0 s is_immediate_constituent_of r '&' s by QC_LANG2:45; then A8: s is_proper_subformula_of p by A7, QC_LANG2:63; r is_immediate_constituent_of r '&' s by QC_LANG2:45; then r is_proper_subformula_of p by A7, QC_LANG2:63; then QuantNbr (r '&' s) = 0 + 0 by A6, A8, CQC_SIM1:17, QC_LANG2:def_21; hence QuantNbr (r '&' s) = 0 ; ::_thesis: verum end; for r being Element of CQC-WFF Al st S1[r] holds S1[ 'not' r] proof let r be Element of CQC-WFF Al; ::_thesis: ( S1[r] implies S1[ 'not' r] ) assume A9: S1[r] ; ::_thesis: S1[ 'not' r] A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43; assume 'not' r is_subformula_of p ; ::_thesis: QuantNbr ('not' r) = 0 then r is_proper_subformula_of p by A10, QC_LANG2:63; hence QuantNbr ('not' r) = 0 by A9, CQC_SIM1:16, QC_LANG2:def_21; ::_thesis: verum end; then A11: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A5, A2, CQC_SIM1:14, CQC_SIM1:15; A12: for r being Element of CQC-WFF Al holds S1[r] from CQC_LANG:sch_1(A11); QuantNbr p = n by A1; hence n = 0 by A12; ::_thesis: verum end; theorem :: SUBSTUT2:32 for Al being QC-alphabet for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds for x being bound_QC-variable of Al for r being Element of CQC-WFF Al holds q <> All (x,r) ) holds QuantNbr p = 0 proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds for x being bound_QC-variable of Al for r being Element of CQC-WFF Al holds q <> All (x,r) ) holds QuantNbr p = 0 let p be Element of CQC-WFF Al; ::_thesis: ( ( for q being Element of CQC-WFF Al st q is_subformula_of p holds for x being bound_QC-variable of Al for r being Element of CQC-WFF Al holds q <> All (x,r) ) implies QuantNbr p = 0 ) assume A1: for q being Element of CQC-WFF Al st q is_subformula_of p holds for x being bound_QC-variable of Al for r being Element of CQC-WFF Al holds q <> All (x,r) ; ::_thesis: QuantNbr p = 0 defpred S1[ Element of CQC-WFF Al] means ( $1 is_subformula_of p implies QuantNbr $1 = 0 ); A2: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds S1[r '&' s] proof let r, s be Element of CQC-WFF Al; ::_thesis: ( S1[r] & S1[s] implies S1[r '&' s] ) assume A3: ( S1[r] & S1[s] ) ; ::_thesis: S1[r '&' s] assume A4: r '&' s is_subformula_of p ; ::_thesis: QuantNbr (r '&' s) = 0 s is_immediate_constituent_of r '&' s by QC_LANG2:45; then A5: s is_proper_subformula_of p by A4, QC_LANG2:63; r is_immediate_constituent_of r '&' s by QC_LANG2:45; then r is_proper_subformula_of p by A4, QC_LANG2:63; then QuantNbr (r '&' s) = 0 + 0 by A3, A5, CQC_SIM1:17, QC_LANG2:def_21; hence QuantNbr (r '&' s) = 0 ; ::_thesis: verum end; for r being Element of CQC-WFF Al st S1[r] holds S1[ 'not' r] proof let r be Element of CQC-WFF Al; ::_thesis: ( S1[r] implies S1[ 'not' r] ) assume A6: S1[r] ; ::_thesis: S1[ 'not' r] A7: r is_immediate_constituent_of 'not' r by QC_LANG2:43; assume 'not' r is_subformula_of p ; ::_thesis: QuantNbr ('not' r) = 0 then r is_proper_subformula_of p by A7, QC_LANG2:63; hence QuantNbr ('not' r) = 0 by A6, CQC_SIM1:16, QC_LANG2:def_21; ::_thesis: verum end; then A8: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A1, A2, CQC_SIM1:14, CQC_SIM1:15; for r being Element of CQC-WFF Al holds S1[r] from CQC_LANG:sch_1(A8); hence QuantNbr p = 0 ; ::_thesis: verum end; theorem Th33: :: SUBSTUT2:33 for Al being QC-alphabet for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q <> 1 ) holds QuantNbr p = 0 proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al st ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q <> 1 ) holds QuantNbr p = 0 let p be Element of CQC-WFF Al; ::_thesis: ( ( for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q <> 1 ) implies QuantNbr p = 0 ) assume A1: for q being Element of CQC-WFF Al st q is_subformula_of p holds QuantNbr q <> 1 ; ::_thesis: QuantNbr p = 0 defpred S1[ Element of CQC-WFF Al] means ( $1 is_subformula_of p implies QuantNbr $1 = 0 ); A2: for x being bound_QC-variable of Al for r being Element of CQC-WFF Al st S1[r] holds S1[ All (x,r)] proof let x be bound_QC-variable of Al; ::_thesis: for r being Element of CQC-WFF Al st S1[r] holds S1[ All (x,r)] let r be Element of CQC-WFF Al; ::_thesis: ( S1[r] implies S1[ All (x,r)] ) assume A3: S1[r] ; ::_thesis: S1[ All (x,r)] now__::_thesis:_not_All_(x,r)_is_subformula_of_p assume A4: All (x,r) is_subformula_of p ; ::_thesis: contradiction r is_immediate_constituent_of All (x,r) by QC_LANG2:46; then r is_proper_subformula_of p by A4, QC_LANG2:63; then QuantNbr (All (x,r)) = 0 + 1 by A3, CQC_SIM1:18, QC_LANG2:def_21; hence contradiction by A1, A4; ::_thesis: verum end; hence S1[ All (x,r)] ; ::_thesis: verum end; A5: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds S1[r '&' s] proof let r, s be Element of CQC-WFF Al; ::_thesis: ( S1[r] & S1[s] implies S1[r '&' s] ) assume A6: ( S1[r] & S1[s] ) ; ::_thesis: S1[r '&' s] assume A7: r '&' s is_subformula_of p ; ::_thesis: QuantNbr (r '&' s) = 0 s is_immediate_constituent_of r '&' s by QC_LANG2:45; then A8: s is_proper_subformula_of p by A7, QC_LANG2:63; r is_immediate_constituent_of r '&' s by QC_LANG2:45; then r is_proper_subformula_of p by A7, QC_LANG2:63; then QuantNbr (r '&' s) = 0 + 0 by A6, A8, CQC_SIM1:17, QC_LANG2:def_21; hence QuantNbr (r '&' s) = 0 ; ::_thesis: verum end; for r being Element of CQC-WFF Al st S1[r] holds S1[ 'not' r] proof let r be Element of CQC-WFF Al; ::_thesis: ( S1[r] implies S1[ 'not' r] ) assume A9: S1[r] ; ::_thesis: S1[ 'not' r] A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43; assume 'not' r is_subformula_of p ; ::_thesis: QuantNbr ('not' r) = 0 then r is_proper_subformula_of p by A10, QC_LANG2:63; hence QuantNbr ('not' r) = 0 by A9, CQC_SIM1:16, QC_LANG2:def_21; ::_thesis: verum end; then A11: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A5, A2, CQC_SIM1:14, CQC_SIM1:15; for r being Element of CQC-WFF Al holds S1[r] from CQC_LANG:sch_1(A11); hence QuantNbr p = 0 ; ::_thesis: verum end; theorem :: SUBSTUT2:34 for Al being QC-alphabet for p being Element of CQC-WFF Al st 1 <= QuantNbr p holds ex q being Element of CQC-WFF Al st ( q is_subformula_of p & QuantNbr q = 1 ) by Th33;