scheme :: QC_LANG3:sch 7
QCDResult9universal{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> QC-formula of F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1()) -> Element of F2() } :
F9(F4()) = F8(F4(),F9((the_scope_of F4())))
provided
A1: for p being QC-formula of F1()
for d being Element of F2() holds
( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st
( d = F . p & ( for p being Element of QC-WFF F1()
for d1, d2 being Element of F2() holds
( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and
A2: F4() is universal