deffunc H₅( Element of NAT , QC-pred_symbol of $1, CQC-variable_list of $1) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = ATOMIC ($2,$3);
set D = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):];
deffunc H₆( Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, set ) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = NEGATIVE $1;
deffunc H₇( Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, Element of CQC-WFF , set ) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = CON ($1,$2,(QuantNbr $3));
deffunc H₈( Element of bound_QC-variables , Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF, set ) -> Element of Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF) = UNIVERSAL ($1,$2);
reconsider V = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM as Function of [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF ;
let F, G be Function of CQC-WFF,(Funcs ([:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):],CQC-WFF)); :: thesis: ( F . VERUM = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds F . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = NEGATIVE (F . r) & F . (r '&' s) = CON ((F . r),(F . s),(QuantNbr r)) & F . (All (x,r)) = UNIVERSAL (x,(F . r)) ) ) & G . VERUM = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds G . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( G . ('not' r) = NEGATIVE (G . r) & G . (r '&' s) = CON ((G . r),(G . s),(QuantNbr r)) & G . (All (x,r)) = UNIVERSAL (x,(G . r)) ) ) implies F = G )
assume that
A4: F . VERUM = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM and
A5: for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds F . (P ! ll) = H₅(k,P,ll) and
A6: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = H₆(F . r,r) & F . (r '&' s) = H₇(F . r,F . s,r,s) & F . (All (x,r)) = H₈(x,F . r,r) ) and
A7: G . VERUM = [:NAT,(Funcs (bound_QC-variables,bound_QC-variables)):] --> VERUM and
A8: for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds G . (P ! ll) = H₅(k,P,ll) and
A9: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( G . ('not' r) = H₆(G . r,r) & G . (r '&' s) = H₇(G . r,G . s,r,s) & G . (All (x,r)) = H₈(x,G . r,r) ) ; :: thesis: F = G
A10: G . VERUM = V by A7;
A11: F . VERUM = V by A4;
thus F = G from CQC_SIM1:sch 3(A11, A5, A6, A10, A8, A9); :: thesis: verum