scheme :: CQC_SIM1:sch 3
CQCF2FUniq{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> non empty set , F₄() -> Function of (CQC-WFF F₁()),(Funcs (F₂(),F₃())), F₅() -> Function of (CQC-WFF F₁()),(Funcs (F₂(),F₃())), F₆() -> Function of F₂(),F₃(), F₇( object , object , object ) -> Function of F₂(),F₃(), F₈( object , object ) -> Function of F₂(),F₃(), F₉( object , object , object , object ) -> Function of F₂(),F₃(), F₁₀( object , object , object ) -> Function of F₂(),F₃() } :

F₄() = F₅()

provided

A1: F₄() . (VERUM F₁()) = F₆() and
A2: for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds F₄() . (P ! ll) = F₇(k,P,ll) and
A3: for r, s being Element of CQC-WFF F₁()
for x being Element of bound_QC-variables F₁() holds
( F₄() . ('not' r) = F₈((F₄() . r),r) & F₄() . (r '&' s) = F₉((F₄() . r),(F₄() . s),r,s) & F₄() . (All (x,r)) = F₁₀(x,(F₄() . r),r) ) and
A4: F₅() . (VERUM F₁()) = F₆() and
A5: for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds F₅() . (P ! ll) = F₇(k,P,ll) and
A6: for r, s being Element of CQC-WFF F₁()
for x being Element of bound_QC-variables F₁() holds
( F₅() . ('not' r) = F₈((F₅() . r),r) & F₅() . (r '&' s) = F₉((F₅() . r),(F₅() . s),r,s) & F₅() . (All (x,r)) = F₁₀(x,(F₅() . r),r) )