let A be QC-alphabet ; :: thesis: for p being QC-formula of A holds
( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
let p be QC-formula of A; :: thesis: ( Bound_Vars (VERUM A) = {} (bound_QC-variables A) & ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
deffunc H1( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = Bound_Vars (the_arguments_of $1);
deffunc H2( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = Bound_Vars $1;
set V = bound_QC-variables A;
deffunc H3( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;
deffunc H4( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;
deffunc H5( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \/ {(bound_in $1)};
A1: for p being QC-formula of A
for X being Subset of (bound_QC-variables A) holds
( X = H2(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( X = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H1(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H3(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H4(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H5(p,d1) ) ) ) ) ) by Def8;
H2( VERUM A) = {} (bound_QC-variables A) from QC_LANG3:sch 3(A1)
.= {} ;
hence Bound_Vars (VERUM A) = {} (bound_QC-variables A) ; :: thesis: ( ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) & ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
thus ( p is atomic implies Bound_Vars p = Bound_Vars (the_arguments_of p) ) :: thesis: ( ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) & ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proof
assume A2: p is atomic ; :: thesis: Bound_Vars p = Bound_Vars (the_arguments_of p)
thus H2(p) = H1(p) from QC_LANG3:sch 4(A1, A2); :: thesis: verum
end;
thus ( p is negative implies Bound_Vars p = Bound_Vars (the_argument_of p) ) :: thesis: ( ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) & ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) )
proof
assume A3: p is negative ; :: thesis: Bound_Vars p = Bound_Vars (the_argument_of p)
thus H2(p) = H3(H2( the_argument_of p)) from QC_LANG3:sch 5(A1, A3); :: thesis: verum
end;
thus ( p is conjunctive implies Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ) :: thesis: ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} )
proof
assume A4: p is conjunctive ; :: thesis: Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p))
for d1, d2 being Subset of (bound_QC-variables A) st d1 = H2( the_left_argument_of p) & d2 = H2( the_right_argument_of p) holds
H2(p) = H4(d1,d2) from QC_LANG3:sch 6(A1, A4);
 hence Bound_Vars p = (Bound_Vars (the_left_argument_of p)) \/ (Bound_Vars (the_right_argument_of p)) ; :: thesis: verum
end;
thus ( p is universal implies Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)} ) :: thesis: verum
proof
assume A5: p is universal ; :: thesis: Bound_Vars p = (Bound_Vars (the_scope_of p)) \/ {(bound_in p)}
thus H2(p) = H5(p,H2( the_scope_of p)) from QC_LANG3:sch 7(A1, A5); :: thesis: verum
end;