:: deftheorem defines still_not-bound_in QC_LANG1:def 30 :
for A being QC-alphabet
for p being QC-formula of A
for b₃ being Subset of (bound_QC-variables A) holds
( b₃ = still_not-bound_in p iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( b₃ = F . p & ( for p being Element of QC-WFF A holds
( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Nat : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) & ( p is negative implies F . p = F . (the_argument_of p) ) & ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) & ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) ) ) ) );