:: 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;