begin
Lm1:
for A being QC-alphabet
for x being bound_QC-variable of A holds not x in fixed_QC-variables A
scheme
CQCFuncEx{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4(
set ,
set ,
set )
-> Element of
F2(),
F5(
set )
-> Element of
F2(),
F6(
set ,
set )
-> Element of
F2(),
F7(
set ,
set )
-> Element of
F2() } :
scheme
CQCFuncUniq{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Function of
(CQC-WFF F1()),
F2(),
F4()
-> Function of
(CQC-WFF F1()),
F2(),
F5()
-> Element of
F2(),
F6(
set ,
set ,
set )
-> Element of
F2(),
F7(
set )
-> Element of
F2(),
F8(
set ,
set )
-> Element of
F2(),
F9(
set ,
set )
-> Element of
F2() } :
provided
A1:
(
F3()
. (VERUM F1()) = F5() & ( 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
(
F3()
. (P ! l) = F6(
k,
P,
l) &
F3()
. ('not' r) = F7(
(F3() . r)) &
F3()
. (r '&' s) = F8(
(F3() . r),
(F3() . s)) &
F3()
. (All (x,r)) = F9(
x,
(F3() . r)) ) ) )
and A2:
(
F4()
. (VERUM F1()) = F5() & ( 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
(
F4()
. (P ! l) = F6(
k,
P,
l) &
F4()
. ('not' r) = F7(
(F4() . r)) &
F4()
. (r '&' s) = F8(
(F4() . r),
(F4() . s)) &
F4()
. (All (x,r)) = F9(
x,
(F4() . r)) ) ) )
scheme
CQCDefcorrectness{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
CQC-WFF F1(),
F4()
-> Element of
F2(),
F5(
set ,
set ,
set )
-> Element of
F2(),
F6(
set )
-> Element of
F2(),
F7(
set ,
set )
-> Element of
F2(),
F8(
set ,
set )
-> Element of
F2() } :
( ex
d being
Element of
F2() ex
F being
Function of
(CQC-WFF F1()),
F2() st
(
d = F . F3() &
F . (VERUM F1()) = F4() & ( 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
(
F . (P ! l) = F5(
k,
P,
l) &
F . ('not' r) = F6(
(F . r)) &
F . (r '&' s) = F7(
(F . r),
(F . s)) &
F . (All (x,r)) = F8(
x,
(F . r)) ) ) ) & ( for
d1,
d2 being
Element of
F2() st ex
F being
Function of
(CQC-WFF F1()),
F2() st
(
d1 = F . F3() &
F . (VERUM F1()) = F4() & ( 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
(
F . (P ! l) = F5(
k,
P,
l) &
F . ('not' r) = F6(
(F . r)) &
F . (r '&' s) = F7(
(F . r),
(F . s)) &
F . (All (x,r)) = F8(
x,
(F . r)) ) ) ) & ex
F being
Function of
(CQC-WFF F1()),
F2() st
(
d2 = F . F3() &
F . (VERUM F1()) = F4() & ( 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
(
F . (P ! l) = F5(
k,
P,
l) &
F . ('not' r) = F6(
(F . r)) &
F . (r '&' s) = F7(
(F . r),
(F . s)) &
F . (All (x,r)) = F8(
x,
(F . r)) ) ) ) holds
d1 = d2 ) )
scheme
CQCDefVERUM{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3(
set )
-> Element of
F2(),
F4()
-> Element of
F2(),
F5(
set ,
set ,
set )
-> Element of
F2(),
F6(
set )
-> Element of
F2(),
F7(
set ,
set )
-> Element of
F2(),
F8(
set ,
set )
-> Element of
F2() } :
provided
scheme
CQCDefatomic{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3()
-> Element of
F2(),
F4(
set )
-> Element of
F2(),
F5(
set ,
set ,
set )
-> Element of
F2(),
F6()
-> Element of
NAT ,
F7()
-> QC-pred_symbol of
F6(),
F1(),
F8()
-> CQC-variable_list of
F6(),
F1(),
F9(
set )
-> Element of
F2(),
F10(
set ,
set )
-> Element of
F2(),
F11(
set ,
set )
-> Element of
F2() } :
F4(
(F7() ! F8()))
= F5(
F6(),
F7(),
F8())
provided
scheme
CQCDefnegative{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3(
set )
-> Element of
F2(),
F4()
-> Element of
F2(),
F5(
set ,
set ,
set )
-> Element of
F2(),
F6(
set )
-> Element of
F2(),
F7()
-> Element of
CQC-WFF F1(),
F8(
set ,
set )
-> Element of
F2(),
F9(
set ,
set )
-> Element of
F2() } :
F3(
('not' F7()))
= F6(
F3(
F7()))
provided
scheme
QCDefconjunctive{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3(
set )
-> Element of
F2(),
F4()
-> Element of
F2(),
F5(
set ,
set ,
set )
-> Element of
F2(),
F6(
set )
-> Element of
F2(),
F7(
set ,
set )
-> Element of
F2(),
F8()
-> Element of
CQC-WFF F1(),
F9()
-> Element of
CQC-WFF F1(),
F10(
set ,
set )
-> Element of
F2() } :
F3(
(F8() '&' F9()))
= F7(
F3(
F8()),
F3(
F9()))
provided
scheme
QCDefuniversal{
F1()
-> QC-alphabet ,
F2()
-> non
empty set ,
F3(
set )
-> Element of
F2(),
F4()
-> Element of
F2(),
F5(
set ,
set ,
set )
-> Element of
F2(),
F6(
set )
-> Element of
F2(),
F7(
set ,
set )
-> Element of
F2(),
F8(
set ,
set )
-> Element of
F2(),
F9()
-> bound_QC-variable of
F1(),
F10()
-> Element of
CQC-WFF F1() } :
F3(
(All (F9(),F10())))
= F8(
F9(),
F3(
F10()))
provided
Lm2:
for A being QC-alphabet
for x being bound_QC-variable of A
for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds
( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) ) ) & ( for q being Element of QC-WFF A holds
( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) ) holds
F1 = F2
definition
let A be
QC-alphabet ;
let p be
Element of
QC-WFF A;
let x be
bound_QC-variable of
A;
existence
ex b1 being Element of QC-WFF A ex F being Function of (QC-WFF A),(QC-WFF A) st
( b1 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) )
uniqueness
for b1, b2 being Element of QC-WFF A st ex F being Function of (QC-WFF A),(QC-WFF A) st
( b1 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) & ex F being Function of (QC-WFF A),(QC-WFF A) st
( b2 = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) holds
b1 = b2
by Lm2;
end;
Lm3:
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A st p is universal holds
p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x))))
begin