deffunc H_{1}( set , Element of QC-WFF F_{1}()) -> Element of Funcs (F_{2}(),F_{3}()) = F_{8}((bound_in $2),$1,(the_scope_of $2));

deffunc H_{2}( set , set , Element of QC-WFF F_{1}()) -> Element of Funcs (F_{2}(),F_{3}()) = F_{7}($1,$2,(the_left_argument_of $3),(the_right_argument_of $3));

deffunc H_{3}( set , Element of QC-WFF F_{1}()) -> Element of Funcs (F_{2}(),F_{3}()) = F_{6}($1,(the_argument_of $2));

deffunc H_{4}( Element of QC-WFF F_{1}()) -> Element of Funcs (F_{2}(),F_{3}()) = F_{5}((the_arity_of (the_pred_symbol_of $1)),(the_pred_symbol_of $1),(the_arguments_of $1));

consider F being Function of (QC-WFF F_{1}()),(Funcs (F_{2}(),F_{3}())) such that

A1: ( F . (VERUM F_{1}()) = F_{4}() & ( for p being Element of QC-WFF F_{1}() holds

( ( p is atomic implies F . p = H_{4}(p) ) & ( p is negative implies F . p = H_{3}(F . (the_argument_of p),p) ) & ( p is conjunctive implies F . p = H_{2}(F . (the_left_argument_of p),F . (the_right_argument_of p),p) ) & ( p is universal implies F . p = H_{1}(F . (the_scope_of p),p) ) ) ) )
from CQC_SIM1:sch 1();

reconsider G = F | (CQC-WFF F_{1}()) as Function of (CQC-WFF F_{1}()),(Funcs (F_{2}(),F_{3}())) by FUNCT_2:32;

take G ; :: thesis: ( G . (VERUM F_{1}()) = F_{4}() & ( for k being Nat

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds G . (P ! l) = F_{5}(k,P,l) ) & ( for r, s being Element of CQC-WFF F_{1}()

for x being Element of bound_QC-variables F_{1}() holds

( G . ('not' r) = F_{6}((G . r),r) & G . (r '&' s) = F_{7}((G . r),(G . s),r,s) & G . (All (x,r)) = F_{8}(x,(G . r),r) ) ) )

thus G . (VERUM F_{1}()) = F_{4}()
by A1, FUNCT_1:49; :: thesis: ( ( for k being Nat

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds G . (P ! l) = F_{5}(k,P,l) ) & ( for r, s being Element of CQC-WFF F_{1}()

for x being Element of bound_QC-variables F_{1}() holds

( G . ('not' r) = F_{6}((G . r),r) & G . (r '&' s) = F_{7}((G . r),(G . s),r,s) & G . (All (x,r)) = F_{8}(x,(G . r),r) ) ) )

thus for k being Nat

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds G . (P ! l) = F_{5}(k,P,l)
:: thesis: for r, s being Element of CQC-WFF F_{1}()

for x being Element of bound_QC-variables F_{1}() holds

( G . ('not' r) = F_{6}((G . r),r) & G . (r '&' s) = F_{7}((G . r),(G . s),r,s) & G . (All (x,r)) = F_{8}(x,(G . r),r) )_{1}(); :: thesis: for x being Element of bound_QC-variables F_{1}() holds

( G . ('not' r) = F_{6}((G . r),r) & G . (r '&' s) = F_{7}((G . r),(G . s),r,s) & G . (All (x,r)) = F_{8}(x,(G . r),r) )

let x be Element of bound_QC-variables F_{1}(); :: thesis: ( G . ('not' r) = F_{6}((G . r),r) & G . (r '&' s) = F_{7}((G . r),(G . s),r,s) & G . (All (x,r)) = F_{8}(x,(G . r),r) )

set r9 = G . r;

set s9 = G . s;

A6: G . r = F . r by FUNCT_1:49;

A7: 'not' r is negative by QC_LANG1:def 19;

then A8: the_argument_of ('not' r) = r by QC_LANG1:def 24;

thus G . ('not' r) = F . ('not' r) by FUNCT_1:49

.= F_{6}((G . r),r)
by A1, A6, A7, A8
; :: thesis: ( G . (r '&' s) = F_{7}((G . r),(G . s),r,s) & G . (All (x,r)) = F_{8}(x,(G . r),r) )

