deffunc H₁( Element of QC-WFF ) -> Element of F₁() = F₃((the_arity_of (the_pred_symbol_of $1)),(the_pred_symbol_of $1),(the_arguments_of $1));
deffunc H₂( Element of QC-WFF , Element of F₁()) -> Element of F₁() = F₆((bound_in $1),$2);
consider F being Function of QC-WFF ,F₁() such that
A1: ( F . VERUM = F₂() & ( for p being Element of QC-WFF holds
( ( p is atomic implies F . p = H₁(p) ) & ( p is negative implies F . p = F₄((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F₅((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = H₂(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch 3();
reconsider G = F | CQC-WFF as Function of CQC-WFF ,F₁() by FUNCT_2:38;
take G ; :: thesis: ( G . VERUM = F₂() & ( for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) ) ) )
thus G . VERUM = F₂() by A1, FUNCT_1:72; :: thesis: for r, s being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
let r, s be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
let x be bound_QC-variable; :: thesis: for k being Element of NAT
for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
let k be Element of NAT ; :: thesis: for l being CQC-variable_list of
for P being QC-pred_symbol of k holds
( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
let l be CQC-variable_list of ; :: thesis: for P being QC-pred_symbol of k holds
( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
let P be QC-pred_symbol of k; :: thesis: ( G . (P ! l) = F₃(k,P,l) & G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
set r' = G . r;
set s' = G . s;
A2: P ! l is atomic by QC_LANG1:def 17;
then A3: ( the_arguments_of (P ! l) = l & the_pred_symbol_of (P ! l) = P & the_arity_of P = k ) by QC_LANG1:35, QC_LANG1:def 21, QC_LANG1:def 22;
thus G . (P ! l) = F . (P ! l) by FUNCT_1:72
.= F₃(k,P,l) by A1, A2, A3 ; :: thesis: ( G . ('not' r) = F₄((G . r)) & G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
A4: ( G . r = F . r & G . s = F . s ) by FUNCT_1:72;
A5: 'not' r is negative by QC_LANG1:def 18;
then A6: the_argument_of ('not' r) = r by QC_LANG1:def 23;
thus G . ('not' r) = F . ('not' r) by FUNCT_1:72
.= F₄((G . r)) by A1, A4, A5, A6 ; :: thesis: ( G . (r '&' s) = F₅((G . r),(G . s)) & G . (All x,r) = F₆(x,(G . r)) )
A7: r '&' s is conjunctive by QC_LANG1:def 19;
then A8: ( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s ) by QC_LANG1:def 24, QC_LANG1:def 25;
thus G . (r '&' s) = F . (r '&' s) by FUNCT_1:72
.= F₅((G . r),(G . s)) by A1, A4, A7, A8 ; :: thesis: G . (All x,r) = F₆(x,(G . r))
A9: All x,r is universal by QC_LANG1:def 20;
then A10: ( bound_in (All x,r) = x & the_scope_of (All x,r) = r ) by QC_LANG1:def 26, QC_LANG1:def 27;
thus G . (All x,r) = F . (All x,r) by FUNCT_1:72
.= F₆(x,(G . r)) by A1, A4, A9, A10 ; :: thesis: verum