scheme :: CQC_SIM1:sch 2
CQCF2FuncEx{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> non empty set , F4() -> Element of Funcs (F2(),F3()), F5( object , object , object ) -> Element of Funcs (F2(),F3()), F6( object , object ) -> Element of Funcs (F2(),F3()), F7( object , object , object , object ) -> Element of Funcs (F2(),F3()), F8( object , object , object ) -> Element of Funcs (F2(),F3()) } :
ex F being Function of (CQC-WFF F1()),(Funcs (F2(),F3())) st
( F . (VERUM F1()) = F4() & ( for k being 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) ) ) )