A9: G . s = F . s by FUNCT_1:49;

A10: r '&' s is conjunctive by QC_LANG1:def 20;

then A11: the_left_argument_of (r '&' s) = r by QC_LANG1:def 25;

A12: the_right_argument_of (r '&' s) = s by A10, QC_LANG1:def 26;

thus G . (r '&' s) = F . (r '&' s) by FUNCT_1:49

.= F_{7}((G . r),(G . s),r,s)
by A1, A6, A9, A10, A11, A12
; :: thesis: G . (All (x,r)) = F_{8}(x,(G . r),r)

A13: All (x,r) is universal by QC_LANG1:def 21;

then A14: bound_in (All (x,r)) = x by QC_LANG1:def 27;

A15: the_scope_of (All (x,r)) = r by A13, QC_LANG1:def 28;

thus G . (All (x,r)) = F . (All (x,r)) by FUNCT_1:49

.= F_{8}(x,(G . r),r)
by A1, A6, A13, A14, A15
; :: thesis: verum

deffunc H

deffunc H

deffunc H

consider F being Function of (QC-WFF F

A1: ( F . (VERUM F

( ( p is atomic implies F . p = H

reconsider G = F | (CQC-WFF F

take G ; :: thesis: ( G . (VERUM F

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

for x being Element of bound_QC-variables F

( G . ('not' r) = F

thus G . (VERUM F

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

for x being Element of bound_QC-variables F

( G . ('not' r) = F

thus for k being Nat

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

for x being Element of bound_QC-variables F

( G . ('not' r) = F

proof

let r, s be Element of CQC-WFF F
let k be Nat; :: thesis: for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds G . (P ! l) = F_{5}(k,P,l)

let l be CQC-variable_list of k,F_{1}(); :: thesis: for P being QC-pred_symbol of k,F_{1}() holds G . (P ! l) = F_{5}(k,P,l)

let P be QC-pred_symbol of k,F_{1}(); :: thesis: G . (P ! l) = F_{5}(k,P,l)

A2: the_arity_of P = k by QC_LANG1:11;

A3: P ! l is atomic by QC_LANG1:def 18;

then A4: the_arguments_of (P ! l) = l by QC_LANG1:def 23;

A5: the_pred_symbol_of (P ! l) = P by A3, QC_LANG1:def 22;

thus G . (P ! l) = F . (P ! l) by FUNCT_1:49

.= F_{5}(k,P,l)
by A1, A3, A4, A5, A2
; :: thesis: verum

end;for P being QC-pred_symbol of k,F

let l be CQC-variable_list of k,F

let P be QC-pred_symbol of k,F

A2: the_arity_of P = k by QC_LANG1:11;

A3: P ! l is atomic by QC_LANG1:def 18;

then A4: the_arguments_of (P ! l) = l by QC_LANG1:def 23;

A5: the_pred_symbol_of (P ! l) = P by A3, QC_LANG1:def 22;

thus G . (P ! l) = F . (P ! l) by FUNCT_1:49

.= F

( G . ('not' r) = F

let x be Element of bound_QC-variables F

set r9 = G . r;

set s9 = G . s;

A6: G . r = F . r by FUNCT_1:49;

A7: 'not' r is negative by QC_LANG1:def 19;

then A8: the_argument_of ('not' r) = r by QC_LANG1:def 24;

thus G . ('not' r) = F . ('not' r) by FUNCT_1:49

.= F

A9: G . s = F . s by FUNCT_1:49;

A10: r '&' s is conjunctive by QC_LANG1:def 20;

then A11: the_left_argument_of (r '&' s) = r by QC_LANG1:def 25;

A12: the_right_argument_of (r '&' s) = s by A10, QC_LANG1:def 26;

thus G . (r '&' s) = F . (r '&' s) by FUNCT_1:49

.= F

A13: All (x,r) is universal by QC_LANG1:def 21;

then A14: bound_in (All (x,r)) = x by QC_LANG1:def 27;

A15: the_scope_of (All (x,r)) = r by A13, QC_LANG1:def 28;

thus G . (All (x,r)) = F . (All (x,r)) by FUNCT_1:49

.= F