scheme :: CQC_SIM1:sch 1
QCFuncExN{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( object ) -> Element of F2(), F5( object , object ) -> Element of F2(), F6( object , object , object ) -> Element of F2(), F7( object , object ) -> Element of F2() } :
ex F being Function of (QC-WFF F1()),F2() st
( F . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F7((F . (the_scope_of p)),p) ) ) ) )