deffunc H1( set , Element of QC-WFF F1()) -> Element of Funcs (F2(),F3()) = F8((bound_in $2),$1,(the_scope_of $2));
deffunc H2( set , set , Element of QC-WFF F1()) -> Element of Funcs (F2(),F3()) = F7($1,$2,(the_left_argument_of $3),(the_right_argument_of $3));
deffunc H3( set , Element of QC-WFF F1()) -> Element of Funcs (F2(),F3()) = F6($1,(the_argument_of $2));
deffunc H4( Element of QC-WFF F1()) -> Element of Funcs (F2(),F3()) = F5((the_arity_of (the_pred_symbol_of $1)),(the_pred_symbol_of $1),(the_arguments_of $1));
consider F being Function of (QC-WFF F1()),(Funcs (F2(),F3())) such that
A1: ( F . (VERUM F1()) = F4() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = H4(p) ) & ( p is negative implies F . p = H3(F . (the_argument_of p),p) ) & ( p is conjunctive implies F . p = H2(F . (the_left_argument_of p),F . (the_right_argument_of p),p) ) & ( p is universal implies F . p = H1(F . (the_scope_of p),p) ) ) ) ) from CQC_SIM1:sch 1();
 reconsider G = F | (CQC-WFF F1()) as Function of (CQC-WFF F1()),(Funcs (F2(),F3())) by FUNCT_2:32;
take G ; :: thesis: ( G . (VERUM F1()) = F4() & ( for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds G . (P ! l) = F5(k,P,l) ) & ( for r, s being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1() holds
( G . ('not' r) = F6((G . r),r) & G . (r '&' s) = F7((G . r),(G . s),r,s) & G . (All (x,r)) = F8(x,(G . r),r) ) ) )
thus G . (VERUM F1()) = F4() by A1, FUNCT_1:49; :: thesis: ( ( for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds G . (P ! l) = F5(k,P,l) ) & ( for r, s being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1() holds
( G . ('not' r) = F6((G . r),r) & G . (r '&' s) = F7((G . r),(G . s),r,s) & G . (All (x,r)) = F8(x,(G . r),r) ) ) )
thus for k being Nat
for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds G . (P ! l) = F5(k,P,l) :: thesis: for r, s being Element of CQC-WFF F1()
for x being Element of bound_QC-variables F1() holds
( G . ('not' r) = F6((G . r),r) & G . (r '&' s) = F7((G . r),(G . s),r,s) & G . (All (x,r)) = F8(x,(G . r),r) )
proof
let k be Nat; :: thesis: for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds G . (P ! l) = F5(k,P,l)
let l be CQC-variable_list of k,F1(); :: thesis: for P being QC-pred_symbol of k,F1() holds G . (P ! l) = F5(k,P,l)
let P be QC-pred_symbol of k,F1(); :: thesis: G . (P ! l) = F5(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
.= F5(k,P,l) by A1, A3, A4, A5, A2 ; :: thesis: verum
end;
let r, s be Element of CQC-WFF F1(); :: thesis: for x being Element of bound_QC-variables F1() holds
( G . ('not' r) = F6((G . r),r) & G . (r '&' s) = F7((G . r),(G . s),r,s) & G . (All (x,r)) = F8(x,(G . r),r) )
let x be Element of bound_QC-variables F1(); :: thesis: ( G . ('not' r) = F6((G . r),r) & G . (r '&' s) = F7((G . r),(G . s),r,s) & G . (All (x,r)) = F8(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
.= F6((G . r),r) by A1, A6, A7, A8 ; :: thesis: ( G . (r '&' s) = F7((G . r),(G . s),r,s) & G . (All (x,r)) = F8(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
.= F7((G . r),(G . s),r,s) by A1, A6, A9, A10, A11, A12 ; :: thesis: G . (All (x,r)) = F8(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
.= F8(x,(G . r),r) by A1, A6, A13, A14, A15 ; :: thesis: verum