begin
scheme
QCFuncExN{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4(
set )
-> Element of
F2(),
F5(
set ,
set )
-> Element of
F2(),
F6(
set ,
set ,
set )
-> Element of
F2(),
F7(
set ,
set )
-> Element of
F2() } :
scheme
CQCF2FuncEx{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> non
empty set ,
F4()
-> Element of
Funcs (
F2(),
F3()),
F5(
set ,
set ,
set )
-> Element of
Funcs (
F2(),
F3()),
F6(
set ,
set )
-> Element of
Funcs (
F2(),
F3()),
F7(
set ,
set ,
set ,
set )
-> Element of
Funcs (
F2(),
F3()),
F8(
set ,
set ,
set )
-> Element of
Funcs (
F2(),
F3()) } :
ex
F being
Function of
(CQC-WFF F1()),
(Funcs (F2(),F3())) st
(
F . (VERUM F1()) = F4() & ( 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
F . (P ! l) = F5(
k,
P,
l) ) & ( for
r,
s being
Element of
CQC-WFF F1()
for
x being
Element of
bound_QC-variables F1() holds
(
F . ('not' r) = F6(
(F . r),
r) &
F . (r '&' s) = F7(
(F . r),
(F . s),
r,
s) &
F . (All (x,r)) = F8(
x,
(F . r),
r) ) ) )
scheme
CQCF2FUniq{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> non
empty set ,
F4()
-> Function of
(CQC-WFF F1()),
(Funcs (F2(),F3())),
F5()
-> Function of
(CQC-WFF F1()),
(Funcs (F2(),F3())),
F6()
-> Function of
F2(),
F3(),
F7(
set ,
set ,
set )
-> Function of
F2(),
F3(),
F8(
set ,
set )
-> Function of
F2(),
F3(),
F9(
set ,
set ,
set ,
set )
-> Function of
F2(),
F3(),
F10(
set ,
set ,
set )
-> Function of
F2(),
F3() } :
provided
A1:
F4()
. (VERUM F1()) = F6()
and A2:
for
k being
Element of
NAT for
ll being
CQC-variable_list of
k,
F1()
for
P being
QC-pred_symbol of
k,
F1() holds
F4()
. (P ! ll) = F7(
k,
P,
ll)
and A3:
for
r,
s being
Element of
CQC-WFF F1()
for
x being
Element of
bound_QC-variables F1() holds
(
F4()
. ('not' r) = F8(
(F4() . r),
r) &
F4()
. (r '&' s) = F9(
(F4() . r),
(F4() . s),
r,
s) &
F4()
. (All (x,r)) = F10(
x,
(F4() . r),
r) )
and A4:
F5()
. (VERUM F1()) = F6()
and A5:
for
k being
Element of
NAT for
ll being
CQC-variable_list of
k,
F1()
for
P being
QC-pred_symbol of
k,
F1() holds
F5()
. (P ! ll) = F7(
k,
P,
ll)
and A6:
for
r,
s being
Element of
CQC-WFF F1()
for
x being
Element of
bound_QC-variables F1() holds
(
F5()
. ('not' r) = F8(
(F5() . r),
r) &
F5()
. (r '&' s) = F9(
(F5() . r),
(F5() . s),
r,
s) &
F5()
. (All (x,r)) = F10(
x,
(F5() . r),
r) )
definition
let A be
QC-alphabet ;
let f,
g be
Function of
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],
(CQC-WFF A);
let n be
Element of
NAT ;
func CON (
f,
g,
n)
-> Element of
Funcs (
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],
(CQC-WFF A))
means :
Def3:
for
t being
QC-symbol of
A for
h being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A))
for
p,
q being
Element of
CQC-WFF A st
p = f . (
t,
h) &
q = g . (
(t + n),
h) holds
it . (
t,
h)
= p '&' q;
existence
ex b1 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st
for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
b1 . (t,h) = p '&' q
uniqueness
for b1, b2 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
b1 . (t,h) = p '&' q ) & ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
b2 . (t,h) = p '&' q ) holds
b1 = b2
end;
::
deftheorem Def3 defines
CON CQC_SIM1:def 3 :
for A being QC-alphabet
for f, g being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)
for n being Element of NAT
for b5 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b5 = CON (f,g,n) iff for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds
b5 . (t,h) = p '&' q );
Lm1:
for A being QC-alphabet
for t being QC-symbol of A
for x being Element of bound_QC-variables A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds h +* (x .--> (x. t)) is Function of (bound_QC-variables A),(bound_QC-variables A)
definition
let A be
QC-alphabet ;
let f be
Function of
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],
(CQC-WFF A);
let x be
bound_QC-variable of
A;
existence
ex b1 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st
for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
b1 . (t,h) = All ((x. t),p)
uniqueness
for b1, b2 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
b1 . (t,h) = All ((x. t),p) ) & ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
b2 . (t,h) = All ((x. t),p) ) holds
b1 = b2
end;
::
deftheorem Def4 defines
UNIVERSAL CQC_SIM1:def 4 :
for A being QC-alphabet
for f being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)
for x being bound_QC-variable of A
for b4 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b4 = UNIVERSAL (x,f) iff for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
b4 . (t,h) = All ((x. t),p) );
Lm2:
for A being QC-alphabet
for k being Element of NAT
for f being CQC-variable_list of k,A holds f is FinSequence of bound_QC-variables A
definition
let A be
QC-alphabet ;
let k be
Element of
NAT ;
let P be
QC-pred_symbol of
k,
A;
let l be
CQC-variable_list of
k,
A;
existence
ex b1 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st
for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b1 . (t,h) = P ! (h * l)
uniqueness
for b1, b2 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b1 . (t,h) = P ! (h * l) ) & ( for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b2 . (t,h) = P ! (h * l) ) holds
b1 = b2
end;
deffunc H1( set , set , set ) -> Element of NAT = 0 ;
deffunc H2( Element of NAT ) -> Element of NAT = $1;
deffunc H3( Element of NAT , Element of NAT ) -> Element of NAT = $1 + $2;
deffunc H4( set , Element of NAT ) -> Element of NAT = $2 + 1;
definition
let A be
QC-alphabet ;
let p be
Element of
CQC-WFF A;
correctness
existence
ex b1 being Element of NAT ex F being Function of (CQC-WFF A),NAT st
( b1 = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds
( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) );
uniqueness
for b1, b2 being Element of NAT st ex F being Function of (CQC-WFF A),NAT st
( b1 = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds
( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) & ex F being Function of (CQC-WFF A),NAT st
( b2 = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds
( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) holds
b1 = b2;
end;
definition
let A be
QC-alphabet ;
let f be
Function of
(CQC-WFF A),
(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)));
let x be
Element of
CQC-WFF A;
.redefine func f . x -> Element of
Funcs (
[:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],
(CQC-WFF A));
coherence
f . x is Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))
end;
definition
let A be
QC-alphabet ;
func SepFunc A -> Function of
(CQC-WFF A),
(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) means :
Def7:
(
it . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for
k being
Element of
NAT for
l being
CQC-variable_list of
k,
A for
P being
QC-pred_symbol of
k,
A holds
it . (P ! l) = ATOMIC (
P,
l) ) & ( for
r,
s being
Element of
CQC-WFF A for
x being
Element of
bound_QC-variables A holds
(
it . ('not' r) = NEGATIVE (it . r) &
it . (r '&' s) = CON (
(it . r),
(it . s),
(QuantNbr r)) &
it . (All (x,r)) = UNIVERSAL (
x,
(it . r)) ) ) );
existence
ex b1 being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st
( b1 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds b1 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( b1 . ('not' r) = NEGATIVE (b1 . r) & b1 . (r '&' s) = CON ((b1 . r),(b1 . s),(QuantNbr r)) & b1 . (All (x,r)) = UNIVERSAL (x,(b1 . r)) ) ) )
uniqueness
for b1, b2 being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st b1 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds b1 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( b1 . ('not' r) = NEGATIVE (b1 . r) & b1 . (r '&' s) = CON ((b1 . r),(b1 . s),(QuantNbr r)) & b1 . (All (x,r)) = UNIVERSAL (x,(b1 . r)) ) ) & b2 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds b2 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( b2 . ('not' r) = NEGATIVE (b2 . r) & b2 . (r '&' s) = CON ((b2 . r),(b2 . s),(QuantNbr r)) & b2 . (All (x,r)) = UNIVERSAL (x,(b2 . r)) ) ) holds
b1 = b2
end;
::
deftheorem Def7 defines
SepFunc CQC_SIM1:def 7 :
for A being QC-alphabet
for b2 being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) holds
( b2 = SepFunc A iff ( b2 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT
for l being CQC-variable_list of k,A
for P being QC-pred_symbol of k,A holds b2 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds
( b2 . ('not' r) = NEGATIVE (b2 . r) & b2 . (r '&' s) = CON ((b2 . r),(b2 . s),(QuantNbr r)) & b2 . (All (x,r)) = UNIVERSAL (x,(b2 . r)) ) ) ) );
scheme
MaxFinDomElem{
F1()
-> non
empty set ,
F2()
-> set ,
P1[
set ,
set ] } :
ex
x being
Element of
F1() st
(
x in F2() & ( for
y being
Element of
F1() st
y in F2() holds
P1[
x,
y] ) )
provided
A1:
(
F2() is
finite &
F2()
<> {} &
F2()
c= F1() )
and A2:
for
x,
y being
Element of
F1() holds
(
P1[
x,
y] or
P1[
y,
x] )
and A3:
for
x,
y,
z being
Element of
F1() st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
definition
let A be
QC-alphabet ;
let p be
Element of
CQC-WFF A;
let X be
Subset of
[:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):];
pred X is_Sep-closed_on p means :
Def12:
(
[p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for
q being
Element of
CQC-WFF A for
t being
QC-symbol of
A for
K being
Finite_Subset of
(bound_QC-variables A) for
f being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A)) st
[('not' q),t,K,f] in X holds
[q,t,K,f] in X ) & ( for
q,
r being
Element of
CQC-WFF A for
t being
QC-symbol of
A for
K being
Finite_Subset of
(bound_QC-variables A) for
f being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A)) st
[(q '&' r),t,K,f] in X holds
(
[q,t,K,f] in X &
[r,(t + (QuantNbr q)),K,f] in X ) ) & ( for
q being
Element of
CQC-WFF A for
x being
Element of
bound_QC-variables A for
t being
QC-symbol of
A for
K being
Finite_Subset of
(bound_QC-variables A) for
f being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A)) st
[(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) );
end;
::
deftheorem Def12 defines
is_Sep-closed_on CQC_SIM1:def 12 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for X being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds
( X is_Sep-closed_on p iff ( [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for q being Element of CQC-WFF A
for t being QC-symbol of A
for K being Finite_Subset of (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in X holds
[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF A
for t being QC-symbol of A
for K being Finite_Subset of (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds
( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF A
for x being Element of bound_QC-variables A
for t being QC-symbol of A
for K being Finite_Subset of (bound_QC-variables A)
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds
[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) ) );
definition
let A be
QC-alphabet ;
let p be
Element of
CQC-WFF A;
existence
ex b1 being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st
( b1 is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds
b1 c= D ) )
uniqueness
for b1, b2 being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st b1 is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds
b1 c= D ) & b2 is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds
b2 c= D ) holds
b1 = b2
end;
theorem Th32:
for
A being
QC-alphabet for
p,
q,
r being
Element of
CQC-WFF A for
t being
QC-symbol of
A for
K being
Finite_Subset of
(bound_QC-variables A) for
f being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A)) st
[(q '&' r),t,K,f] in SepQuadruples p holds
(
[q,t,K,f] in SepQuadruples p &
[r,(t + (QuantNbr q)),K,f] in SepQuadruples p )
theorem Th34:
for
A being
QC-alphabet for
t being
QC-symbol of
A for
q,
p being
Element of
CQC-WFF A for
f being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A))
for
K being
Finite_Subset of
(bound_QC-variables A) holds
( not
[q,t,K,f] in SepQuadruples p or
[q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or
[('not' q),t,K,f] in SepQuadruples p or ex
r being
Element of
CQC-WFF A st
[(q '&' r),t,K,f] in SepQuadruples p or ex
r being
Element of
CQC-WFF A ex
u being
QC-symbol of
A st
(
t = u + (QuantNbr r) &
[(r '&' q),u,K,f] in SepQuadruples p ) or ex
x being
Element of
bound_QC-variables A ex
u being
QC-symbol of
A ex
h being
Element of
Funcs (
(bound_QC-variables A),
(bound_QC-variables A)) st
(
u ++ = t &
h +* ({x} --> (x. u)) = f & (
[(All (x,q)),u,K,h] in SepQuadruples p or
[(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )
scheme
Sepregression{
F1()
-> QC-alphabet ,
F2()
-> Element of
CQC-WFF F1(),
P1[
set ,
set ,
set ,
set ] } :
provided
A1:
P1[
F2(),
index F2(),
{}. (bound_QC-variables F1()),
id (bound_QC-variables F1())]
and A2:
for
q being
Element of
CQC-WFF F1()
for
t being
QC-symbol of
F1()
for
K being
Finite_Subset of
(bound_QC-variables F1()) for
f being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1())) st
[('not' q),t,K,f] in SepQuadruples F2() &
P1[
'not' q,
t,
K,
f] holds
P1[
q,
t,
K,
f]
and A3:
for
q,
r being
Element of
CQC-WFF F1()
for
t being
QC-symbol of
F1()
for
K being
Finite_Subset of
(bound_QC-variables F1()) for
f being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1())) st
[(q '&' r),t,K,f] in SepQuadruples F2() &
P1[
q '&' r,
t,
K,
f] holds
(
P1[
q,
t,
K,
f] &
P1[
r,
t + (QuantNbr q),
K,
f] )
and A4:
for
q being
Element of
CQC-WFF F1()
for
x being
bound_QC-variable of
F1()
for
t being
QC-symbol of
F1()
for
K being
Finite_Subset of
(bound_QC-variables F1()) for
f being
Element of
Funcs (
(bound_QC-variables F1()),
(bound_QC-variables F1())) st
[(All (x,q)),t,K,f] in SepQuadruples F2() &
P1[
All (
x,
q),
t,
K,
f] holds
P1[
q,
t ++ ,
K \/ {x},
f +* (x .--> (x. t))]