:: Variables in Formulae of the First Order Language :: by Czes{\l}aw Byli\'nski and Grzegorz Bancerek :: :: Received November 23, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin scheme :: QC_LANG3:sch 1 QCFuncUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Function of (QC-WFF F1()),F2(), F4() -> Function of (QC-WFF F1()),F2(), F5() -> Element of F2(), F6( set ) -> Element of F2(), F7( set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9( set , set ) -> Element of F2() } : F3() = F4() provided A1: for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F3() . p = F5() ) & ( p is atomic implies F3() . p = F6(p) ) & ( p is negative & d1 = F3() . (the_argument_of p) implies F3() . p = F7(d1) ) & ( p is conjunctive & d1 = F3() . (the_left_argument_of p) & d2 = F3() . (the_right_argument_of p) implies F3() . p = F8(d1,d2) ) & ( p is universal & d1 = F3() . (the_scope_of p) implies F3() . p = F9(p,d1) ) ) and A2: for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F4() . p = F5() ) & ( p is atomic implies F4() . p = F6(p) ) & ( p is negative & d1 = F4() . (the_argument_of p) implies F4() . p = F7(d1) ) & ( p is conjunctive & d1 = F4() . (the_left_argument_of p) & d2 = F4() . (the_right_argument_of p) implies F4() . p = F8(d1,d2) ) & ( p is universal & d1 = F4() . (the_scope_of p) implies F4() . p = F9(p,d1) ) ) proofend; scheme :: QC_LANG3:sch 2 QCDefD{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> Element of QC-WFF F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2() } : ( ex d being Element of F2() ex F being Function of (QC-WFF F1()),F2() st ( d = F . F4() & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ( for x1, x2 being Element of F2() st ex F being Function of (QC-WFF F1()),F2() st ( x1 = F . F4() & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F1()),F2() st ( x2 = F . F4() & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) holds x1 = x2 ) ) proofend; scheme :: QC_LANG3:sch 3 QCDResult9VERUM{ F1() -> QC-alphabet , F2() -> non empty set , F3( Element of QC-WFF F1()) -> Element of F2(), F4() -> Element of F2(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2() } : F3((VERUM F1())) = F4() provided A1: for p being QC-formula of F1() for d being Element of F2() holds ( d = F3(p) iff ex F being Function of (QC-WFF F1()),F2() st ( d = F . p & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F4() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) proofend; scheme :: QC_LANG3:sch 4 QCDResult9atomic{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( Element of QC-WFF F1()) -> Element of F2(), F5() -> QC-formula of F1(), F6( Element of QC-WFF F1()) -> Element of F2(), F7( Element of F2()) -> Element of F2(), F8( Element of F2(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1(), Element of F2()) -> Element of F2() } : F4(F5()) = F6(F5()) provided A1: for p being QC-formula of F1() for d being Element of F2() holds ( d = F4(p) iff ex F being Function of (QC-WFF F1()),F2() st ( d = F . p & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F6(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F7(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F8(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F9(p,d1) ) ) ) ) ) and A2: F5() is atomic proofend; scheme :: QC_LANG3:sch 5 QCDResult9negative{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> QC-formula of F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1()) -> Element of F2() } : F9(F4()) = F6(F9((the_argument_of F4()))) provided A1: for p being QC-formula of F1() for d being Element of F2() holds ( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st ( d = F . p & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and A2: F4() is negative proofend; scheme :: QC_LANG3:sch 6 QCDResult9conjunctive{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( Element of QC-WFF F1()) -> Element of F2(), F5( Element of F2()) -> Element of F2(), F6( Element of F2(), Element of F2()) -> Element of F2(), F7( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1()) -> Element of F2(), F9() -> QC-formula of F1() } : for d1, d2 being Element of F2() st d1 = F8((the_left_argument_of F9())) & d2 = F8((the_right_argument_of F9())) holds F8(F9()) = F6(d1,d2) provided A1: for p being QC-formula of F1() for d being Element of F2() holds ( d = F8(p) iff ex F being Function of (QC-WFF F1()),F2() st ( d = F . p & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F4(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F5(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F6(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F7(p,d1) ) ) ) ) ) and A2: F9() is conjunctive proofend; scheme :: QC_LANG3:sch 7 QCDResult9universal{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4() -> QC-formula of F1(), F5( Element of QC-WFF F1()) -> Element of F2(), F6( Element of F2()) -> Element of F2(), F7( Element of F2(), Element of F2()) -> Element of F2(), F8( Element of QC-WFF F1(), Element of F2()) -> Element of F2(), F9( Element of QC-WFF F1()) -> Element of F2() } : F9(F4()) = F8(F4(),F9((the_scope_of F4()))) provided A1: for p being QC-formula of F1() for d being Element of F2() holds ( d = F9(p) iff ex F being Function of (QC-WFF F1()),F2() st ( d = F . p & ( for p being Element of QC-WFF F1() for d1, d2 being Element of F2() holds ( ( p = VERUM F1() implies F . p = F3() ) & ( p is atomic implies F . p = F5(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F6(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F7(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F8(p,d1) ) ) ) ) ) and A2: F4() is universal proofend; theorem :: QC_LANG3:1 for A being QC-alphabet for P being QC-pred_symbol of A holds P is QC-pred_symbol of (the_arity_of P),A proofend; definition let A be QC-alphabet ; let l be FinSequence of QC-variables A; let V be non empty Subset of (QC-variables A); func variables_in (l,V) -> Subset of V equals :: QC_LANG3:def 1 { (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } ; coherence { (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } is Subset of V proofend; end; :: deftheorem defines variables_in QC_LANG3:def_1_:_ for A being QC-alphabet for l being FinSequence of QC-variables A for V being non empty Subset of (QC-variables A) holds variables_in (l,V) = { (l . k) where k is Element of NAT : ( 1 <= k & k <= len l & l . k in V ) } ; theorem :: QC_LANG3:2 for A being QC-alphabet for l being FinSequence of QC-variables A holds still_not-bound_in l = variables_in (l,(bound_QC-variables A)) ; Lm1: now__::_thesis:_for_A_being_QC-alphabet_ for_p_being_QC-formula_of_A for_d_being_Subset_of_(bound_QC-variables_A)_holds_ (_d_=_H1(p)_iff_ex_F_being_Function_of_(QC-WFF_A),(bool_(bound_QC-variables_A))_st_ (_d_=_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_=_H2(p)_)_&_(_p_is_negative_&_d1_=_F_._(the_argument_of_p)_implies_F_._p_=_H4(d1)_)_&_(_p_is_conjunctive_&_d1_=_F_._(the_left_argument_of_p)_&_d2_=_F_._(the_right_argument_of_p)_implies_F_._p_=_H5(d1,d2)_)_&_(_p_is_universal_&_d1_=_F_._(the_scope_of_p)_implies_F_._p_=_H3(p,d1)_)_)_)_)_) let A be QC-alphabet ; ::_thesis: for p being QC-formula of A for d being Subset of (bound_QC-variables A) holds ( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) deffunc H1( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in $1; deffunc H2( Element of QC-WFF A) -> Element of bool (bound_QC-variables A) = still_not-bound_in (the_arguments_of $1); deffunc H3( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \ {(bound_in $1)}; deffunc H4( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1; deffunc H5( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2; thus for p being QC-formula of A for d being Subset of (bound_QC-variables A) holds ( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) ::_thesis: verum proof let p be QC-formula of A; ::_thesis: for d being Subset of (bound_QC-variables A) holds ( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) let d be Subset of (bound_QC-variables A); ::_thesis: ( d = H1(p) iff ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) ) thus ( d = still_not-bound_in p implies ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) ) ::_thesis: ( ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = H2(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H4(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H5(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H3(p,d1) ) ) ) ) implies d = H1(p) ) proof assume d = still_not-bound_in p ; ::_thesis: ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st ( d = 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 = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) then consider F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A1: ( d = 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 Element of 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)} ) ) ) ) by QC_LANG1:def_30; take F ; ::_thesis: ( d = 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 = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ) ) thus d = F . p by A1; ::_thesis: 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 = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) let p be Element of QC-WFF A; ::_thesis: 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 = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) let d1, d2 be Subset of (bound_QC-variables A); ::_thesis: ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) thus ( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) ) by A1; ::_thesis: ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) thus ( ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) by A1; ::_thesis: verum end; given F being Function of (QC-WFF A),(bool (bound_QC-variables A)) such that A2: d = F . p and A3: 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 = still_not-bound_in (the_arguments_of p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 \ {(bound_in p)} ) ) ; ::_thesis: d = H1(p) now__::_thesis:_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_Element_of_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)}_)_) let p be Element of QC-WFF A; ::_thesis: ( F . (VERUM A) = {} & ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of 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)} ) ) thus F . (VERUM A) = {} by A3; ::_thesis: ( ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of 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)} ) ) thus ( p is atomic implies F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ) ::_thesis: ( ( 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)} ) ) proof assume p is atomic ; ::_thesis: F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } then F . p = still_not-bound_in (the_arguments_of p) by A3; hence F . p = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in bound_QC-variables A ) } ; ::_thesis: verum end; thus ( p is negative implies F . p = F . (the_argument_of p) ) by A3; ::_thesis: ( ( 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)} ) ) thus ( p is conjunctive implies F . p = (F . (the_left_argument_of p)) \/ (F . (the_right_argument_of p)) ) by A3; ::_thesis: ( p is universal implies F . p = (F . (the_scope_of p)) \ {(bound_in p)} ) assume p is universal ; ::_thesis: F . p = (F . (the_scope_of p)) \ {(bound_in p)} hence F . p = (F . (the_scope_of p)) \ {(bound_in p)} by A3; ::_thesis: verum end; hence d = H1(p) by A2, QC_LANG1:def_30; ::_thesis: verum end; end; theorem Th3: :: QC_LANG3:3 for A being QC-alphabet holds still_not-bound_in (VERUM A) = {} proofend; theorem Th4: :: QC_LANG3:4 for A being QC-alphabet for p being QC-formula of A st p is atomic holds still_not-bound_in p = still_not-bound_in (the_arguments_of p) proofend; theorem :: QC_LANG3:5 for k being Element of NAT for A being QC-alphabet for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A holds still_not-bound_in (P ! l) = still_not-bound_in l proofend; theorem Th6: :: QC_LANG3:6 for A being QC-alphabet for p being QC-formula of A st p is negative holds still_not-bound_in p = still_not-bound_in (the_argument_of p) proofend; theorem Th7: :: QC_LANG3:7 for A being QC-alphabet for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p proofend; theorem Th8: :: QC_LANG3:8 for A being QC-alphabet holds still_not-bound_in (FALSUM A) = {} proofend; theorem Th9: :: QC_LANG3:9 for A being QC-alphabet for p being QC-formula of A st p is conjunctive holds still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p)) proofend; theorem Th10: :: QC_LANG3:10 for A being QC-alphabet for p, q being QC-formula of A holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) proofend; theorem Th11: :: QC_LANG3:11 for A being QC-alphabet for p being QC-formula of A st p is universal holds still_not-bound_in p = (still_not-bound_in (the_scope_of p)) \ {(bound_in p)} proofend; theorem Th12: :: QC_LANG3:12 for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x} proofend; theorem Th13: :: QC_LANG3:13 for A being QC-alphabet for p being QC-formula of A st p is disjunctive holds still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p)) proofend; theorem :: QC_LANG3:14 for A being QC-alphabet for p, q being QC-formula of A holds still_not-bound_in (p 'or' q) = (still_not-bound_in p) \/ (still_not-bound_in q) proofend; theorem Th15: :: QC_LANG3:15 for A being QC-alphabet for p being QC-formula of A st p is conditional holds still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p)) proofend; theorem Th16: :: QC_LANG3:16 for A being QC-alphabet for p, q being QC-formula of A holds still_not-bound_in (p => q) = (still_not-bound_in p) \/ (still_not-bound_in q) proofend; theorem Th17: :: QC_LANG3:17 for A being QC-alphabet for p being QC-formula of A st p is biconditional holds still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p)) proofend; theorem :: QC_LANG3:18 for A being QC-alphabet for p, q being QC-formula of A holds still_not-bound_in (p <=> q) = (still_not-bound_in p) \/ (still_not-bound_in q) proofend; theorem Th19: :: QC_LANG3:19 for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A holds still_not-bound_in (Ex (x,p)) = (still_not-bound_in p) \ {x} proofend; theorem :: QC_LANG3:20 for A being QC-alphabet holds ( VERUM A is closed & FALSUM A is closed ) proofend; theorem Th21: :: QC_LANG3:21 for A being QC-alphabet for p being QC-formula of A holds ( p is closed iff 'not' p is closed ) proofend; theorem Th22: :: QC_LANG3:22 for A being QC-alphabet for p, q being QC-formula of A holds ( ( p is closed & q is closed ) iff p '&' q is closed ) proofend; theorem Th23: :: QC_LANG3:23 for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A holds ( All (x,p) is closed iff still_not-bound_in p c= {x} ) proofend; theorem :: QC_LANG3:24 for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A st p is closed holds All (x,p) is closed proofend; theorem :: QC_LANG3:25 for A being QC-alphabet for p, q being QC-formula of A holds ( ( p is closed & q is closed ) iff p 'or' q is closed ) proofend; theorem Th26: :: QC_LANG3:26 for A being QC-alphabet for p, q being QC-formula of A holds ( ( p is closed & q is closed ) iff p => q is closed ) proofend; theorem :: QC_LANG3:27 for A being QC-alphabet for p, q being QC-formula of A holds ( ( p is closed & q is closed ) iff p <=> q is closed ) proofend; theorem Th28: :: QC_LANG3:28 for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A holds ( Ex (x,p) is closed iff still_not-bound_in p c= {x} ) proofend; theorem :: QC_LANG3:29 for A being QC-alphabet for x being bound_QC-variable of A for p being QC-formula of A st p is closed holds Ex (x,p) is closed proofend; definition let A be QC-alphabet ; let s be QC-symbol of A; func x. s -> bound_QC-variable of A equals :: QC_LANG3:def 2 [4,s]; coherence [4,s] is bound_QC-variable of A proofend; end; :: deftheorem defines x. QC_LANG3:def_2_:_ for A being QC-alphabet for s being QC-symbol of A holds x. s = [4,s]; theorem :: QC_LANG3:30 for A being QC-alphabet for x being bound_QC-variable of A ex t being QC-symbol of A st x. t = x proofend; definition let A be QC-alphabet ; let k be Element of NAT ; funcA a. k -> free_QC-variable of A equals :: QC_LANG3:def 3 [6,k]; coherence [6,k] is free_QC-variable of A proofend; end; :: deftheorem defines a. QC_LANG3:def_3_:_ for A being QC-alphabet for k being Element of NAT holds A a. k = [6,k]; theorem :: QC_LANG3:31 for A being QC-alphabet for a being free_QC-variable of A ex i being Element of NAT st A a. i = a proofend; theorem :: QC_LANG3:32 for A being QC-alphabet for c being Element of fixed_QC-variables A for a being Element of free_QC-variables A holds c <> a proofend; theorem :: QC_LANG3:33 for A being QC-alphabet for c being Element of fixed_QC-variables A for x being Element of bound_QC-variables A holds c <> x proofend; theorem :: QC_LANG3:34 for A being QC-alphabet for a being Element of free_QC-variables A for x being Element of bound_QC-variables A holds a <> x proofend; definition let A be QC-alphabet ; let V be non empty Subset of (QC-variables A); let p be Element of QC-WFF A; func Vars (p,V) -> Subset of V means :Def4: :: QC_LANG3:def 4 ex F being Function of (QC-WFF A),(bool V) st ( it = F . p & ( for p being Element of QC-WFF A for d1, d2 being Subset of V holds ( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ); correctness existence ex b1 being Subset of V ex F being Function of (QC-WFF A),(bool V) st ( b1 = F . p & ( for p being Element of QC-WFF A for d1, d2 being Subset of V holds ( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ); uniqueness for b1, b2 being Subset of V st ex F being Function of (QC-WFF A),(bool V) st ( b1 = F . p & ( for p being Element of QC-WFF A for d1, d2 being Subset of V holds ( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) & ex F being Function of (QC-WFF A),(bool V) st ( b2 = F . p & ( for p being Element of QC-WFF A for d1, d2 being Subset of V holds ( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) holds b1 = b2; proofend; end; :: deftheorem Def4 defines Vars QC_LANG3:def_4_:_ for A being QC-alphabet for V being non empty Subset of (QC-variables A) for p being Element of QC-WFF A for b4 being Subset of V holds ( b4 = Vars (p,V) iff ex F being Function of (QC-WFF A),(bool V) st ( b4 = F . p & ( for p being Element of QC-WFF A for d1, d2 being Subset of V holds ( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = variables_in ((the_arguments_of p),V) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = d1 ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = d1 \/ d2 ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = d1 ) ) ) ) ); Lm2: now__::_thesis:_for_A_being_QC-alphabet_ for_V_being_non_empty_Subset_of_(QC-variables_A)_holds_ (_H1(_VERUM_A)_=_{}_&_(_for_p_being_Element_of_QC-WFF_A_st_p_is_atomic_holds_ Vars_(p,V)_=_variables_in_((the_arguments_of_p),V)_)_&_(_for_p_being_Element_of_QC-WFF_A_st_p_is_negative_holds_ Vars_(p,V)_=_Vars_((the_argument_of_p),V)_)_&_(_for_p_being_Element_of_QC-WFF_A_st_p_is_conjunctive_holds_ Vars_(p,V)_=_(Vars_((the_left_argument_of_p),V))_\/_(Vars_((the_right_argument_of_p),V))_)_&_(_for_p_being_Element_of_QC-WFF_A_st_p_is_universal_holds_ Vars_(p,V)_=_Vars_((the_scope_of_p),V)_)_) let A be QC-alphabet ; ::_thesis: for V being non empty Subset of (QC-variables A) holds ( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) ) ) let V be non empty Subset of (QC-variables A); ::_thesis: ( H1( VERUM A) = {} & ( for p being Element of QC-WFF A st p is atomic holds Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) ) ) deffunc H1( Element of QC-WFF A) -> Subset of V = Vars ($1,V); deffunc H2( Element of QC-WFF A) -> Subset of V = variables_in ((the_arguments_of $1),V); deffunc H3( Subset of V) -> Subset of V = $1; deffunc H4( Subset of V, Subset of V) -> Element of bool V = $1 \/ $2; deffunc H5( Element of QC-WFF A, Subset of V) -> Subset of V = $2; A1: for p being Element of QC-WFF A for X being Subset of V holds ( X = H1(p) iff ex F being Function of (QC-WFF A),(bool V) st ( X = F . p & ( for p being Element of QC-WFF A for d1, d2 being Subset of V holds ( ( p = VERUM A implies F . p = {} V ) & ( p is atomic implies F . p = H2(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 Def4; thus H1( VERUM A) = {} V from QC_LANG3:sch_3(A1) .= {} ; ::_thesis: ( ( for p being Element of QC-WFF A st p is atomic holds Vars (p,V) = variables_in ((the_arguments_of p),V) ) & ( for p being Element of QC-WFF A st p is negative holds Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) ) ) thus for p being Element of QC-WFF A st p is atomic holds Vars (p,V) = variables_in ((the_arguments_of p),V) ::_thesis: ( ( for p being Element of QC-WFF A st p is negative holds Vars (p,V) = Vars ((the_argument_of p),V) ) & ( for p being Element of QC-WFF A st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) ) ) proof let p be Element of QC-WFF A; ::_thesis: ( p is atomic implies Vars (p,V) = variables_in ((the_arguments_of p),V) ) assume A2: p is atomic ; ::_thesis: Vars (p,V) = variables_in ((the_arguments_of p),V) thus H1(p) = H2(p) from QC_LANG3:sch_4(A1, A2); ::_thesis: verum end; thus for p being Element of QC-WFF A st p is negative holds Vars (p,V) = Vars ((the_argument_of p),V) ::_thesis: ( ( for p being Element of QC-WFF A st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) & ( for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) ) ) proof let p be Element of QC-WFF A; ::_thesis: ( p is negative implies Vars (p,V) = Vars ((the_argument_of p),V) ) assume A3: p is negative ; ::_thesis: Vars (p,V) = Vars ((the_argument_of p),V) thus H1(p) = H3(H1( the_argument_of p)) from QC_LANG3:sch_5(A1, A3); ::_thesis: verum end; thus for p being Element of QC-WFF A st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ::_thesis: for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) proof let p be Element of QC-WFF A; ::_thesis: ( p is conjunctive implies Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ) assume A4: p is conjunctive ; ::_thesis: Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) for d1, d2 being Subset of V st d1 = H1( the_left_argument_of p) & d2 = H1( the_right_argument_of p) holds H1(p) = H4(d1,d2) from QC_LANG3:sch_6(A1, A4); hence Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) ; ::_thesis: verum end; thus for p being Element of QC-WFF A st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) ::_thesis: verum proof let p be Element of QC-WFF A; ::_thesis: ( p is universal implies Vars (p,V) = Vars ((the_scope_of p),V) ) assume A5: p is universal ; ::_thesis: Vars (p,V) = Vars ((the_scope_of p),V) thus H1(p) = H5(p,H1( the_scope_of p)) from QC_LANG3:sch_7(A1, A5); ::_thesis: verum end; end; theorem :: QC_LANG3:35 for A being QC-alphabet for V being non empty Subset of (QC-variables A) holds Vars ((VERUM A),V) = {} by Lm2; theorem Th36: :: QC_LANG3:36 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is atomic holds ( Vars (p,V) = variables_in ((the_arguments_of p),V) & Vars (p,V) = { ((the_arguments_of p) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p) . k in V ) } ) proofend; theorem Th37: :: QC_LANG3:37 for k being Element of NAT for A being QC-alphabet for V being non empty Subset of (QC-variables A) for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A holds ( Vars ((P ! l),V) = variables_in (l,V) & Vars ((P ! l),V) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in V ) } ) proofend; theorem :: QC_LANG3:38 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is negative holds Vars (p,V) = Vars ((the_argument_of p),V) by Lm2; theorem Th39: :: QC_LANG3:39 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars (('not' p),V) = Vars (p,V) proofend; theorem Th40: :: QC_LANG3:40 for A being QC-alphabet for V being non empty Subset of (QC-variables A) holds Vars ((FALSUM A),V) = {} proofend; theorem :: QC_LANG3:41 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is conjunctive holds Vars (p,V) = (Vars ((the_left_argument_of p),V)) \/ (Vars ((the_right_argument_of p),V)) by Lm2; theorem Th42: :: QC_LANG3:42 for A being QC-alphabet for p, q being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars ((p '&' q),V) = (Vars (p,V)) \/ (Vars (q,V)) proofend; theorem :: QC_LANG3:43 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is universal holds Vars (p,V) = Vars ((the_scope_of p),V) by Lm2; theorem Th44: :: QC_LANG3:44 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars ((All (x,p)),V) = Vars (p,V) proofend; theorem Th45: :: QC_LANG3:45 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is disjunctive holds Vars (p,V) = (Vars ((the_left_disjunct_of p),V)) \/ (Vars ((the_right_disjunct_of p),V)) proofend; theorem :: QC_LANG3:46 for A being QC-alphabet for p, q being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars ((p 'or' q),V) = (Vars (p,V)) \/ (Vars (q,V)) proofend; theorem Th47: :: QC_LANG3:47 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is conditional holds Vars (p,V) = (Vars ((the_antecedent_of p),V)) \/ (Vars ((the_consequent_of p),V)) proofend; theorem Th48: :: QC_LANG3:48 for A being QC-alphabet for p, q being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars ((p => q),V) = (Vars (p,V)) \/ (Vars (q,V)) proofend; theorem Th49: :: QC_LANG3:49 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is biconditional holds Vars (p,V) = (Vars ((the_left_side_of p),V)) \/ (Vars ((the_right_side_of p),V)) proofend; theorem :: QC_LANG3:50 for A being QC-alphabet for p, q being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars ((p <=> q),V) = (Vars (p,V)) \/ (Vars (q,V)) proofend; theorem :: QC_LANG3:51 for A being QC-alphabet for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) st p is existential holds Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V) proofend; theorem :: QC_LANG3:52 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A for V being non empty Subset of (QC-variables A) holds Vars ((Ex (x,p)),V) = Vars (p,V) proofend; definition let A be QC-alphabet ; let p be Element of QC-WFF A; func Free p -> Subset of (free_QC-variables A) equals :: QC_LANG3:def 5 Vars (p,(free_QC-variables A)); correctness coherence Vars (p,(free_QC-variables A)) is Subset of (free_QC-variables A); ; end; :: deftheorem defines Free QC_LANG3:def_5_:_ for A being QC-alphabet for p being Element of QC-WFF A holds Free p = Vars (p,(free_QC-variables A)); theorem :: QC_LANG3:53 for A being QC-alphabet holds Free (VERUM A) = {} by Lm2; theorem :: QC_LANG3:54 for k being Element of NAT for A being QC-alphabet for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A holds Free (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } by Th37; theorem :: QC_LANG3:55 for A being QC-alphabet for p being Element of QC-WFF A holds Free ('not' p) = Free p by Th39; theorem :: QC_LANG3:56 for A being QC-alphabet holds Free (FALSUM A) = {} by Th40; theorem :: QC_LANG3:57 for A being QC-alphabet for p, q being Element of QC-WFF A holds Free (p '&' q) = (Free p) \/ (Free q) by Th42; theorem :: QC_LANG3:58 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds Free (All (x,p)) = Free p by Th44; theorem :: QC_LANG3:59 for A being QC-alphabet for p, q being Element of QC-WFF A holds Free (p 'or' q) = (Free p) \/ (Free q) proofend; theorem Th60: :: QC_LANG3:60 for A being QC-alphabet for p, q being Element of QC-WFF A holds Free (p => q) = (Free p) \/ (Free q) proofend; theorem :: QC_LANG3:61 for A being QC-alphabet for p, q being Element of QC-WFF A holds Free (p <=> q) = (Free p) \/ (Free q) proofend; theorem :: QC_LANG3:62 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds Free (Ex (x,p)) = Free p proofend; definition let A be QC-alphabet ; let p be Element of QC-WFF A; func Fixed p -> Subset of (fixed_QC-variables A) equals :: QC_LANG3:def 6 Vars (p,(fixed_QC-variables A)); correctness coherence Vars (p,(fixed_QC-variables A)) is Subset of (fixed_QC-variables A); ; end; :: deftheorem defines Fixed QC_LANG3:def_6_:_ for A being QC-alphabet for p being Element of QC-WFF A holds Fixed p = Vars (p,(fixed_QC-variables A)); theorem :: QC_LANG3:63 for A being QC-alphabet holds Fixed (VERUM A) = {} by Lm2; theorem :: QC_LANG3:64 for k being Element of NAT for A being QC-alphabet for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A holds Fixed (P ! l) = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by Th37; theorem :: QC_LANG3:65 for A being QC-alphabet for p being Element of QC-WFF A holds Fixed ('not' p) = Fixed p by Th39; theorem :: QC_LANG3:66 for A being QC-alphabet holds Fixed (FALSUM A) = {} proofend; theorem :: QC_LANG3:67 for A being QC-alphabet for p, q being Element of QC-WFF A holds Fixed (p '&' q) = (Fixed p) \/ (Fixed q) by Th42; theorem :: QC_LANG3:68 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds Fixed (All (x,p)) = Fixed p by Th44; theorem :: QC_LANG3:69 for A being QC-alphabet for p, q being Element of QC-WFF A holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q) proofend; theorem Th70: :: QC_LANG3:70 for A being QC-alphabet for p, q being Element of QC-WFF A holds Fixed (p => q) = (Fixed p) \/ (Fixed q) proofend; theorem :: QC_LANG3:71 for A being QC-alphabet for p, q being Element of QC-WFF A holds Fixed (p <=> q) = (Fixed p) \/ (Fixed q) proofend; theorem :: QC_LANG3:72 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds Fixed (Ex (x,p)) = Fixed p proofend;