deffunc H1( Element of QC-WFF F1(), Element of F2()) -> Element of F2() = F7((bound_in $1),$2);
deffunc H2( Element of QC-WFF F1()) -> Element of F2() = F4((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()),F2() such that
A1:
( F . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() holds
( ( p is atomic implies F . p = H2(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = H1(p,F . (the_scope_of p)) ) ) ) )
from QC_LANG1:sch 3();
reconsider G = F | (CQC-WFF F1()) as Function of (CQC-WFF F1()),F2() by FUNCT_2:32;
take
G
; ( G . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
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) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) ) ) )
thus
G . (VERUM F1()) = F3()
by A1, FUNCT_1:49; for r, s being Element of CQC-WFF F1()
for x being bound_QC-variable of F1()
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) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let r, s be Element of CQC-WFF F1(); for x being bound_QC-variable of F1()
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) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let x be bound_QC-variable of F1(); 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) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let k be Nat; for l being CQC-variable_list of k,F1()
for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let l be CQC-variable_list of k,F1(); for P being QC-pred_symbol of k,F1() holds
( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
let P be QC-pred_symbol of k,F1(); ( G . (P ! l) = F4(k,P,l) & G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
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 & the_pred_symbol_of (P ! l) = P )
by QC_LANG1:def 22, QC_LANG1:def 23;
thus G . (P ! l) =
F . (P ! l)
by FUNCT_1:49
.=
F4(k,P,l)
by A1, A3, A4, A2
; ( G . ('not' r) = F5((G . r)) & G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
set r9 = G . r;
set s9 = G . s;
A5:
G . r = F . r
by FUNCT_1:49;
A6:
r '&' s is conjunctive
by QC_LANG1:def 20;
then A7:
( the_left_argument_of (r '&' s) = r & the_right_argument_of (r '&' s) = s )
by QC_LANG1:def 25, QC_LANG1:def 26;
A8:
'not' r is negative
by QC_LANG1:def 19;
then A9:
the_argument_of ('not' r) = r
by QC_LANG1:def 24;
thus G . ('not' r) =
F . ('not' r)
by FUNCT_1:49
.=
F5((G . r))
by A1, A5, A8, A9
; ( G . (r '&' s) = F6((G . r),(G . s)) & G . (All (x,r)) = F7(x,(G . r)) )
A10:
G . s = F . s
by FUNCT_1:49;
thus G . (r '&' s) =
F . (r '&' s)
by FUNCT_1:49
.=
F6((G . r),(G . s))
by A1, A5, A10, A6, A7
; G . (All (x,r)) = F7(x,(G . r))
A11:
All (x,r) is universal
by QC_LANG1:def 21;
then A12:
( bound_in (All (x,r)) = x & the_scope_of (All (x,r)) = r )
by QC_LANG1:def 27, QC_LANG1:def 28;
thus G . (All (x,r)) =
F . (All (x,r))
by FUNCT_1:49
.=
F7(x,(G . r))
by A1, A5, A11, A12
; verum