scheme :: SUBSTUT1:sch 4
SubQCFuncUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Function of (QC-Sub-WFF F1()),F2(), F4() -> Function of (QC-Sub-WFF F1()),F2(), F5() -> Element of F2(), F6( set ) -> Element of F2(), F7( set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9( set , set , set ) -> Element of F2() } :
F3() = F4()
provided
A1: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F3() . S = F5() ) & ( S is Sub_atomic implies F3() . S = F6(S) ) & ( S is Sub_negative & d1 = F3() . (Sub_the_argument_of S) implies F3() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F3() . (Sub_the_left_argument_of S) & d2 = F3() . (Sub_the_right_argument_of S) implies F3() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F3() . (Sub_the_scope_of S) implies F3() . S = F9(F1(),S,d1) ) ) and
A2: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F4() . S = F5() ) & ( S is Sub_atomic implies F4() . S = F6(S) ) & ( S is Sub_negative & d1 = F4() . (Sub_the_argument_of S) implies F4() . S = F7(d1) ) & ( S is Sub_conjunctive & d1 = F4() . (Sub_the_left_argument_of S) & d2 = F4() . (Sub_the_right_argument_of S) implies F4() . S = F8(d1,d2) ) & ( S is Sub_universal & d1 = F4() . (Sub_the_scope_of S) implies F4() . S = F9(F1(),S,d1) ) )