:: VALUAT_1 semantic presentation begin definition let Al be QC-alphabet ; let A be set ; func Valuations_in (Al,A) -> set equals :: VALUAT_1:def 1 Funcs ((bound_QC-variables Al),A); coherence Funcs ((bound_QC-variables Al),A) is set ; end; :: deftheorem defines Valuations_in VALUAT_1:def_1_:_ for Al being QC-alphabet for A being set holds Valuations_in (Al,A) = Funcs ((bound_QC-variables Al),A); registration let Al be QC-alphabet ; let A be non empty set ; cluster Valuations_in (Al,A) -> functional non empty ; coherence ( not Valuations_in (Al,A) is empty & Valuations_in (Al,A) is functional ) ; end; theorem Th1: :: VALUAT_1:1 for Al being QC-alphabet for A being non empty set for x being set st x is Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being set st x is Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A let A be non empty set ; ::_thesis: for x being set st x is Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A let x be set ; ::_thesis: ( x is Element of Valuations_in (Al,A) implies x is Function of (bound_QC-variables Al),A ) assume x is Element of Valuations_in (Al,A) ; ::_thesis: x is Function of (bound_QC-variables Al),A then ex f being Function st ( x = f & dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def_2; hence x is Function of (bound_QC-variables Al),A by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; definition let Al be QC-alphabet ; let A be non empty set ; :: original: Valuations_in redefine func Valuations_in (Al,A) -> FUNCTION_DOMAIN of bound_QC-variables Al,A; coherence Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A proof for x being Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A by Th1; hence Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A by FUNCT_2:def_12; ::_thesis: verum end; end; definition let Al be QC-alphabet ; let A be non empty set ; let x be bound_QC-variable of Al; let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); func FOR_ALL (x,p) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def2: :: VALUAT_1:def 2 for v being Element of Valuations_in (Al,A) holds it . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ; existence ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } proof deffunc H1( Function) -> Element of BOOLEAN = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = \$1 . y } ; consider f being Function of (Valuations_in (Al,A)),BOOLEAN such that A1: for v being Element of Valuations_in (Al,A) holds f . v = H1(v) from FUNCT_2:sch_4(); ( dom f = Valuations_in (Al,A) & rng f c= BOOLEAN ) by FUNCT_2:def_1, RELAT_1:def_19; then reconsider f = f as Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:def_2; take f ; ::_thesis: for v being Element of Valuations_in (Al,A) holds f . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } thus for v being Element of Valuations_in (Al,A) holds f . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } by A1; ::_thesis: verum end; uniqueness for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ) & ( for v being Element of Valuations_in (Al,A) holds b2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ) holds b1 = b2 proof let f1, f2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( ( for v being Element of Valuations_in (Al,A) holds f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ) & ( for v being Element of Valuations_in (Al,A) holds f2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ) implies f1 = f2 ) assume that A2: for v being Element of Valuations_in (Al,A) holds f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } and A3: for v being Element of Valuations_in (Al,A) holds f2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ; ::_thesis: f1 = f2 for v being Element of Valuations_in (Al,A) holds f1 . v = f2 . v proof let v be Element of Valuations_in (Al,A); ::_thesis: f1 . v = f2 . v f1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } by A2; hence f1 . v = f2 . v by A3; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def2 defines FOR_ALL VALUAT_1:def_2_:_ for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p, b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( b5 = FOR_ALL (x,p) iff for v being Element of Valuations_in (Al,A) holds b5 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v9 . y = v . y } ); theorem Th2: :: VALUAT_1:2 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) A1: now__::_thesis:_(_ex_v1_being_Element_of_Valuations_in_(Al,A)_st_ (_p_._v1_=_FALSE_&_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ v1_._y_=_v_._y_)_)_implies_(FOR_ALL_(x,p))_._v_=_FALSE_) assume ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ; ::_thesis: (FOR_ALL (x,p)) . v = FALSE then FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } ; then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } = FALSE by MARGREL1:17; hence (FOR_ALL (x,p)) . v = FALSE by Def2; ::_thesis: verum end; now__::_thesis:_(_(FOR_ALL_(x,p))_._v_=_FALSE_implies_ex_v1_being_Element_of_Valuations_in_(Al,A)_st_ (_p_._v1_=_FALSE_&_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ v1_._y_=_v_._y_)_)_) assume (FOR_ALL (x,p)) . v = FALSE ; ::_thesis: ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } = FALSE by Def2; then FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } by MARGREL1:17; hence ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ; ::_thesis: verum end; hence ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) by A1; ::_thesis: verum end; theorem Th3: :: VALUAT_1:3 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) A1: now__::_thesis:_(_(FOR_ALL_(x,p))_._v_=_TRUE_implies_for_v1_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ v1_._y_=_v_._y_)_holds_ p_._v1_=_TRUE_) assume (FOR_ALL (x,p)) . v = TRUE ; ::_thesis: for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } = TRUE by Def2; then A2: not FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } by MARGREL1:17; thus for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ::_thesis: verum proof let v1 be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) implies p . v1 = TRUE ) assume for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ; ::_thesis: p . v1 = TRUE then not p . v1 = FALSE by A2; hence p . v1 = TRUE by XBOOLEAN:def_3; ::_thesis: verum end; end; now__::_thesis:_(_(_for_v1_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ v1_._y_=_v_._y_)_holds_ p_._v1_=_TRUE_)_implies_(FOR_ALL_(x,p))_._v_=_TRUE_) assume for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ; ::_thesis: (FOR_ALL (x,p)) . v = TRUE then for v1 being Element of Valuations_in (Al,A) holds ( not p . v1 = FALSE or ex y being bound_QC-variable of Al st ( x <> y & not v1 . y = v . y ) ) ; then not FALSE in { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } ; then ALL { (p . v99) where v99 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds v99 . y = v . y } = TRUE by MARGREL1:17; hence (FOR_ALL (x,p)) . v = TRUE by Def2; ::_thesis: verum end; hence ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) by A1; ::_thesis: verum end; notation let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let ll be CQC-variable_list of k,Al; let v be Element of Valuations_in (Al,A); synonym v *' ll for A * Al; end; definition let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let ll be CQC-variable_list of k,Al; let v be Element of Valuations_in (Al,A); :: original: *' redefine funcv *' ll -> FinSequence of A means :Def3: :: VALUAT_1:def 3 ( len it = k & ( for i being natural number st 1 <= i & i <= k holds it . i = v . (ll . i) ) ); coherence *' is FinSequence of A proof ( rng v c= A & rng (v * ll) c= rng v ) by RELAT_1:26, RELAT_1:def_19; then A1: rng (v * ll) c= A by XBOOLE_1:1; A2: len ll = k by CARD_1:def_7; dom v = bound_QC-variables Al by FUNCT_2:def_1; then rng ll c= dom v by RELAT_1:def_19; then dom (v * ll) = dom ll by RELAT_1:27 .= Seg k by A2, FINSEQ_1:def_3 ; then v * ll is FinSequence-like by FINSEQ_1:def_2; hence *' is FinSequence of A by A1, FINSEQ_1:def_4; ::_thesis: verum end; compatibility for b1 being FinSequence of A holds ( b1 = *' iff ( len b1 = k & ( for i being natural number st 1 <= i & i <= k holds b1 . i = v . (ll . i) ) ) ) proof let IT be FinSequence of A; ::_thesis: ( IT = *' iff ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds IT . i = v . (ll . i) ) ) ) A3: len ll = k by CARD_1:def_7; dom v = bound_QC-variables Al by FUNCT_2:def_1; then A4: rng ll c= dom v by RELAT_1:def_19; thus ( IT = v * ll implies ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds IT . i = v . (ll . i) ) ) ) ::_thesis: ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds IT . i = v . (ll . i) ) implies IT = *' ) proof assume A5: IT = v * ll ; ::_thesis: ( len IT = k & ( for i being natural number st 1 <= i & i <= k holds IT . i = v . (ll . i) ) ) then A6: dom ll = dom IT by A4, RELAT_1:27; hence len IT = k by A3, FINSEQ_3:29; ::_thesis: for i being natural number st 1 <= i & i <= k holds IT . i = v . (ll . i) let i be natural number ; ::_thesis: ( 1 <= i & i <= k implies IT . i = v . (ll . i) ) assume ( 1 <= i & i <= k ) ; ::_thesis: IT . i = v . (ll . i) then i in dom IT by A3, A6, FINSEQ_3:25; hence IT . i = v . (ll . i) by A5, FUNCT_1:12; ::_thesis: verum end; assume that A7: len IT = k and A8: for i being Nat st 1 <= i & i <= k holds IT . i = v . (ll . i) ; ::_thesis: IT = *' A9: for x being set holds ( x in dom IT iff ( x in dom ll & ll . x in dom v ) ) proof let x be set ; ::_thesis: ( x in dom IT iff ( x in dom ll & ll . x in dom v ) ) thus ( x in dom IT implies ( x in dom ll & ll . x in dom v ) ) ::_thesis: ( x in dom ll & ll . x in dom v implies x in dom IT ) proof assume x in dom IT ; ::_thesis: ( x in dom ll & ll . x in dom v ) hence x in dom ll by A3, A7, FINSEQ_3:29; ::_thesis: ll . x in dom v then ll . x in rng ll by FUNCT_1:def_3; hence ll . x in dom v by A4; ::_thesis: verum end; assume that A10: x in dom ll and ll . x in dom v ; ::_thesis: x in dom IT thus x in dom IT by A3, A7, A10, FINSEQ_3:29; ::_thesis: verum end; for x being set st x in dom IT holds IT . x = v . (ll . x) proof let x be set ; ::_thesis: ( x in dom IT implies IT . x = v . (ll . x) ) assume A11: x in dom IT ; ::_thesis: IT . x = v . (ll . x) then reconsider i = x as Element of NAT ; ( 1 <= i & i <= k ) by A7, A11, FINSEQ_3:25; hence IT . x = v . (ll . x) by A8; ::_thesis: verum end; hence IT = *' by A9, FUNCT_1:10; ::_thesis: verum end; end; :: deftheorem Def3 defines *' VALUAT_1:def_3_:_ for Al being QC-alphabet for A being non empty set for k being Element of NAT for ll being CQC-variable_list of k,Al for v being Element of Valuations_in (Al,A) for b6 being FinSequence of A holds ( b6 = v *' ll iff ( len b6 = k & ( for i being natural number st 1 <= i & i <= k holds b6 . i = v . (ll . i) ) ) ); definition let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let ll be CQC-variable_list of k,Al; let r be Element of relations_on A; funcll 'in' r -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def4: :: VALUAT_1:def 4 for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies it . v = TRUE ) & ( it . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies it . v = FALSE ) & ( it . v = FALSE implies not v *' ll in r ) ); existence ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) ) proof defpred S1[ set ] means ex v being Element of Valuations_in (Al,A) st ( \$1 = v & v *' ll in r ); deffunc H1( set ) -> Element of BOOLEAN = TRUE ; deffunc H2( set ) -> Element of BOOLEAN = FALSE ; A1: for x being set st x in Valuations_in (Al,A) holds ( ( S1[x] implies H1(x) in BOOLEAN ) & ( not S1[x] implies H2(x) in BOOLEAN ) ) ; consider f being Function of (Valuations_in (Al,A)),BOOLEAN such that A2: for x being set st x in Valuations_in (Al,A) holds ( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) ) from FUNCT_2:sch_5(A1); ( dom f = Valuations_in (Al,A) & rng f c= BOOLEAN ) by FUNCT_2:def_1, RELAT_1:def_19; then reconsider f = f as Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:def_2; take f ; ::_thesis: for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies f . v = TRUE ) & ( f . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f . v = FALSE ) & ( f . v = FALSE implies not v *' ll in r ) ) let v be Element of Valuations_in (Al,A); ::_thesis: ( ( v *' ll in r implies f . v = TRUE ) & ( f . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f . v = FALSE ) & ( f . v = FALSE implies not v *' ll in r ) ) ( ( for v9 being Element of Valuations_in (Al,A) holds ( not v = v9 or not v9 *' ll in r ) ) implies f . v = FALSE ) by A2; hence ( ( v *' ll in r implies f . v = TRUE ) & ( f . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f . v = FALSE ) & ( f . v = FALSE implies not v *' ll in r ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b2 . v = TRUE ) & ( b2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b2 . v = FALSE ) & ( b2 . v = FALSE implies not v *' ll in r ) ) ) holds b1 = b2 proof let f1, f2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( ( for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies f1 . v = TRUE ) & ( f1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f1 . v = FALSE ) & ( f1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies f2 . v = TRUE ) & ( f2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f2 . v = FALSE ) & ( f2 . v = FALSE implies not v *' ll in r ) ) ) implies f1 = f2 ) assume that A3: for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies f1 . v = TRUE ) & ( f1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f1 . v = FALSE ) & ( f1 . v = FALSE implies not v *' ll in r ) ) and A4: for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies f2 . v = TRUE ) & ( f2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies f2 . v = FALSE ) & ( f2 . v = FALSE implies not v *' ll in r ) ) ; ::_thesis: f1 = f2 for v being Element of Valuations_in (Al,A) holds f1 . v = f2 . v proof let v be Element of Valuations_in (Al,A); ::_thesis: f1 . v = f2 . v percases ( v *' ll in r or not v *' ll in r ) ; supposeA5: v *' ll in r ; ::_thesis: f1 . v = f2 . v then f1 . v = TRUE by A3; hence f1 . v = f2 . v by A4, A5; ::_thesis: verum end; supposeA6: not v *' ll in r ; ::_thesis: f1 . v = f2 . v then f1 . v = FALSE by A3; hence f1 . v = f2 . v by A4, A6; ::_thesis: verum end; end; end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines 'in' VALUAT_1:def_4_:_ for Al being QC-alphabet for A being non empty set for k being Element of NAT for ll being CQC-variable_list of k,Al for r being Element of relations_on A for b6 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( b6 = ll 'in' r iff for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b6 . v = TRUE ) & ( b6 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b6 . v = FALSE ) & ( b6 . v = FALSE implies not v *' ll in r ) ) ); definition let Al be QC-alphabet ; let A be non empty set ; let F be Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)); let p be Element of CQC-WFF Al; :: original: . redefine funcF . p -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); coherence F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) proof thus F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ; ::_thesis: verum end; end; definition let Al be QC-alphabet ; let D be non empty set ; mode interpretation of Al,D -> Function of (QC-pred_symbols Al),(relations_on D) means :: VALUAT_1:def 5 for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not it . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ); existence ex b1 being Function of (QC-pred_symbols Al),(relations_on D) st for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not b1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) proof reconsider F1 = (QC-pred_symbols Al) --> (empty_rel D) as Function of (QC-pred_symbols Al),(relations_on D) ; take F1 ; ::_thesis: for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) let P be Element of QC-pred_symbols Al; ::_thesis: for r being Element of relations_on D holds ( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) thus for r being Element of relations_on D holds ( not F1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) by FUNCOP_1:7; ::_thesis: verum end; end; :: deftheorem defines interpretation VALUAT_1:def_5_:_ for Al being QC-alphabet for D being non empty set for b3 being Function of (QC-pred_symbols Al),(relations_on D) holds ( b3 is interpretation of Al,D iff for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not b3 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) ); definition let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let J be interpretation of Al,A; let P be QC-pred_symbol of k,Al; :: original: . redefine funcJ . P -> Element of relations_on A; coherence J . P is Element of relations_on A by FUNCT_2:5; end; definition let Al be QC-alphabet ; let A be non empty set ; let J be interpretation of Al,A; let p be Element of CQC-WFF Al; func Valid (p,J) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def6: :: VALUAT_1:def 6 ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( it = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ); existence ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) proof deffunc H1( Element of NAT , QC-pred_symbol of \$1,Al, CQC-variable_list of \$1,Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = \$3 'in' (J . \$2); set D = Funcs ((Valuations_in (Al,A)),BOOLEAN); set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H2( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (('not' \$1),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H3( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN), Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((\$1 '&' \$2),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H4( bound_QC-variable of Al, Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((FOR_ALL (\$1,\$2)),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); consider F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that W1: F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) and W2: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! l) = H1(k,P,l) & F . ('not' r) = H2(F . r) & F . (r '&' s) = H3(F . r,F . s) & F . (All (x,r)) = H4(x,F . r) ) from CQC_LANG:sch_2(); take F . p ; ::_thesis: ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( F . p = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) take F ; ::_thesis: ( F . p = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) thus F . p = F . p ; ::_thesis: ( F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) (Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; hence F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE by W1, FUNCT_7:def_1; ::_thesis: for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let p, q be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let ll be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let P be QC-pred_symbol of k,Al; ::_thesis: ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) thus F . (P ! ll) = ll 'in' (J . P) by W2; ::_thesis: ( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) X1: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F . ('not' p) = H2(F . p) by W2 .= 'not' (F . p) by X1, FUNCT_7:def_1 ; ::_thesis: ( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) X1: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F . (p '&' q) = H3(F . p,F . q) by W2 .= (F . p) '&' (F . q) by X1, FUNCT_7:def_1 ; ::_thesis: F . (All (x,p)) = FOR_ALL (x,(F . p)) thus F . (All (x,p)) = H4(x,F . p) by W2 .= FOR_ALL (x,(F . p)) by FUNCT_7:def_1 ; ::_thesis: verum end; uniqueness for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( b2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) holds b1 = b2 proof deffunc H1( Element of NAT , QC-pred_symbol of \$1,Al, CQC-variable_list of \$1,Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = \$3 'in' (J . \$2); set D = Funcs ((Valuations_in (Al,A)),BOOLEAN); set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H2( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (('not' \$1),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H3( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN), Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((\$1 '&' \$2),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H4( bound_QC-variable of Al, Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((FOR_ALL (\$1,\$2)),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); let d1, d2 be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) implies d1 = d2 ) given F1 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that Z1: d1 = F1 . p and Z2: F1 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and Z3: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = 'not' (F1 . r) & F1 . (r '&' s) = (F1 . r) '&' (F1 . s) & F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) ) ; ::_thesis: ( for F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) holds ( not d2 = F . p or not F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE or ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al ex k being Element of NAT ex ll being CQC-variable_list of k,Al ex P being QC-pred_symbol of k,Al st ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) implies not F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) or d1 = d2 ) Y2: now__::_thesis:_(_F1_._(VERUM_Al)_=_In_(((Valuations_in_(Al,A))_-->_TRUE),(Funcs_((Valuations_in_(Al,A)),BOOLEAN)))_&_(_for_r,_s_being_Element_of_CQC-WFF_Al for_x_being_bound_QC-variable_of_Al for_k_being_Element_of_NAT_ for_l_being_CQC-variable_list_of_k,Al for_P_being_QC-pred_symbol_of_k,Al_holds_ (_F1_._(P_!_l)_=_H1(k,P,l)_&_F1_._('not'_r)_=_H2(F1_._r)_&_F1_._(r_'&'_s)_=_H3(F1_._r,F1_._s)_&_F1_._(All_(x,r))_=_H4(x,F1_._r)_)_)_) thus F1 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by Z2, FUNCT_7:def_1; ::_thesis: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) let r, s be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) let k be Element of NAT ; ::_thesis: for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) let l be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) let P be QC-pred_symbol of k,Al; ::_thesis: ( F1 . (P ! l) = H1(k,P,l) & F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) thus F1 . (P ! l) = H1(k,P,l) by Z3; ::_thesis: ( F1 . ('not' r) = H2(F1 . r) & F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) X1: 'not' (F1 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F1 . ('not' r) = 'not' (F1 . r) by Z3 .= H2(F1 . r) by X1, FUNCT_7:def_1 ; ::_thesis: ( F1 . (r '&' s) = H3(F1 . r,F1 . s) & F1 . (All (x,r)) = H4(x,F1 . r) ) X1: (F1 . r) '&' (F1 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F1 . (r '&' s) = (F1 . r) '&' (F1 . s) by Z3 .= H3(F1 . r,F1 . s) by X1, FUNCT_7:def_1 ; ::_thesis: F1 . (All (x,r)) = H4(x,F1 . r) thus F1 . (All (x,r)) = FOR_ALL (x,(F1 . r)) by Z3 .= H4(x,F1 . r) by FUNCT_7:def_1 ; ::_thesis: verum end; given F2 being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that Z4: d2 = F2 . p and Z5: F2 . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and Z6: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = 'not' (F2 . r) & F2 . (r '&' s) = (F2 . r) '&' (F2 . s) & F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) ) ; ::_thesis: d1 = d2 Y5: now__::_thesis:_(_F2_._(VERUM_Al)_=_In_(((Valuations_in_(Al,A))_-->_TRUE),(Funcs_((Valuations_in_(Al,A)),BOOLEAN)))_&_(_for_r,_s_being_Element_of_CQC-WFF_Al for_x_being_bound_QC-variable_of_Al for_k_being_Element_of_NAT_ for_l_being_CQC-variable_list_of_k,Al for_P_being_QC-pred_symbol_of_k,Al_holds_ (_F2_._(P_!_l)_=_H1(k,P,l)_&_F2_._('not'_r)_=_H2(F2_._r)_&_F2_._(r_'&'_s)_=_H3(F2_._r,F2_._s)_&_F2_._(All_(x,r))_=_H4(x,F2_._r)_)_)_) thus F2 . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by Z5, FUNCT_7:def_1; ::_thesis: for r, s being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) let r, s be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) let k be Element of NAT ; ::_thesis: for l being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) let l be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) let P be QC-pred_symbol of k,Al; ::_thesis: ( F2 . (P ! l) = H1(k,P,l) & F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) thus F2 . (P ! l) = H1(k,P,l) by Z6; ::_thesis: ( F2 . ('not' r) = H2(F2 . r) & F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) X1: 'not' (F2 . r) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F2 . ('not' r) = 'not' (F2 . r) by Z6 .= H2(F2 . r) by X1, FUNCT_7:def_1 ; ::_thesis: ( F2 . (r '&' s) = H3(F2 . r,F2 . s) & F2 . (All (x,r)) = H4(x,F2 . r) ) X1: (F2 . r) '&' (F2 . s) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F2 . (r '&' s) = (F2 . r) '&' (F2 . s) by Z6 .= H3(F2 . r,F2 . s) by X1, FUNCT_7:def_1 ; ::_thesis: F2 . (All (x,r)) = H4(x,F2 . r) thus F2 . (All (x,r)) = FOR_ALL (x,(F2 . r)) by Z6 .= H4(x,F2 . r) by FUNCT_7:def_1 ; ::_thesis: verum end; F1 = F2 from CQC_LANG:sch_3(Y2, Y5); hence d1 = d2 by Z1, Z4; ::_thesis: verum end; end; :: deftheorem Def6 defines Valid VALUAT_1:def_6_:_ for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A for p being Element of CQC-WFF Al for b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( b5 = Valid (p,J) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( b5 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) ); Lm1: for Al being QC-alphabet for p being Element of CQC-WFF Al for A being non empty set for J being interpretation of Al,A holds ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for A being non empty set for J being interpretation of Al,A holds ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) let p be Element of CQC-WFF Al; ::_thesis: for A being non empty set for J being interpretation of Al,A holds ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) let A be non empty set ; ::_thesis: for J being interpretation of Al,A holds ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) let J be interpretation of Al,A; ::_thesis: ( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) set D = Funcs ((Valuations_in (Al,A)),BOOLEAN); set V = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H1( Element of NAT , QC-pred_symbol of \$1,Al, CQC-variable_list of \$1,Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = \$3 'in' (J . \$2); deffunc H2( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In (('not' \$1),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H3( Element of Funcs ((Valuations_in (Al,A)),BOOLEAN), Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((\$1 '&' \$2),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H4( bound_QC-variable of Al, Element of Funcs ((Valuations_in (Al,A)),BOOLEAN)) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = In ((FOR_ALL (\$1,\$2)),(Funcs ((Valuations_in (Al,A)),BOOLEAN))); deffunc H5( Element of CQC-WFF Al) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) = Valid (\$1,J); A1: for p being Element of CQC-WFF Al for d being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) ) proof let p be Element of CQC-WFF Al; ::_thesis: for d being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) ) let d be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( d = H5(p) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) ) thus ( d = H5(p) implies ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) ) ::_thesis: ( ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) implies d = H5(p) ) proof assume d = H5(p) ; ::_thesis: ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) then consider F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that W1: d = F . p and W2: F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE and W3: for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) by Def6; take F ; ::_thesis: ( d = F . p & F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) thus d = F . p by W1; ::_thesis: ( F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) & ( for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ) ) thus F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) by W2, FUNCT_7:def_1; ::_thesis: for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) let p, q be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) let ll be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) let P be QC-pred_symbol of k,Al; ::_thesis: ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) thus F . (P ! ll) = H1(k,P,ll) by W3; ::_thesis: ( F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) X1: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F . ('not' p) = 'not' (F . p) by W3 .= H2(F . p) by X1, FUNCT_7:def_1 ; ::_thesis: ( F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) X1: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F . (p '&' q) = (F . p) '&' (F . q) by W3 .= H3(F . p,F . q) by X1, FUNCT_7:def_1 ; ::_thesis: F . (All (x,p)) = H4(x,F . p) thus F . (All (x,p)) = FOR_ALL (x,(F . p)) by W3 .= H4(x,F . p) by FUNCT_7:def_1 ; ::_thesis: verum end; given F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) such that G1: d = F . p and G2: F . (VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) and G3: for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = H2(F . p) & F . (p '&' q) = H3(F . p,F . q) & F . (All (x,p)) = H4(x,F . p) ) ; ::_thesis: d = H5(p) (Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; then H2: F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE by G2, FUNCT_7:def_1; for p, q being Element of CQC-WFF Al for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) proof let p, q be Element of CQC-WFF Al; ::_thesis: for x being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let x be bound_QC-variable of Al; ::_thesis: for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let ll be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) let P be QC-pred_symbol of k,Al; ::_thesis: ( F . (P ! ll) = H1(k,P,ll) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) thus F . (P ! ll) = H1(k,P,ll) by G3; ::_thesis: ( F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) X1: 'not' (F . p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F . ('not' p) = H2(F . p) by G3 .= 'not' (F . p) by X1, FUNCT_7:def_1 ; ::_thesis: ( F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) X1: (F . p) '&' (F . q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; thus F . (p '&' q) = H3(F . p,F . q) by G3 .= (F . p) '&' (F . q) by X1, FUNCT_7:def_1 ; ::_thesis: F . (All (x,p)) = FOR_ALL (x,(F . p)) thus F . (All (x,p)) = H4(x,F . p) by G3 .= FOR_ALL (x,(F . p)) by FUNCT_7:def_1 ; ::_thesis: verum end; hence d = H5(p) by G1, H2, Def6; ::_thesis: verum end; X1: (Valuations_in (Al,A)) --> TRUE in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; H5( VERUM Al) = In (((Valuations_in (Al,A)) --> TRUE),(Funcs ((Valuations_in (Al,A)),BOOLEAN))) from CQC_LANG:sch_5(A1); hence H5( VERUM Al) = (Valuations_in (Al,A)) --> TRUE by X1, FUNCT_7:def_1; ::_thesis: ( ( for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) hereby ::_thesis: ( ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds H5(P ! ll) = H1(k,P,ll) let ll be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds H5(P ! ll) = H1(k,P,ll) let P be QC-pred_symbol of k,Al; ::_thesis: H5(P ! ll) = H1(k,P,ll) thus H5(P ! ll) = H1(k,P,ll) from CQC_LANG:sch_6(A1); ::_thesis: verum end; hereby ::_thesis: ( ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) ) let p be Element of CQC-WFF Al; ::_thesis: H5( 'not' p) = 'not' H5(p) X1: 'not' H5(p) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; H5( 'not' p) = H2(H5(p)) from CQC_LANG:sch_7(A1); hence H5( 'not' p) = 'not' H5(p) by X1, FUNCT_7:def_1; ::_thesis: verum end; hereby ::_thesis: for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) let q be Element of CQC-WFF Al; ::_thesis: H5(p '&' q) = H5(p) '&' H5(q) X1: H5(p) '&' H5(q) in Funcs ((Valuations_in (Al,A)),BOOLEAN) by FUNCT_2:8; H5(p '&' q) = H3(H5(p),H5(q)) from CQC_LANG:sch_8(A1); hence H5(p '&' q) = H5(p) '&' H5(q) by X1, FUNCT_7:def_1; ::_thesis: verum end; let x be bound_QC-variable of Al; ::_thesis: Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) H5( All (x,p)) = H4(x,H5(p)) from CQC_LANG:sch_9(A1); hence H5( All (x,p)) = FOR_ALL (x,H5(p)) by FUNCT_7:def_1; ::_thesis: verum end; theorem :: VALUAT_1:4 for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A holds Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE by Lm1; theorem Th5: :: VALUAT_1:5 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE let v be Element of Valuations_in (Al,A); ::_thesis: for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE let J be interpretation of Al,A; ::_thesis: (Valid ((VERUM Al),J)) . v = TRUE ((Valuations_in (Al,A)) --> TRUE) . v = TRUE by FUNCOP_1:7; hence (Valid ((VERUM Al),J)) . v = TRUE by Lm1; ::_thesis: verum end; theorem :: VALUAT_1:6 for Al being QC-alphabet for k being Element of NAT for A being non empty set for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) by Lm1; theorem Th7: :: VALUAT_1:7 for Al being QC-alphabet for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let k be Element of NAT ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let v be Element of Valuations_in (Al,A); ::_thesis: for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let ll be CQC-variable_list of k,Al; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let J be interpretation of Al,A; ::_thesis: for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let P be QC-pred_symbol of k,Al; ::_thesis: for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) let r be Element of relations_on A; ::_thesis: ( p = P ! ll & r = J . P implies ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) ) assume that A1: p = P ! ll and A2: r = J . P ; ::_thesis: ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) A3: now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_v_*'_ll_in_r_) assume (Valid (p,J)) . v = TRUE ; ::_thesis: v *' ll in r then (ll 'in' (J . P)) . v <> FALSE by A1, Lm1; hence v *' ll in r by A2, Def4; ::_thesis: verum end; now__::_thesis:_(_v_*'_ll_in_r_implies_(Valid_(p,J))_._v_=_TRUE_) assume v *' ll in r ; ::_thesis: (Valid (p,J)) . v = TRUE then (ll 'in' (J . P)) . v = TRUE by A2, Def4; hence (Valid (p,J)) . v = TRUE by A1, Lm1; ::_thesis: verum end; hence ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) by A3; ::_thesis: verum end; theorem Th8: :: VALUAT_1:8 for Al being QC-alphabet for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let k be Element of NAT ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let v be Element of Valuations_in (Al,A); ::_thesis: for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let ll be CQC-variable_list of k,Al; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let J be interpretation of Al,A; ::_thesis: for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let P be QC-pred_symbol of k,Al; ::_thesis: for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) let r be Element of relations_on A; ::_thesis: ( p = P ! ll & r = J . P implies ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) ) assume that A1: p = P ! ll and A2: r = J . P ; ::_thesis: ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) A3: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_not_v_*'_ll_in_r_) assume (Valid (p,J)) . v = FALSE ; ::_thesis: not v *' ll in r then (ll 'in' (J . P)) . v <> TRUE by A1, Lm1; hence not v *' ll in r by A2, Def4; ::_thesis: verum end; now__::_thesis:_(_not_v_*'_ll_in_r_implies_(Valid_(p,J))_._v_=_FALSE_) assume not v *' ll in r ; ::_thesis: (Valid (p,J)) . v = FALSE then (ll 'in' (J . P)) . v = FALSE by A2, Def4; hence (Valid (p,J)) . v = FALSE by A1, Lm1; ::_thesis: verum end; hence ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) by A3; ::_thesis: verum end; theorem :: VALUAT_1:9 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid (('not' p),J) = 'not' (Valid (p,J)) by Lm1; theorem Th10: :: VALUAT_1:10 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) let J be interpretation of Al,A; ::_thesis: (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) (Valid (('not' p),J)) . v = ('not' (Valid (p,J))) . v by Lm1; hence (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) by MARGREL1:def_19; ::_thesis: verum end; theorem :: VALUAT_1:11 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) by Lm1; theorem Th12: :: VALUAT_1:12 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) let J be interpretation of Al,A; ::_thesis: (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) (Valid ((p '&' q),J)) . v = ((Valid (p,J)) '&' (Valid (q,J))) . v by Lm1; hence (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) by MARGREL1:def_20; ::_thesis: verum end; theorem :: VALUAT_1:13 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) by Lm1; theorem Th14: :: VALUAT_1:14 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE let J be interpretation of Al,A; ::_thesis: (Valid ((p '&' ('not' p)),J)) . v = FALSE A1: now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_((Valid_(p,J))_._v)_'&'_('not'_((Valid_(p,J))_._v))_=_FALSE_) assume (Valid (p,J)) . v = TRUE ; ::_thesis: ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) = FALSE then 'not' ((Valid (p,J)) . v) = FALSE by MARGREL1:11; hence ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) = FALSE by MARGREL1:12; ::_thesis: verum end; A2: ( (Valid (p,J)) . v = FALSE implies ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) = FALSE ) by MARGREL1:12; (Valid ((p '&' ('not' p)),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (('not' p),J)) . v) by Th12 .= ((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v)) by Th10 ; hence (Valid ((p '&' ('not' p)),J)) . v = FALSE by A1, A2, XBOOLEAN:def_3; ::_thesis: verum end; theorem :: VALUAT_1:15 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE let J be interpretation of Al,A; ::_thesis: (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE (Valid (('not' (p '&' ('not' p))),J)) . v = 'not' ((Valid ((p '&' ('not' p)),J)) . v) by Th10 .= 'not' FALSE by Th14 ; hence (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE by MARGREL1:11; ::_thesis: verum end; definition let Al be QC-alphabet ; let A be non empty set ; let p be Element of CQC-WFF Al; let J be interpretation of Al,A; let v be Element of Valuations_in (Al,A); predJ,v |= p means :Def7: :: VALUAT_1:def 7 (Valid (p,J)) . v = TRUE ; end; :: deftheorem Def7 defines |= VALUAT_1:def_7_:_ for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds ( J,v |= p iff (Valid (p,J)) . v = TRUE ); theorem :: VALUAT_1:16 for Al being QC-alphabet for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) let k be Element of NAT ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) let v be Element of Valuations_in (Al,A); ::_thesis: for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) let ll be CQC-variable_list of k,Al; ::_thesis: for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) let J be interpretation of Al,A; ::_thesis: for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) let P be QC-pred_symbol of k,Al; ::_thesis: ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) A1: now__::_thesis:_(_(ll_'in'_(J_._P))_._v_=_TRUE_implies_J,v_|=_P_!_ll_) assume (ll 'in' (J . P)) . v = TRUE ; ::_thesis: J,v |= P ! ll then (Valid ((P ! ll),J)) . v = TRUE by Lm1; hence J,v |= P ! ll by Def7; ::_thesis: verum end; now__::_thesis:_(_J,v_|=_P_!_ll_implies_(ll_'in'_(J_._P))_._v_=_TRUE_) assume J,v |= P ! ll ; ::_thesis: (ll 'in' (J . P)) . v = TRUE then (Valid ((P ! ll),J)) . v = TRUE by Def7; hence (ll 'in' (J . P)) . v = TRUE by Lm1; ::_thesis: verum end; hence ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) by A1; ::_thesis: verum end; theorem :: VALUAT_1:17 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= 'not' p iff not J,v |= p ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= 'not' p iff not J,v |= p ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= 'not' p iff not J,v |= p ) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= 'not' p iff not J,v |= p ) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= 'not' p iff not J,v |= p ) let J be interpretation of Al,A; ::_thesis: ( J,v |= 'not' p iff not J,v |= p ) A1: now__::_thesis:_(_not_J,v_|=_p_implies_J,v_|=_'not'_p_) assume not J,v |= p ; ::_thesis: J,v |= 'not' p then not (Valid (p,J)) . v = TRUE by Def7; then (Valid (p,J)) . v = FALSE by XBOOLEAN:def_3; then 'not' ((Valid (p,J)) . v) = TRUE by MARGREL1:11; then ('not' (Valid (p,J))) . v = TRUE by MARGREL1:def_19; then (Valid (('not' p),J)) . v = TRUE by Lm1; hence J,v |= 'not' p by Def7; ::_thesis: verum end; now__::_thesis:_(_J,v_|=_'not'_p_implies_not_J,v_|=_p_) assume J,v |= 'not' p ; ::_thesis: not J,v |= p then (Valid (('not' p),J)) . v = TRUE by Def7; then ('not' (Valid (p,J))) . v = TRUE by Lm1; then 'not' ((Valid (p,J)) . v) = TRUE by MARGREL1:def_19; then (Valid (p,J)) . v = FALSE by MARGREL1:11; hence not J,v |= p by Def7; ::_thesis: verum end; hence ( J,v |= 'not' p iff not J,v |= p ) by A1; ::_thesis: verum end; theorem :: VALUAT_1:18 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) let J be interpretation of Al,A; ::_thesis: ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) A1: now__::_thesis:_(_J,v_|=_p_&_J,v_|=_q_implies_J,v_|=_p_'&'_q_) assume ( J,v |= p & J,v |= q ) ; ::_thesis: J,v |= p '&' q then ( (Valid (p,J)) . v = TRUE & (Valid (q,J)) . v = TRUE ) by Def7; then ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) = TRUE ; then ((Valid (p,J)) '&' (Valid (q,J))) . v = TRUE by MARGREL1:def_20; then (Valid ((p '&' q),J)) . v = TRUE by Lm1; hence J,v |= p '&' q by Def7; ::_thesis: verum end; now__::_thesis:_(_J,v_|=_p_'&'_q_implies_(_J,v_|=_p_&_J,v_|=_q_)_) assume J,v |= p '&' q ; ::_thesis: ( J,v |= p & J,v |= q ) then (Valid ((p '&' q),J)) . v = TRUE by Def7; then ((Valid (p,J)) '&' (Valid (q,J))) . v = TRUE by Lm1; then ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) = TRUE by MARGREL1:def_20; then ( (Valid (p,J)) . v = TRUE & (Valid (q,J)) . v = TRUE ) by MARGREL1:12; hence ( J,v |= p & J,v |= q ) by Def7; ::_thesis: verum end; hence ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) by A1; ::_thesis: verum end; theorem Th19: :: VALUAT_1:19 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) let J be interpretation of Al,A; ::_thesis: ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) A1: now__::_thesis:_(_(FOR_ALL_(x,(Valid_(p,J))))_._v_=_TRUE_implies_J,v_|=_All_(x,p)_) assume (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ; ::_thesis: J,v |= All (x,p) then (Valid ((All (x,p)),J)) . v = TRUE by Lm1; hence J,v |= All (x,p) by Def7; ::_thesis: verum end; now__::_thesis:_(_J,v_|=_All_(x,p)_implies_(FOR_ALL_(x,(Valid_(p,J))))_._v_=_TRUE_) assume J,v |= All (x,p) ; ::_thesis: (FOR_ALL (x,(Valid (p,J)))) . v = TRUE then (Valid ((All (x,p)),J)) . v = TRUE by Def7; hence (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Lm1; ::_thesis: verum end; hence ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) by A1; ::_thesis: verum end; theorem Th20: :: VALUAT_1:20 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) let J be interpretation of Al,A; ::_thesis: ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) hereby ::_thesis: ( ( for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) implies J,v |= All (x,p) ) assume J,v |= All (x,p) ; ::_thesis: for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE then (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Th19; hence for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE by Th3; ::_thesis: verum end; assume for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ; ::_thesis: J,v |= All (x,p) then (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Th3; hence J,v |= All (x,p) by Th19; ::_thesis: verum end; theorem :: VALUAT_1:21 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J) let A be non empty set ; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J) let J be interpretation of Al,A; ::_thesis: Valid (('not' ('not' p)),J) = Valid (p,J) now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_(Valid_(('not'_('not'_p)),J))_._v_=_(Valid_(p,J))_._v let v be Element of Valuations_in (Al,A); ::_thesis: (Valid (('not' ('not' p)),J)) . v = (Valid (p,J)) . v thus (Valid (('not' ('not' p)),J)) . v = 'not' ((Valid (('not' p),J)) . v) by Th10 .= 'not' ('not' ((Valid (p,J)) . v)) by Th10 .= (Valid (p,J)) . v ; ::_thesis: verum end; hence Valid (('not' ('not' p)),J) = Valid (p,J) by FUNCT_2:63; ::_thesis: verum end; theorem Th22: :: VALUAT_1:22 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J) let A be non empty set ; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J) let J be interpretation of Al,A; ::_thesis: Valid ((p '&' p),J) = Valid (p,J) now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_(Valid_((p_'&'_p),J))_._v_=_(Valid_(p,J))_._v let v be Element of Valuations_in (Al,A); ::_thesis: (Valid ((p '&' p),J)) . v = (Valid (p,J)) . v thus (Valid ((p '&' p),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (p,J)) . v) by Th12 .= (Valid (p,J)) . v ; ::_thesis: verum end; hence Valid ((p '&' p),J) = Valid (p,J) by FUNCT_2:63; ::_thesis: verum end; theorem Th23: :: VALUAT_1:23 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) let J be interpretation of Al,A; ::_thesis: ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) A1: now__::_thesis:_(_(_(Valid_(p,J))_._v_=_FALSE_or_(Valid_(q,J))_._v_=_TRUE_)_implies_J,v_|=_p_=>_q_) A2: now__::_thesis:_(_(Valid_(q,J))_._v_=_TRUE_implies_J,v_|=_p_=>_q_) assume A3: (Valid (q,J)) . v = TRUE ; ::_thesis: J,v |= p => q assume not J,v |= p => q ; ::_thesis: contradiction then (Valid ((p => q),J)) . v <> TRUE by Def7; then (Valid ((p => q),J)) . v = FALSE by XBOOLEAN:def_3; then (Valid (('not' (p '&' ('not' q))),J)) . v = FALSE by QC_LANG2:def_2; then 'not' ((Valid ((p '&' ('not' q)),J)) . v) = FALSE by Th10; then (Valid ((p '&' ('not' q)),J)) . v = TRUE by MARGREL1:11; then ((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v) = TRUE by Th12; then ((Valid (p,J)) . v) '&' ('not' ((Valid (q,J)) . v)) = TRUE by Th10; then 'not' ((Valid (q,J)) . v) = TRUE by MARGREL1:12; hence contradiction by A3, MARGREL1:11; ::_thesis: verum end; A4: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_J,v_|=_p_=>_q_) assume (Valid (p,J)) . v = FALSE ; ::_thesis: J,v |= p => q then ((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v) = FALSE by MARGREL1:12; then (Valid ((p '&' ('not' q)),J)) . v = FALSE by Th12; then 'not' ((Valid ((p '&' ('not' q)),J)) . v) = TRUE by MARGREL1:11; then (Valid (('not' (p '&' ('not' q))),J)) . v = TRUE by Th10; then (Valid ((p => q),J)) . v = TRUE by QC_LANG2:def_2; hence J,v |= p => q by Def7; ::_thesis: verum end; assume ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ; ::_thesis: J,v |= p => q hence J,v |= p => q by A4, A2; ::_thesis: verum end; now__::_thesis:_(_not_J,v_|=_p_=>_q_or_(Valid_(p,J))_._v_=_FALSE_or_(Valid_(q,J))_._v_=_TRUE_) assume J,v |= p => q ; ::_thesis: ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) then (Valid ((p => q),J)) . v = TRUE by Def7; then (Valid (('not' (p '&' ('not' q))),J)) . v = TRUE by QC_LANG2:def_2; then 'not' ((Valid ((p '&' ('not' q)),J)) . v) = TRUE by Th10; then (Valid ((p '&' ('not' q)),J)) . v = FALSE by MARGREL1:11; then ((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v) = FALSE by Th12; then ((Valid (p,J)) . v) '&' ('not' ((Valid (q,J)) . v)) = FALSE by Th10; then ( (Valid (p,J)) . v = FALSE or 'not' ((Valid (q,J)) . v) = FALSE ) by MARGREL1:12; hence ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) by MARGREL1:11; ::_thesis: verum end; hence ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) by A1; ::_thesis: verum end; theorem Th24: :: VALUAT_1:24 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) let J be interpretation of Al,A; ::_thesis: ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) hereby ::_thesis: ( ( J,v |= p implies J,v |= q ) implies J,v |= p => q ) assume J,v |= p => q ; ::_thesis: ( J,v |= p implies J,v |= q ) then ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) by Th23; hence ( J,v |= p implies J,v |= q ) by Def7; ::_thesis: verum end; assume ( J,v |= p implies J,v |= q ) ; ::_thesis: J,v |= p => q then ( (Valid (p,J)) . v = TRUE implies (Valid (q,J)) . v = TRUE ) by Def7; then ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) by XBOOLEAN:def_3; hence J,v |= p => q by Th23; ::_thesis: verum end; theorem Th25: :: VALUAT_1:25 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds p . v = TRUE proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds p . v = TRUE let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds p . v = TRUE let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds p . v = TRUE let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds p . v = TRUE let p be Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); ::_thesis: ( (FOR_ALL (x,p)) . v = TRUE implies p . v = TRUE ) for y being bound_QC-variable of Al st x <> y holds v . y = v . y ; hence ( (FOR_ALL (x,p)) . v = TRUE implies p . v = TRUE ) by Th3; ::_thesis: verum end; definition let Al be QC-alphabet ; let A be non empty set ; let J be interpretation of Al,A; let p be Element of CQC-WFF Al; predJ |= p means :Def8: :: VALUAT_1:def 8 for v being Element of Valuations_in (Al,A) holds J,v |= p; end; :: deftheorem Def8 defines |= VALUAT_1:def_8_:_ for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A for p being Element of CQC-WFF Al holds ( J |= p iff for v being Element of Valuations_in (Al,A) holds J,v |= p ); Lm2: for u, w, z being Element of BOOLEAN holds 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE proof let u, w, z be Element of BOOLEAN ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE percases ( ( z = TRUE & w = TRUE ) or ( w = FALSE & u = TRUE ) or u = FALSE or z = FALSE ) by XBOOLEAN:def_3; suppose ( z = TRUE & w = TRUE ) ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE then 'not' (w '&' z) = FALSE by MARGREL1:11; then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12; then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12; hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum end; supposethat A1: w = FALSE and A2: u = TRUE ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE 'not' w = TRUE by A1, MARGREL1:11; then 'not' (u '&' ('not' w)) = FALSE by A2, MARGREL1:11; then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12; hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum end; suppose u = FALSE ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE then u '&' z = FALSE by MARGREL1:12; then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12; then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12; hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum end; suppose z = FALSE ; ::_thesis: 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE then u '&' z = FALSE by MARGREL1:12; then ('not' (w '&' z)) '&' (u '&' z) = FALSE by MARGREL1:12; then ('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z)) = FALSE by MARGREL1:12; hence 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE by MARGREL1:11; ::_thesis: verum end; end; end; Lm3: now__::_thesis:_for_Al_being_QC-alphabet_ for_A_being_non_empty_set_ for_Y,_Z_being_bound_QC-variable_of_Al for_V1,_V2_being_Element_of_Valuations_in_(Al,A)_ex_v_being_Element_of_Valuations_in_(Al,A)_st_ (_(_for_x_being_bound_QC-variable_of_Al_st_x_<>_Y_holds_ v_._x_=_V1_._x_)_&_v_._Y_=_V2_._Z_) let Al be QC-alphabet ; ::_thesis: for A being non empty set for Y, Z being bound_QC-variable of Al for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st ( ( for x being bound_QC-variable of Al st x <> Y holds v . x = V1 . x ) & v . Y = V2 . Z ) let A be non empty set ; ::_thesis: for Y, Z being bound_QC-variable of Al for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st ( ( for x being bound_QC-variable of Al st x <> Y holds v . x = V1 . x ) & v . Y = V2 . Z ) let Y, Z be bound_QC-variable of Al; ::_thesis: for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st ( ( for x being bound_QC-variable of Al st x <> Y holds v . x = V1 . x ) & v . Y = V2 . Z ) let V1, V2 be Element of Valuations_in (Al,A); ::_thesis: ex v being Element of Valuations_in (Al,A) st ( ( for x being bound_QC-variable of Al st x <> Y holds v . x = V1 . x ) & v . Y = V2 . Z ) thus ex v being Element of Valuations_in (Al,A) st ( ( for x being bound_QC-variable of Al st x <> Y holds v . x = V1 . x ) & v . Y = V2 . Z ) ::_thesis: verum proof deffunc H1( set ) -> Element of A = V2 . Z; deffunc H2( set ) -> set = V1 . \$1; defpred S1[ set ] means for x1 being bound_QC-variable of Al st x1 = \$1 holds x1 <> Y; A1: for x being set st x in bound_QC-variables Al holds ( ( S1[x] implies H2(x) in A ) & ( not S1[x] implies H1(x) in A ) ) by FUNCT_2:5; consider f being Function of (bound_QC-variables Al),A such that A2: for x being set st x in bound_QC-variables Al holds ( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A1); ( dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def_1, RELAT_1:def_19; then reconsider f = f as Element of Valuations_in (Al,A) by FUNCT_2:def_2; take f ; ::_thesis: ( ( for x being bound_QC-variable of Al st x <> Y holds f . x = V1 . x ) & f . Y = V2 . Z ) now__::_thesis:_for_x_being_bound_QC-variable_of_Al_holds_ (_(_x_<>_Y_implies_f_._x_=_V1_._x_)_&_(_x_=_Y_implies_f_._Y_=_V2_._Z_)_) let x be bound_QC-variable of Al; ::_thesis: ( ( x <> Y implies f . x = V1 . x ) & ( x = Y implies f . Y = V2 . Z ) ) now__::_thesis:_(_x_<>_Y_implies_f_._x_=_V1_._x_) assume A3: x <> Y ; ::_thesis: f . x = V1 . x ( ( for x1 being bound_QC-variable of Al st x1 = x holds x1 <> Y ) implies f . x = V1 . x ) by A2; hence f . x = V1 . x by A3; ::_thesis: verum end; hence ( x <> Y implies f . x = V1 . x ) ; ::_thesis: ( x = Y implies f . Y = V2 . Z ) thus ( x = Y implies f . Y = V2 . Z ) by A2; ::_thesis: verum end; hence ( ( for x being bound_QC-variable of Al st x <> Y holds f . x = V1 . x ) & f . Y = V2 . Z ) ; ::_thesis: verum end; end; theorem :: VALUAT_1:26 for Al being QC-alphabet for A being non empty set for Y, Z being bound_QC-variable of Al for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st ( ( for x being bound_QC-variable of Al st x <> Y holds v . x = V1 . x ) & v . Y = V2 . Z ) by Lm3; theorem Th27: :: VALUAT_1:27 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A st not x in still_not-bound_in p holds for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A st not x in still_not-bound_in p holds for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A st not x in still_not-bound_in p holds for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w let x be bound_QC-variable of Al; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A st not x in still_not-bound_in p holds for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st not x in still_not-bound_in p holds for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w let J be interpretation of Al,A; ::_thesis: ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w ) defpred S1[ Element of CQC-WFF Al] means ( not x in still_not-bound_in \$1 implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (\$1,J)) . v = (Valid (\$1,J)) . w ); A1: now__::_thesis:_for_s,_t_being_Element_of_CQC-WFF_Al for_y_being_bound_QC-variable_of_Al for_k_being_Element_of_NAT_ for_ll_being_CQC-variable_list_of_k,Al for_P_being_QC-pred_symbol_of_k,Al_holds_ (_S1[_VERUM_Al]_&_S1[P_!_ll]_&_(_S1[s]_implies_S1[_'not'_s]_)_&_(_S1[s]_&_S1[t]_implies_S1[s_'&'_t]_)_&_(_S1[s]_implies_S1[_All_(y,s)]_)_) let s, t be Element of CQC-WFF Al; ::_thesis: for y being bound_QC-variable of Al for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) let y be bound_QC-variable of Al; ::_thesis: for k being Element of NAT for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) let ll be CQC-variable_list of k,Al; ::_thesis: for P being QC-pred_symbol of k,Al holds ( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) let P be QC-pred_symbol of k,Al; ::_thesis: ( S1[ VERUM Al] & S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) thus S1[ VERUM Al] ::_thesis: ( S1[P ! ll] & ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) proof assume not x in still_not-bound_in (VERUM Al) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w ::_thesis: verum proof let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w ) assume for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w (Valid ((VERUM Al),J)) . v = TRUE by Th5; hence (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w by Th5; ::_thesis: verum end; end; A2: rng ll c= bound_QC-variables Al by RELAT_1:def_19; thus S1[P ! ll] ::_thesis: ( ( S1[s] implies S1[ 'not' s] ) & ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) proof assume A3: not x in still_not-bound_in (P ! ll) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w ::_thesis: verum proof let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w ) assume A4: for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w A5: now__::_thesis:_(_(Valid_((P_!_ll),J))_._v_=_TRUE_implies_(Valid_((P_!_ll),J))_._v_=_(Valid_((P_!_ll),J))_._w_) A6: len (v *' ll) = k by Def3; A7: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(v_*'_ll)_holds_ (v_*'_ll)_._i_=_(w_*'_ll)_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i ) assume A8: ( 1 <= i & i <= len (v *' ll) ) ; ::_thesis: (v *' ll) . i = (w *' ll) . i A9: len (v *' ll) = len ll by A6, CARD_1:def_7; then i in dom ll by A8, FINSEQ_3:25; then ll . i in rng ll by FUNCT_1:def_3; then reconsider z = ll . i as bound_QC-variable of Al by A2; A10: i in NAT by ORDINAL1:def_12; ll . i <> x proof reconsider M = still_not-bound_in ll as set ; not x in M by A3, QC_LANG3:5; then not x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:2; then not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } by QC_LANG3:def_1; hence ll . i <> x by A8, A10, A9; ::_thesis: verum end; then A11: w . z = v . z by A4; (v *' ll) . i = v . (ll . i) by A6, A8, Def3; hence (v *' ll) . i = (w *' ll) . i by A6, A8, A11, Def3; ::_thesis: verum end; assume A12: (Valid ((P ! ll),J)) . v = TRUE ; ::_thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w then (ll 'in' (J . P)) . v = TRUE by Lm1; then A13: v *' ll in J . P by Def4; len (w *' ll) = k by Def3; then w *' ll in J . P by A13, A6, A7, FINSEQ_1:14; then (ll 'in' (J . P)) . w = TRUE by Def4; hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A12, Lm1; ::_thesis: verum end; now__::_thesis:_(_(Valid_((P_!_ll),J))_._v_=_FALSE_implies_(Valid_((P_!_ll),J))_._v_=_(Valid_((P_!_ll),J))_._w_) A14: len (v *' ll) = k by Def3; A15: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(v_*'_ll)_holds_ (v_*'_ll)_._i_=_(w_*'_ll)_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i ) assume A16: ( 1 <= i & i <= len (v *' ll) ) ; ::_thesis: (v *' ll) . i = (w *' ll) . i A17: len (v *' ll) = len ll by A14, CARD_1:def_7; then i in dom ll by A16, FINSEQ_3:25; then ll . i in rng ll by FUNCT_1:def_3; then reconsider z = ll . i as bound_QC-variable of Al by A2; ll . i <> x proof reconsider M = still_not-bound_in ll as set ; not x in M by A3, QC_LANG3:5; then not x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:2; then ( i in NAT & not x in { (ll . i2) where i2 is Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } ) by ORDINAL1:def_12, QC_LANG3:def_1; hence ll . i <> x by A16, A17; ::_thesis: verum end; then A18: w . z = v . z by A4; (v *' ll) . i = v . (ll . i) by A14, A16, Def3; hence (v *' ll) . i = (w *' ll) . i by A14, A16, A18, Def3; ::_thesis: verum end; assume A19: (Valid ((P ! ll),J)) . v = FALSE ; ::_thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w then (ll 'in' (J . P)) . v = FALSE by Lm1; then A20: not v *' ll in J . P by Def4; len (w *' ll) = k by Def3; then not w *' ll in J . P by A20, A14, A15, FINSEQ_1:14; then (ll 'in' (J . P)) . w = FALSE by Def4; hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A19, Lm1; ::_thesis: verum end; hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A5, XBOOLEAN:def_3; ::_thesis: verum end; end; thus ( S1[s] implies S1[ 'not' s] ) ::_thesis: ( ( S1[s] & S1[t] implies S1[s '&' t] ) & ( S1[s] implies S1[ All (y,s)] ) ) proof assume A21: ( ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (s,J)) . v = (Valid (s,J)) . w ) & not x in still_not-bound_in ('not' s) ) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w ::_thesis: verum proof let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w ) assume A22: for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w A23: now__::_thesis:_(_(Valid_(('not'_s),J))_._v_=_FALSE_implies_(Valid_(('not'_s),J))_._v_=_(Valid_(('not'_s),J))_._w_) assume A24: (Valid (('not' s),J)) . v = FALSE ; ::_thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w then 'not' ((Valid (s,J)) . v) = FALSE by Th10; then (Valid (s,J)) . v = TRUE by MARGREL1:11; then (Valid (s,J)) . w = TRUE by A21, A22, QC_LANG3:7; then 'not' ((Valid (s,J)) . w) = FALSE by MARGREL1:11; hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A24, Th10; ::_thesis: verum end; now__::_thesis:_(_(Valid_(('not'_s),J))_._v_=_TRUE_implies_(Valid_(('not'_s),J))_._v_=_(Valid_(('not'_s),J))_._w_) assume A25: (Valid (('not' s),J)) . v = TRUE ; ::_thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w then 'not' ((Valid (s,J)) . v) = TRUE by Th10; then (Valid (s,J)) . v = FALSE by MARGREL1:11; then (Valid (s,J)) . w = FALSE by A21, A22, QC_LANG3:7; then 'not' ((Valid (s,J)) . w) = TRUE by MARGREL1:11; hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A25, Th10; ::_thesis: verum end; hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A23, XBOOLEAN:def_3; ::_thesis: verum end; end; thus ( S1[s] & S1[t] implies S1[s '&' t] ) ::_thesis: ( S1[s] implies S1[ All (y,s)] ) proof assume that A26: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (s,J)) . v = (Valid (s,J)) . w ) and A27: ( not x in still_not-bound_in t implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (t,J)) . v = (Valid (t,J)) . w ) and A28: not x in still_not-bound_in (s '&' t) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w A29: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A28, QC_LANG3:10; thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w ::_thesis: verum proof let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w ) assume A30: for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w A31: now__::_thesis:_(_(Valid_((s_'&'_t),J))_._v_=_FALSE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_) assume A32: (Valid ((s '&' t),J)) . v = FALSE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w A33: now__::_thesis:_(_(Valid_(s,J))_._v_=_FALSE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_) assume (Valid (s,J)) . v = FALSE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w then (Valid (s,J)) . w = FALSE by A26, A29, A30, XBOOLE_0:def_3; then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE by MARGREL1:12; hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A32, Th12; ::_thesis: verum end; A34: now__::_thesis:_(_(Valid_(t,J))_._v_=_FALSE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_) assume (Valid (t,J)) . v = FALSE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w then (Valid (t,J)) . w = FALSE by A27, A29, A30, XBOOLE_0:def_3; then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE by MARGREL1:12; hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A32, Th12; ::_thesis: verum end; ((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = FALSE by A32, Th12; hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A33, A34, MARGREL1:12; ::_thesis: verum end; now__::_thesis:_(_(Valid_((s_'&'_t),J))_._v_=_TRUE_implies_(Valid_((s_'&'_t),J))_._v_=_(Valid_((s_'&'_t),J))_._w_) assume A35: (Valid ((s '&' t),J)) . v = TRUE ; ::_thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w then A36: ((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = TRUE by Th12; then (Valid (t,J)) . v = TRUE by MARGREL1:12; then A37: (Valid (t,J)) . w = TRUE by A27, A29, A30, XBOOLE_0:def_3; (Valid (s,J)) . v = TRUE by A36, MARGREL1:12; then (Valid (s,J)) . w = TRUE by A26, A29, A30, XBOOLE_0:def_3; then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = TRUE by A37; hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A35, Th12; ::_thesis: verum end; hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A31, XBOOLEAN:def_3; ::_thesis: verum end; end; thus ( S1[s] implies S1[ All (y,s)] ) ::_thesis: verum proof assume that A38: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (s,J)) . v = (Valid (s,J)) . w ) and A39: not x in still_not-bound_in (All (y,s)) ; ::_thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w A40: not x in (still_not-bound_in s) \ {y} by A39, QC_LANG3:12; thus for v, w being Element of Valuations_in (Al,A) st ( for z being bound_QC-variable of Al st x <> z holds w . z = v . z ) holds (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w ::_thesis: verum proof let v, w be Element of Valuations_in (Al,A); ::_thesis: ( ( for z being bound_QC-variable of Al st x <> z holds w . z = v . z ) implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w ) assume A41: for z being bound_QC-variable of Al st x <> z holds w . z = v . z ; ::_thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w A42: now__::_thesis:_(_(Valid_((All_(y,s)),J))_._v_=_FALSE_implies_(Valid_((All_(y,s)),J))_._v_=_(Valid_((All_(y,s)),J))_._w_) assume A43: (Valid ((All (y,s)),J)) . v = FALSE ; ::_thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w then (FOR_ALL (y,(Valid (s,J)))) . v = FALSE by Lm1; then consider v1 being Element of Valuations_in (Al,A) such that A44: (Valid (s,J)) . v1 = FALSE and A45: for z being bound_QC-variable of Al st y <> z holds v1 . z = v . z by Th2; A46: now__::_thesis:_(_not_x_in_still_not-bound_in_s_implies_ex_v2_being_Element_of_Valuations_in_(Al,A)_st_ (_(Valid_(s,J))_._v2_=_FALSE_&_(_for_z_being_bound_QC-variable_of_Al_st_y_<>_z_holds_ v2_._z_=_w_._z_)_)_) assume A47: not x in still_not-bound_in s ; ::_thesis: ex v2 being Element of Valuations_in (Al,A) st ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z ) ) consider v2 being Element of Valuations_in (Al,A) such that A48: ( ( for z being bound_QC-variable of Al st z <> y holds v2 . z = w . z ) & v2 . y = v1 . y ) by Lm3; take v2 = v2; ::_thesis: ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z ) ) for z being bound_QC-variable of Al st x <> z holds v2 . z = v1 . z proof let z be bound_QC-variable of Al; ::_thesis: ( x <> z implies v2 . z = v1 . z ) assume A49: x <> z ; ::_thesis: v2 . z = v1 . z now__::_thesis:_(_z_<>_y_implies_v2_._z_=_v1_._z_) assume A50: z <> y ; ::_thesis: v2 . z = v1 . z hence v2 . z = w . z by A48 .= v . z by A41, A49 .= v1 . z by A45, A50 ; ::_thesis: verum end; hence v2 . z = v1 . z by A48; ::_thesis: verum end; hence (Valid (s,J)) . v2 = FALSE by A38, A44, A47; ::_thesis: for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z thus for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z by A48; ::_thesis: verum end; now__::_thesis:_(_x_in_{y}_implies_ex_v2_being_Element_of_Valuations_in_(Al,A)_st_ (_(Valid_(s,J))_._v2_=_FALSE_&_(_for_z_being_bound_QC-variable_of_Al_st_y_<>_z_holds_ v2_._z_=_w_._z_)_)_) assume A51: x in {y} ; ::_thesis: ex v2 being Element of Valuations_in (Al,A) st ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z ) ) take v2 = v1; ::_thesis: ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z ) ) thus (Valid (s,J)) . v2 = FALSE by A44; ::_thesis: for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z for z being bound_QC-variable of Al st y <> z holds v1 . z = w . z proof let z be bound_QC-variable of Al; ::_thesis: ( y <> z implies v1 . z = w . z ) assume A52: y <> z ; ::_thesis: v1 . z = w . z then A53: x <> z by A51, TARSKI:def_1; thus v1 . z = v . z by A45, A52 .= w . z by A41, A53 ; ::_thesis: verum end; hence for z being bound_QC-variable of Al st y <> z holds v2 . z = w . z ; ::_thesis: verum end; then (FOR_ALL (y,(Valid (s,J)))) . w = FALSE by A40, A46, Th2, XBOOLE_0:def_5; hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A43, Lm1; ::_thesis: verum end; now__::_thesis:_(_(Valid_((All_(y,s)),J))_._v_=_TRUE_implies_(Valid_((All_(y,s)),J))_._v_=_(Valid_((All_(y,s)),J))_._w_) assume A54: (Valid ((All (y,s)),J)) . v = TRUE ; ::_thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w then A55: (FOR_ALL (y,(Valid (s,J)))) . v = TRUE by Lm1; for v1 being Element of Valuations_in (Al,A) st ( for z being bound_QC-variable of Al st y <> z holds v1 . z = w . z ) holds (Valid (s,J)) . v1 = TRUE proof let v1 be Element of Valuations_in (Al,A); ::_thesis: ( ( for z being bound_QC-variable of Al st y <> z holds v1 . z = w . z ) implies (Valid (s,J)) . v1 = TRUE ) assume A56: for z being bound_QC-variable of Al st y <> z holds v1 . z = w . z ; ::_thesis: (Valid (s,J)) . v1 = TRUE A57: now__::_thesis:_(_not_x_in_still_not-bound_in_s_implies_(Valid_(s,J))_._v1_=_TRUE_) assume A58: not x in still_not-bound_in s ; ::_thesis: (Valid (s,J)) . v1 = TRUE consider v2 being Element of Valuations_in (Al,A) such that A59: ( ( for z being bound_QC-variable of Al st z <> y holds v2 . z = v . z ) & v2 . y = v1 . y ) by Lm3; A60: for z being bound_QC-variable of Al st x <> z holds v2 . z = v1 . z proof let z be bound_QC-variable of Al; ::_thesis: ( x <> z implies v2 . z = v1 . z ) assume A61: x <> z ; ::_thesis: v2 . z = v1 . z now__::_thesis:_(_z_<>_y_implies_v2_._z_=_v1_._z_) assume A62: z <> y ; ::_thesis: v2 . z = v1 . z hence v2 . z = v . z by A59 .= w . z by A41, A61 .= v1 . z by A56, A62 ; ::_thesis: verum end; hence v2 . z = v1 . z by A59; ::_thesis: verum end; (Valid (s,J)) . v2 = TRUE by A55, A59, Th3; hence (Valid (s,J)) . v1 = TRUE by A38, A58, A60; ::_thesis: verum end; now__::_thesis:_(_x_in_{y}_implies_(Valid_(s,J))_._v1_=_TRUE_) assume x in {y} ; ::_thesis: (Valid (s,J)) . v1 = TRUE then A63: x = y by TARSKI:def_1; for z being bound_QC-variable of Al st y <> z holds v1 . z = v . z proof let z be bound_QC-variable of Al; ::_thesis: ( y <> z implies v1 . z = v . z ) assume A64: y <> z ; ::_thesis: v1 . z = v . z hence v . z = w . z by A41, A63 .= v1 . z by A56, A64 ; ::_thesis: verum end; hence (Valid (s,J)) . v1 = TRUE by A55, Th3; ::_thesis: verum end; hence (Valid (s,J)) . v1 = TRUE by A40, A57, XBOOLE_0:def_5; ::_thesis: verum end; then (FOR_ALL (y,(Valid (s,J)))) . w = TRUE by Th3; hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A54, Lm1; ::_thesis: verum end; hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A42, XBOOLEAN:def_3; ::_thesis: verum end; end; end; for s being Element of CQC-WFF Al holds S1[s] from CQC_LANG:sch_1(A1); hence ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w ) ; ::_thesis: verum end; theorem Th28: :: VALUAT_1:28 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p let J be interpretation of Al,A; ::_thesis: ( J,v |= p & not x in still_not-bound_in p implies for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) assume that A1: J,v |= p and A2: not x in still_not-bound_in p ; ::_thesis: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p now__::_thesis:_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ w_._y_=_v_._y_)_holds_ J,w_|=_p let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies J,w |= p ) assume A3: for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: J,w |= p (Valid (p,J)) . v = TRUE by A1, Def7; then (Valid (p,J)) . w = TRUE by A2, A3, Th27; hence J,w |= p by Def7; ::_thesis: verum end; hence for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ; ::_thesis: verum end; theorem Th29: :: VALUAT_1:29 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) let J be interpretation of Al,A; ::_thesis: ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) A1: now__::_thesis:_(_(_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ w_._y_=_v_._y_)_holds_ J,w_|=_p_)_implies_J,v_|=_All_(x,p)_) assume A2: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ; ::_thesis: J,v |= All (x,p) for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . w = TRUE proof let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies (Valid (p,J)) . w = TRUE ) assume for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: (Valid (p,J)) . w = TRUE then J,w |= p by A2; hence (Valid (p,J)) . w = TRUE by Def7; ::_thesis: verum end; hence J,v |= All (x,p) by Th20; ::_thesis: verum end; now__::_thesis:_(_J,v_|=_All_(x,p)_implies_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ w_._y_=_v_._y_)_holds_ J,w_|=_p_) assume A3: J,v |= All (x,p) ; ::_thesis: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) implies J,w |= p ) assume for y being bound_QC-variable of Al st x <> y holds w . y = v . y ; ::_thesis: J,w |= p then (Valid (p,J)) . w = TRUE by A3, Th20; hence J,w |= p by Def7; ::_thesis: verum end; hence ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) by A1; ::_thesis: verum end; theorem Th30: :: VALUAT_1:30 for Al being QC-alphabet for A being non empty set for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let A be non empty set ; ::_thesis: for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let J be interpretation of Al,A; ::_thesis: for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let s9 be QC-formula of Al; ::_thesis: ( x <> y & p = s9 . x & q = s9 . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) defpred S1[ Element of QC-WFF Al] means for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = \$1 . x & q = \$1 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v; A1: now__::_thesis:_for_s_being_Element_of_QC-WFF_Al_holds_ (_(_s_is_atomic_implies_S1[s]_)_&_S1[_VERUM_Al]_&_(_s_is_negative_&_S1[_the_argument_of_s]_implies_S1[s]_)_&_(_s_is_conjunctive_&_S1[_the_left_argument_of_s]_&_S1[_the_right_argument_of_s]_implies_S1[s]_)_&_(_s_is_universal_&_S1[_the_scope_of_s]_implies_S1[s]_)_) let s be Element of QC-WFF Al; ::_thesis: ( ( s is atomic implies S1[s] ) & S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) thus ( s is atomic implies S1[s] ) ::_thesis: ( S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) proof assume A2: s is atomic ; ::_thesis: S1[s] thus for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum proof consider k being Element of NAT , P being QC-pred_symbol of k,Al, l being QC-variable_list of k,Al such that A3: s = P ! l by A2, QC_LANG1:def_18; let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) assume that x <> y and A4: p = s . x and A5: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v set lx = Subst (l,((Al a. 0) .--> x)); set ly = Subst (l,((Al a. 0) .--> y)); let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v ) assume A6: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v A7: p = P ! (Subst (l,((Al a. 0) .--> x))) by A4, A3, CQC_LANG:17; then A8: { ((Subst (l,((Al a. 0) .--> x))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((Al a. 0) .--> x))) & (Subst (l,((Al a. 0) .--> x))) . i in free_QC-variables Al ) } = {} by CQC_LANG:7; A9: q = P ! (Subst (l,((Al a. 0) .--> y))) by A5, A3, CQC_LANG:17; then A10: { ((Subst (l,((Al a. 0) .--> y))) . i) where i is Element of NAT : ( 1 <= i & i <= len (Subst (l,((Al a. 0) .--> y))) & (Subst (l,((Al a. 0) .--> y))) . i in free_QC-variables Al ) } = {} by CQC_LANG:7; A11: { ((Subst (l,((Al a. 0) .--> y))) . j) where j is Element of NAT : ( 1 <= j & j <= len (Subst (l,((Al a. 0) .--> y))) & (Subst (l,((Al a. 0) .--> y))) . j in fixed_QC-variables Al ) } = {} by A9, CQC_LANG:7; { ((Subst (l,((Al a. 0) .--> x))) . j) where j is Element of NAT : ( 1 <= j & j <= len (Subst (l,((Al a. 0) .--> x))) & (Subst (l,((Al a. 0) .--> x))) . j in fixed_QC-variables Al ) } = {} by A7, CQC_LANG:7; then reconsider lx = Subst (l,((Al a. 0) .--> x)), ly = Subst (l,((Al a. 0) .--> y)) as CQC-variable_list of k,Al by A8, A10, A11, CQC_LANG:5; A12: len (v *' lx) = k by Def3; A13: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_(v_*'_lx)_holds_ (v_*'_lx)_._i_=_(v_*'_ly)_._i let i be Nat; ::_thesis: ( 1 <= i & i <= len (v *' lx) implies (v *' lx) . i = (v *' ly) . i ) assume that A14: 1 <= i and A15: i <= len (v *' lx) ; ::_thesis: (v *' lx) . i = (v *' ly) . i A16: i in NAT by ORDINAL1:def_12; A17: i <= len l by A12, A15, CARD_1:def_7; A18: now__::_thesis:_(_l_._i_<>_Al_a._0_implies_(v_*'_lx)_._i_=_(v_*'_ly)_._i_) assume l . i <> Al a. 0 ; ::_thesis: (v *' lx) . i = (v *' ly) . i then A19: ( lx . i = l . i & ly . i = l . i ) by A14, A17, A16, CQC_LANG:3; v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def3; hence (v *' lx) . i = (v *' ly) . i by A12, A14, A15, A19, Def3; ::_thesis: verum end; now__::_thesis:_(_l_._i_=_Al_a._0_implies_(v_*'_lx)_._i_=_(v_*'_ly)_._i_) assume l . i = Al a. 0 ; ::_thesis: (v *' lx) . i = (v *' ly) . i then A20: ( lx . i = x & ly . i = y ) by A14, A17, A16, CQC_LANG:3; v . (lx . i) = (v *' lx) . i by A12, A14, A15, Def3; hence (v *' lx) . i = (v *' ly) . i by A6, A12, A14, A15, A20, Def3; ::_thesis: verum end; hence (v *' lx) . i = (v *' ly) . i by A18; ::_thesis: verum end; len (v *' ly) = k by Def3; then A21: v *' lx = v *' ly by A12, A13, FINSEQ_1:14; A22: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(q,J))_._v_=_FALSE_) assume (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (q,J)) . v = FALSE then not v *' lx in J . P by A7, Th8; hence (Valid (q,J)) . v = FALSE by A9, A21, Th8; ::_thesis: verum end; now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_) assume (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE then v *' lx in J . P by A7, Th7; hence (Valid (q,J)) . v = TRUE by A9, A21, Th7; ::_thesis: verum end; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A22, XBOOLEAN:def_3; ::_thesis: verum end; end; thus S1[ VERUM Al] ::_thesis: ( ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) proof let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = (VERUM Al) . x & q = (VERUM Al) . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = (VERUM Al) . x & q = (VERUM Al) . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) assume that x <> y and A23: p = (VERUM Al) . x and A24: q = (VERUM Al) . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v ) assume v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v p = VERUM Al by A23, CQC_LANG:15; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A24, CQC_LANG:15; ::_thesis: verum end; thus ( s is negative & S1[ the_argument_of s] implies S1[s] ) ::_thesis: ( ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) proof assume that A25: s is negative and A26: for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = (the_argument_of s) . x & q = (the_argument_of s) . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ; ::_thesis: S1[s] thus for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum proof let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) assume that x <> y and A27: p = s . x and A28: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v A29: s . y = 'not' ((the_argument_of s) . y) by A25, CQC_LANG:18; then reconsider qa = (the_argument_of s) . y as Element of CQC-WFF Al by A28, CQC_LANG:8; A30: s . x = 'not' ((the_argument_of s) . x) by A25, CQC_LANG:18; then reconsider pa = (the_argument_of s) . x as Element of CQC-WFF Al by A27, CQC_LANG:8; let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v ) assume A31: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v A32: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(q,J))_._v_=_FALSE_) assume (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (q,J)) . v = FALSE then 'not' ((Valid (pa,J)) . v) = FALSE by A27, A30, Th10; then (Valid (pa,J)) . v = TRUE by MARGREL1:11; then (Valid (qa,J)) . v = TRUE by A26, A31; then 'not' ((Valid (qa,J)) . v) = FALSE by MARGREL1:11; hence (Valid (q,J)) . v = FALSE by A28, A29, Th10; ::_thesis: verum end; now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_) assume (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE then 'not' ((Valid (pa,J)) . v) = TRUE by A27, A30, Th10; then (Valid (pa,J)) . v = FALSE by MARGREL1:11; then (Valid (qa,J)) . v = FALSE by A26, A31; then 'not' ((Valid (qa,J)) . v) = TRUE by MARGREL1:11; hence (Valid (q,J)) . v = TRUE by A28, A29, Th10; ::_thesis: verum end; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A32, XBOOLEAN:def_3; ::_thesis: verum end; end; thus ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) ::_thesis: ( s is universal & S1[ the_scope_of s] implies S1[s] ) proof assume that A33: s is conjunctive and A34: for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = (the_left_argument_of s) . x & q = (the_left_argument_of s) . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v and A35: for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = (the_right_argument_of s) . x & q = (the_right_argument_of s) . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ; ::_thesis: S1[s] thus for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum proof let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) assume that x <> y and A36: p = s . x and A37: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v A38: s . x = ((the_left_argument_of s) . x) '&' ((the_right_argument_of s) . x) by A33, CQC_LANG:20; then reconsider pla = (the_left_argument_of s) . x, pra = (the_right_argument_of s) . x as Element of CQC-WFF Al by A36, CQC_LANG:9; A39: s . y = ((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y) by A33, CQC_LANG:20; then reconsider qla = (the_left_argument_of s) . y, qra = (the_right_argument_of s) . y as Element of CQC-WFF Al by A37, CQC_LANG:9; let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v ) assume A40: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v A41: now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume A42: (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v A43: now__::_thesis:_(_(Valid_(pla,J))_._v_=_FALSE_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume (Valid (pla,J)) . v = FALSE ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v then (Valid (qla,J)) . v = FALSE by A34, A40; then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:12; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A37, A39, A42, Th12; ::_thesis: verum end; A44: now__::_thesis:_(_(Valid_(pra,J))_._v_=_FALSE_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume (Valid (pra,J)) . v = FALSE ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v then (Valid (qra,J)) . v = FALSE by A35, A40; then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = FALSE by MARGREL1:12; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A37, A39, A42, Th12; ::_thesis: verum end; ((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = FALSE by A36, A38, A42, Th12; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A43, A44, MARGREL1:12; ::_thesis: verum end; now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_) assume (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE then A45: ((Valid (pla,J)) . v) '&' ((Valid (pra,J)) . v) = TRUE by A36, A38, Th12; then (Valid (pra,J)) . v = TRUE by MARGREL1:12; then A46: (Valid (qra,J)) . v = TRUE by A35, A40; (Valid (pla,J)) . v = TRUE by A45, MARGREL1:12; then (Valid (qla,J)) . v = TRUE by A34, A40; then ((Valid (qla,J)) . v) '&' ((Valid (qra,J)) . v) = TRUE by A46; hence (Valid (q,J)) . v = TRUE by A37, A39, Th12; ::_thesis: verum end; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A41, XBOOLEAN:def_3; ::_thesis: verum end; end; thus ( s is universal & S1[ the_scope_of s] implies S1[s] ) ::_thesis: verum proof assume that A47: s is universal and A48: for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = (the_scope_of s) . x & q = (the_scope_of s) . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ; ::_thesis: S1[s] consider xx being bound_QC-variable of Al, pp being Element of QC-WFF Al such that A49: s = All (xx,pp) by A47, QC_LANG1:def_21; A50: xx = bound_in s by A47, A49, QC_LANG1:def_27; thus for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ::_thesis: verum proof let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al st x <> y & p = s . x & q = s . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let p, q be Element of CQC-WFF Al; ::_thesis: ( x <> y & p = s . x & q = s . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) assume that x <> y and A51: p = s . x and A52: q = s . y ; ::_thesis: for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v let v be Element of Valuations_in (Al,A); ::_thesis: ( v . x = v . y implies (Valid (p,J)) . v = (Valid (q,J)) . v ) assume A53: v . x = v . y ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v A54: now__::_thesis:_(_x_<>_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume A55: x <> bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v then s . x = All ((bound_in s),((the_scope_of s) . x)) by A47, CQC_LANG:23; then reconsider ps = (the_scope_of s) . x as Element of CQC-WFF Al by A51, CQC_LANG:13; A56: All ((bound_in s),ps) = p by A47, A51, A55, CQC_LANG:23; A57: now__::_thesis:_(_y_<>_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume A58: y <> bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v then s . y = All ((bound_in s),((the_scope_of s) . y)) by A47, CQC_LANG:23; then reconsider qs = (the_scope_of s) . y as Element of CQC-WFF Al by A52, CQC_LANG:13; A59: Valid ((All ((bound_in s),qs)),J) = FOR_ALL ((bound_in s),(Valid (qs,J))) by Lm1; A60: Valid ((All ((bound_in s),ps)),J) = FOR_ALL ((bound_in s),(Valid (ps,J))) by Lm1; A61: All ((bound_in s),qs) = q by A47, A52, A58, CQC_LANG:23; A62: now__::_thesis:_(_(Valid_(p,J))_._v_=_TRUE_implies_(Valid_(q,J))_._v_=_TRUE_) assume A63: (Valid (p,J)) . v = TRUE ; ::_thesis: (Valid (q,J)) . v = TRUE for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st bound_in s <> y holds v1 . y = v . y ) holds (Valid (qs,J)) . v1 = TRUE proof let v1 be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st bound_in s <> y holds v1 . y = v . y ) implies (Valid (qs,J)) . v1 = TRUE ) assume A64: for y being bound_QC-variable of Al st bound_in s <> y holds v1 . y = v . y ; ::_thesis: (Valid (qs,J)) . v1 = TRUE then A65: ( v1 . x = v . x & v1 . y = v . y ) by A55, A58; (Valid (ps,J)) . v1 = TRUE by A56, A60, A63, A64, Th3; hence (Valid (qs,J)) . v1 = TRUE by A48, A53, A65; ::_thesis: verum end; hence (Valid (q,J)) . v = TRUE by A61, A59, Th3; ::_thesis: verum end; now__::_thesis:_(_(Valid_(p,J))_._v_=_FALSE_implies_(Valid_(q,J))_._v_=_FALSE_) assume A66: (Valid (p,J)) . v = FALSE ; ::_thesis: (Valid (q,J)) . v = FALSE ex v1 being Element of Valuations_in (Al,A) st ( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable of Al st bound_in s <> y holds v1 . y = v . y ) ) proof consider v1 being Element of Valuations_in (Al,A) such that A67: (Valid (ps,J)) . v1 = FALSE and A68: for y being bound_QC-variable of Al st bound_in s <> y holds v1 . y = v . y by A56, A60, A66, Th2; ( v1 . x = v . x & v1 . y = v . y ) by A55, A58, A68; then (Valid (qs,J)) . v1 = FALSE by A48, A53, A67; hence ex v1 being Element of Valuations_in (Al,A) st ( (Valid (qs,J)) . v1 = FALSE & ( for y being bound_QC-variable of Al st bound_in s <> y holds v1 . y = v . y ) ) by A68; ::_thesis: verum end; hence (Valid (q,J)) . v = FALSE by A61, A59, Th2; ::_thesis: verum end; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A62, XBOOLEAN:def_3; ::_thesis: verum end; now__::_thesis:_(_y_=_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume A69: y = bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v then q = All (y,pp) by A49, A50, A52, CQC_LANG:24; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A49, A50, A51, A69, CQC_LANG:27; ::_thesis: verum end; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A57; ::_thesis: verum end; now__::_thesis:_(_x_=_bound_in_s_implies_(Valid_(p,J))_._v_=_(Valid_(q,J))_._v_) assume A70: x = bound_in s ; ::_thesis: (Valid (p,J)) . v = (Valid (q,J)) . v then p = All (x,pp) by A49, A50, A51, CQC_LANG:24; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A49, A50, A52, A70, CQC_LANG:27; ::_thesis: verum end; hence (Valid (p,J)) . v = (Valid (q,J)) . v by A54; ::_thesis: verum end; end; end; for s being Element of QC-WFF Al holds S1[s] from QC_LANG1:sch_2(A1); hence ( x <> y & p = s9 . x & q = s9 . y implies for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v ) ; ::_thesis: verum end; theorem Th31: :: VALUAT_1:31 for Al being QC-alphabet for x, y being bound_QC-variable of Al for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds not x in still_not-bound_in (s9 . y) proof let Al be QC-alphabet ; ::_thesis: for x, y being bound_QC-variable of Al for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds not x in still_not-bound_in (s9 . y) let x, y be bound_QC-variable of Al; ::_thesis: for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds not x in still_not-bound_in (s9 . y) let s9 be QC-formula of Al; ::_thesis: ( x <> y & not x in still_not-bound_in s9 implies not x in still_not-bound_in (s9 . y) ) defpred S1[ Element of QC-WFF Al] means ( x <> y & not x in still_not-bound_in \$1 implies not x in still_not-bound_in (\$1 . y) ); A1: now__::_thesis:_for_s_being_Element_of_QC-WFF_Al_holds_ (_(_s_is_atomic_implies_S1[s]_)_&_S1[_VERUM_Al]_&_(_s_is_negative_&_S1[_the_argument_of_s]_implies_S1[s]_)_&_(_s_is_conjunctive_&_S1[_the_left_argument_of_s]_&_S1[_the_right_argument_of_s]_implies_S1[s]_)_&_(_s_is_universal_&_S1[_the_scope_of_s]_implies_S1[s]_)_) let s be Element of QC-WFF Al; ::_thesis: ( ( s is atomic implies S1[s] ) & S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) thus ( s is atomic implies S1[s] ) ::_thesis: ( S1[ VERUM Al] & ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) proof assume that A2: s is atomic and A3: x <> y and A4: not x in still_not-bound_in s ; ::_thesis: not x in still_not-bound_in (s . y) thus not x in still_not-bound_in (s . y) ::_thesis: verum proof set l = the_arguments_of s; set ll = Subst ((the_arguments_of s),((Al a. 0) .--> y)); A5: still_not-bound_in s = still_not-bound_in (the_arguments_of s) by A2, QC_LANG3:4 .= variables_in ((the_arguments_of s),(bound_QC-variables Al)) by QC_LANG3:2 .= { ((the_arguments_of s) . k) where k is Element of NAT : ( 1 <= k & k <= len (the_arguments_of s) & (the_arguments_of s) . k in bound_QC-variables Al ) } by QC_LANG3:def_1 ; A6: ( x in { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } implies x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } ) proof assume x in { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } ; ::_thesis: x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } then consider k being Element of NAT such that A7: x = (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k and A8: 1 <= k and A9: k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) and (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ; A10: k <= len (the_arguments_of s) by A9, CQC_LANG:def_1; then x = (the_arguments_of s) . k by A3, A7, A8, CQC_LANG:3; hence x in { ((the_arguments_of s) . i) where i is Element of NAT : ( 1 <= i & i <= len (the_arguments_of s) & (the_arguments_of s) . i in bound_QC-variables Al ) } by A8, A10; ::_thesis: verum end; A11: s . y = (the_pred_symbol_of s) ! (Subst ((the_arguments_of s),((Al a. 0) .--> y))) by A2, CQC_LANG:16; A12: ( s . y is atomic & the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y)) ) proof consider k being Element of NAT , p being QC-pred_symbol of k,Al, l2 being QC-variable_list of k,Al such that A13: s = p ! l2 by A2, QC_LANG1:def_18; l2 = the_arguments_of s by A2, A13, QC_LANG1:def_23; then reconsider l3 = Subst ((the_arguments_of s),((Al a. 0) .--> y)) as QC-variable_list of k,Al ; A14: s . y = p ! l3 by A2, A11, A13, QC_LANG1:def_22; hence s . y is atomic by QC_LANG1:def_18; ::_thesis: the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y)) hence the_arguments_of (s . y) = Subst ((the_arguments_of s),((Al a. 0) .--> y)) by A14, QC_LANG1:def_23; ::_thesis: verum end; then still_not-bound_in (the_arguments_of (s . y)) = variables_in ((Subst ((the_arguments_of s),((Al a. 0) .--> y))),(bound_QC-variables Al)) by QC_LANG3:2 .= { ((Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k) where k is Element of NAT : ( 1 <= k & k <= len (Subst ((the_arguments_of s),((Al a. 0) .--> y))) & (Subst ((the_arguments_of s),((Al a. 0) .--> y))) . k in bound_QC-variables Al ) } by QC_LANG3:def_1 ; hence not x in still_not-bound_in (s . y) by A4, A5, A12, A6, QC_LANG3:4; ::_thesis: verum end; end; thus S1[ VERUM Al] by CQC_LANG:15; ::_thesis: ( ( s is negative & S1[ the_argument_of s] implies S1[s] ) & ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) thus ( s is negative & S1[ the_argument_of s] implies S1[s] ) ::_thesis: ( ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) & ( s is universal & S1[ the_scope_of s] implies S1[s] ) ) proof assume that A15: s is negative and A16: ( ( x <> y & not x in still_not-bound_in (the_argument_of s) implies not x in still_not-bound_in ((the_argument_of s) . y) ) & x <> y & not x in still_not-bound_in s ) ; ::_thesis: not x in still_not-bound_in (s . y) not x in still_not-bound_in ('not' ((the_argument_of s) . y)) by A15, A16, QC_LANG3:6, QC_LANG3:7; hence not x in still_not-bound_in (s . y) by A15, CQC_LANG:18; ::_thesis: verum end; thus ( s is conjunctive & S1[ the_left_argument_of s] & S1[ the_right_argument_of s] implies S1[s] ) ::_thesis: ( s is universal & S1[ the_scope_of s] implies S1[s] ) proof assume that A17: s is conjunctive and A18: ( ( x <> y & not x in still_not-bound_in (the_left_argument_of s) implies not x in still_not-bound_in ((the_left_argument_of s) . y) ) & ( x <> y & not x in still_not-bound_in (the_right_argument_of s) implies not x in still_not-bound_in ((the_right_argument_of s) . y) ) & x <> y & not x in still_not-bound_in s ) ; ::_thesis: not x in still_not-bound_in (s . y) still_not-bound_in s = (still_not-bound_in (the_left_argument_of s)) \/ (still_not-bound_in (the_right_argument_of s)) by A17, QC_LANG3:9; then not x in (still_not-bound_in ((the_left_argument_of s) . y)) \/ (still_not-bound_in ((the_right_argument_of s) . y)) by A18, XBOOLE_0:def_3; then not x in still_not-bound_in (((the_left_argument_of s) . y) '&' ((the_right_argument_of s) . y)) by QC_LANG3:10; hence not x in still_not-bound_in (s . y) by A17, CQC_LANG:20; ::_thesis: verum end; thus ( s is universal & S1[ the_scope_of s] implies S1[s] ) ::_thesis: verum proof assume that A19: s is universal and A20: ( x <> y & not x in still_not-bound_in (the_scope_of s) implies not x in still_not-bound_in ((the_scope_of s) . y) ) and A21: x <> y and A22: not x in still_not-bound_in s ; ::_thesis: not x in still_not-bound_in (s . y) A23: still_not-bound_in s = (still_not-bound_in (the_scope_of s)) \ {(bound_in s)} by A19, QC_LANG3:11; thus not x in still_not-bound_in (s . y) ::_thesis: verum proof A24: now__::_thesis:_(_x_in_{(bound_in_s)}_implies_not_x_in_still_not-bound_in_(s_._y)_) still_not-bound_in (All (x,((the_scope_of s) . y))) = (still_not-bound_in ((the_scope_of s) . y)) \ {x} by QC_LANG3:12; then A25: ( ( not x in still_not-bound_in ((the_scope_of s) . y) or x in {x} ) iff not x in still_not-bound_in (All (x,((the_scope_of s) . y))) ) by XBOOLE_0:def_5; assume x in {(bound_in s)} ; ::_thesis: not x in still_not-bound_in (s . y) then x = bound_in s by TARSKI:def_1; hence not x in still_not-bound_in (s . y) by A19, A21, A25, CQC_LANG:23, TARSKI:def_1; ::_thesis: verum end; now__::_thesis:_(_not_x_in_still_not-bound_in_(the_scope_of_s)_implies_not_x_in_still_not-bound_in_(s_._y)_) assume not x in still_not-bound_in (the_scope_of s) ; ::_thesis: not x in still_not-bound_in (s . y) then not x in (still_not-bound_in ((the_scope_of s) . y)) \ {(bound_in s)} by A20, A21, XBOOLE_0:def_5; then not x in still_not-bound_in (All ((bound_in s),((the_scope_of s) . y))) by QC_LANG3:12; hence not x in still_not-bound_in (s . y) by A19, A22, CQC_LANG:22, CQC_LANG:23; ::_thesis: verum end; hence not x in still_not-bound_in (s . y) by A22, A23, A24, XBOOLE_0:def_5; ::_thesis: verum end; end; end; for s being Element of QC-WFF Al holds S1[s] from QC_LANG1:sch_2(A1); hence ( x <> y & not x in still_not-bound_in s9 implies not x in still_not-bound_in (s9 . y) ) ; ::_thesis: verum end; theorem Th32: :: VALUAT_1:32 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds J,v |= VERUM Al proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds J,v |= VERUM Al let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds J,v |= VERUM Al let v be Element of Valuations_in (Al,A); ::_thesis: for J being interpretation of Al,A holds J,v |= VERUM Al let J be interpretation of Al,A; ::_thesis: J,v |= VERUM Al ((Valuations_in (Al,A)) --> TRUE) . v = TRUE by FUNCOP_1:7; then (Valid ((VERUM Al),J)) . v = TRUE by Lm1; hence J,v |= VERUM Al by Def7; ::_thesis: verum end; theorem Th33: :: VALUAT_1:33 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p) let J be interpretation of Al,A; ::_thesis: J,v |= (p '&' q) => (q '&' p) thus (Valid (((p '&' q) => (q '&' p)),J)) . v = TRUE :: according to VALUAT_1:def_7 ::_thesis: verum proof assume not (Valid (((p '&' q) => (q '&' p)),J)) . v = TRUE ; ::_thesis: contradiction then A1: (Valid (((p '&' q) => (q '&' p)),J)) . v = FALSE by XBOOLEAN:def_3; (Valid (((p '&' q) => (q '&' p)),J)) . v = (Valid (('not' ((p '&' q) '&' ('not' (q '&' p)))),J)) . v by QC_LANG2:def_2 .= 'not' ((Valid (((p '&' q) '&' ('not' (q '&' p))),J)) . v) by Th10 .= 'not' (((Valid ((p '&' q),J)) . v) '&' ((Valid (('not' (q '&' p)),J)) . v)) by Th12 .= 'not' (((Valid ((p '&' q),J)) . v) '&' ('not' ((Valid ((q '&' p),J)) . v))) by Th10 ; then A2: ((Valid ((p '&' q),J)) . v) '&' ('not' ((Valid ((q '&' p),J)) . v)) = TRUE by A1, MARGREL1:11; then 'not' ((Valid ((q '&' p),J)) . v) = TRUE by MARGREL1:12; then A3: (Valid ((q '&' p),J)) . v = FALSE by MARGREL1:11; (Valid ((p '&' q),J)) . v = TRUE by A2, MARGREL1:12; then ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) = TRUE by Th12; hence contradiction by A3, Th12; ::_thesis: verum end; end; theorem Th34: :: VALUAT_1:34 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p let J be interpretation of Al,A; ::_thesis: J,v |= (('not' p) => p) => p ('not' p) => p = 'not' (('not' p) '&' ('not' p)) by QC_LANG2:def_2; then A1: (Valid (((('not' p) => p) => p),J)) . v = (Valid (('not' (('not' (('not' p) '&' ('not' p))) '&' ('not' p))),J)) . v by QC_LANG2:def_2 .= 'not' ((Valid ((('not' (('not' p) '&' ('not' p))) '&' ('not' p)),J)) . v) by Th10 .= 'not' (((Valid (('not' (('not' p) '&' ('not' p))),J)) . v) '&' ((Valid (('not' p),J)) . v)) by Th12 ; (Valid (('not' (('not' p) '&' ('not' p))),J)) . v = 'not' ((Valid ((('not' p) '&' ('not' p)),J)) . v) by Th10 .= 'not' ((Valid (('not' p),J)) . v) by Th22 .= 'not' ('not' ((Valid (p,J)) . v)) by Th10 .= (Valid (p,J)) . v ; then (Valid (((('not' p) => p) => p),J)) . v = 'not' (((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v))) by A1, Th10 .= TRUE by XBOOLEAN:102 ; hence (Valid (((('not' p) => p) => p),J)) . v = TRUE ; :: according to VALUAT_1:def_7 ::_thesis: verum end; theorem Th35: :: VALUAT_1:35 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= p => (('not' p) => q) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= p => (('not' p) => q) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= p => (('not' p) => q) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= p => (('not' p) => q) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= p => (('not' p) => q) let J be interpretation of Al,A; ::_thesis: J,v |= p => (('not' p) => q) ('not' p) => q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def_2; then A1: (Valid ((p => (('not' p) => q)),J)) . v = (Valid (('not' (p '&' ('not' ('not' (('not' p) '&' ('not' q)))))),J)) . v by QC_LANG2:def_2 .= 'not' ((Valid ((p '&' ('not' ('not' (('not' p) '&' ('not' q))))),J)) . v) by Th10 .= 'not' (((Valid (p,J)) . v) '&' ((Valid (('not' ('not' (('not' p) '&' ('not' q)))),J)) . v)) by Th12 ; (Valid (('not' ('not' (('not' p) '&' ('not' q)))),J)) . v = 'not' ((Valid (('not' (('not' p) '&' ('not' q))),J)) . v) by Th10 .= 'not' ('not' ((Valid ((('not' p) '&' ('not' q)),J)) . v)) by Th10 .= ((Valid (('not' p),J)) . v) '&' ((Valid (('not' q),J)) . v) by Th12 .= ('not' ((Valid (p,J)) . v)) '&' ((Valid (('not' q),J)) . v) by Th10 .= ('not' ((Valid (p,J)) . v)) '&' ('not' ((Valid (q,J)) . v)) by Th10 ; then A2: (Valid ((p => (('not' p) => q)),J)) . v = 'not' ((((Valid (p,J)) . v) '&' ('not' ((Valid (p,J)) . v))) '&' ('not' ((Valid (q,J)) . v))) by A1, MARGREL1:16 .= 'not' (FALSE '&' ('not' ((Valid (q,J)) . v))) by XBOOLEAN:138 ; FALSE '&' ('not' ((Valid (q,J)) . v)) = FALSE by MARGREL1:13; hence (Valid ((p => (('not' p) => q)),J)) . v = TRUE by A2, MARGREL1:11; :: according to VALUAT_1:def_7 ::_thesis: verum end; theorem Th36: :: VALUAT_1:36 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for v being Element of Valuations_in (Al,A) for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let A be non empty set ; ::_thesis: for v being Element of Valuations_in (Al,A) for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let v be Element of Valuations_in (Al,A); ::_thesis: for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let p, q, t be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let J be interpretation of Al,A; ::_thesis: J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) ( p => q = 'not' (p '&' ('not' q)) & ('not' (q '&' t)) => ('not' (p '&' t)) = 'not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))) ) by QC_LANG2:def_2; then A1: (Valid (((p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))),J)) . v = (Valid (('not' (('not' (p '&' ('not' q))) '&' ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))))),J)) . v by QC_LANG2:def_2 .= 'not' ((Valid ((('not' (p '&' ('not' q))) '&' ('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t))))))),J)) . v) by Th10 .= 'not' (((Valid (('not' (p '&' ('not' q))),J)) . v) '&' ((Valid (('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))),J)) . v)) by Th12 ; A2: (Valid (('not' (p '&' ('not' q))),J)) . v = 'not' ((Valid ((p '&' ('not' q)),J)) . v) by Th10 .= 'not' (((Valid (p,J)) . v) '&' ((Valid (('not' q),J)) . v)) by Th12 .= 'not' (((Valid (p,J)) . v) '&' ('not' ((Valid (q,J)) . v))) by Th10 ; (Valid (('not' ('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))))),J)) . v = 'not' ((Valid (('not' (('not' (q '&' t)) '&' ('not' ('not' (p '&' t))))),J)) . v) by Th10 .= 'not' ('not' ((Valid ((('not' (q '&' t)) '&' ('not' ('not' (p '&' t)))),J)) . v)) by Th10 .= ((Valid (('not' (q '&' t)),J)) . v) '&' ((Valid (('not' ('not' (p '&' t))),J)) . v) by Th12 .= ('not' ((Valid ((q '&' t),J)) . v)) '&' ((Valid (('not' ('not' (p '&' t))),J)) . v) by Th10 .= ('not' ((Valid ((q '&' t),J)) . v)) '&' ('not' ((Valid (('not' (p '&' t)),J)) . v)) by Th10 .= ('not' ((Valid ((q '&' t),J)) . v)) '&' ('not' ('not' ((Valid ((p '&' t),J)) . v))) by Th10 .= ('not' (((Valid (q,J)) . v) '&' ((Valid (t,J)) . v))) '&' ((Valid ((p '&' t),J)) . v) by Th12 .= ('not' (((Valid (q,J)) . v) '&' ((Valid (t,J)) . v))) '&' (((Valid (p,J)) . v) '&' ((Valid (t,J)) . v)) by Th12 ; hence (Valid (((p => q) => (('not' (q '&' t)) => ('not' (p '&' t)))),J)) . v = TRUE by A1, A2, Lm2; :: according to VALUAT_1:def_7 ::_thesis: verum end; theorem :: VALUAT_1:37 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & J,v |= p => q holds J,v |= q by Th24; theorem Th38: :: VALUAT_1:38 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (All (x,p)) => p proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (All (x,p)) => p let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (All (x,p)) => p let x be bound_QC-variable of Al; ::_thesis: for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (All (x,p)) => p let v be Element of Valuations_in (Al,A); ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (All (x,p)) => p let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J,v |= (All (x,p)) => p let J be interpretation of Al,A; ::_thesis: J,v |= (All (x,p)) => p thus (Valid (((All (x,p)) => p),J)) . v = TRUE :: according to VALUAT_1:def_7 ::_thesis: verum proof assume not (Valid (((All (x,p)) => p),J)) . v = TRUE ; ::_thesis: contradiction then A1: (Valid (((All (x,p)) => p),J)) . v = FALSE by XBOOLEAN:def_3; (Valid (((All (x,p)) => p),J)) . v = (Valid (('not' ((All (x,p)) '&' ('not' p))),J)) . v by QC_LANG2:def_2 .= 'not' ((Valid (((All (x,p)) '&' ('not' p)),J)) . v) by Th10 .= 'not' (((Valid ((All (x,p)),J)) . v) '&' ((Valid (('not' p),J)) . v)) by Th12 .= 'not' (((Valid ((All (x,p)),J)) . v) '&' ('not' ((Valid (p,J)) . v))) by Th10 ; then A2: ((Valid ((All (x,p)),J)) . v) '&' ('not' ((Valid (p,J)) . v)) = TRUE by A1, MARGREL1:11; then 'not' ((Valid (p,J)) . v) = TRUE by MARGREL1:12; then A3: (Valid (p,J)) . v = FALSE by MARGREL1:11; (Valid ((All (x,p)),J)) . v = TRUE by A2, MARGREL1:12; then (FOR_ALL (x,(Valid (p,J)))) . v = TRUE by Lm1; hence contradiction by A3, Th25; ::_thesis: verum end; end; theorem :: VALUAT_1:39 for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A holds J |= VERUM Al proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for J being interpretation of Al,A holds J |= VERUM Al let A be non empty set ; ::_thesis: for J being interpretation of Al,A holds J |= VERUM Al let J be interpretation of Al,A; ::_thesis: J |= VERUM Al let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= VERUM Al thus J,v |= VERUM Al by Th32; ::_thesis: verum end; theorem :: VALUAT_1:40 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p) let A be non empty set ; ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p) let J be interpretation of Al,A; ::_thesis: J |= (p '&' q) => (q '&' p) let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (p '&' q) => (q '&' p) thus J,v |= (p '&' q) => (q '&' p) by Th33; ::_thesis: verum end; theorem :: VALUAT_1:41 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (('not' p) => p) => p proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (('not' p) => p) => p let A be non empty set ; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (('not' p) => p) => p let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (('not' p) => p) => p let J be interpretation of Al,A; ::_thesis: J |= (('not' p) => p) => p let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (('not' p) => p) => p thus J,v |= (('not' p) => p) => p by Th34; ::_thesis: verum end; theorem :: VALUAT_1:42 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= p => (('not' p) => q) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= p => (('not' p) => q) let A be non empty set ; ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= p => (('not' p) => q) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= p => (('not' p) => q) let J be interpretation of Al,A; ::_thesis: J |= p => (('not' p) => q) let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= p => (('not' p) => q) thus J,v |= p => (('not' p) => q) by Th35; ::_thesis: verum end; theorem :: VALUAT_1:43 for Al being QC-alphabet for A being non empty set for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let A be non empty set ; ::_thesis: for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let p, q, t be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let J be interpretation of Al,A; ::_thesis: J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) thus J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) by Th36; ::_thesis: verum end; theorem :: VALUAT_1:44 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p & J |= p => q holds J |= q proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p & J |= p => q holds J |= q let A be non empty set ; ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p & J |= p => q holds J |= q let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st J |= p & J |= p => q holds J |= q let J be interpretation of Al,A; ::_thesis: ( J |= p & J |= p => q implies J |= q ) assume A1: ( J |= p & J |= p => q ) ; ::_thesis: J |= q now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_J,v_|=_q let v be Element of Valuations_in (Al,A); ::_thesis: J,v |= q ( J,v |= p & J,v |= p => q ) by A1, Def8; hence J,v |= q by Th24; ::_thesis: verum end; hence J |= q by Def8; ::_thesis: verum end; theorem :: VALUAT_1:45 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (All (x,p)) => p proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (All (x,p)) => p let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (All (x,p)) => p let x be bound_QC-variable of Al; ::_thesis: for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (All (x,p)) => p let p be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A holds J |= (All (x,p)) => p let J be interpretation of Al,A; ::_thesis: J |= (All (x,p)) => p let v be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,v |= (All (x,p)) => p thus J,v |= (All (x,p)) => p by Th38; ::_thesis: verum end; theorem :: VALUAT_1:46 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds J |= p => (All (x,q)) proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds J |= p => (All (x,q)) let A be non empty set ; ::_thesis: for x being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds J |= p => (All (x,q)) let x be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds J |= p => (All (x,q)) let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds J |= p => (All (x,q)) let J be interpretation of Al,A; ::_thesis: ( J |= p => q & not x in still_not-bound_in p implies J |= p => (All (x,q)) ) assume that A1: for v being Element of Valuations_in (Al,A) holds J,v |= p => q and A2: not x in still_not-bound_in p ; :: according to VALUAT_1:def_8 ::_thesis: J |= p => (All (x,q)) let u be Element of Valuations_in (Al,A); :: according to VALUAT_1:def_8 ::_thesis: J,u |= p => (All (x,q)) now__::_thesis:_(_J,u_|=_p_implies_J,u_|=_All_(x,q)_) assume A3: J,u |= p ; ::_thesis: J,u |= All (x,q) now__::_thesis:_for_w_being_Element_of_Valuations_in_(Al,A)_st_(_for_y_being_bound_QC-variable_of_Al_st_x_<>_y_holds_ w_._y_=_u_._y_)_holds_ J,w_|=_q let w be Element of Valuations_in (Al,A); ::_thesis: ( ( for y being bound_QC-variable of Al st x <> y holds w . y = u . y ) implies J,w |= q ) assume for y being bound_QC-variable of Al st x <> y holds w . y = u . y ; ::_thesis: J,w |= q then A4: J,w |= p by A2, A3, Th28; J,w |= p => q by A1; hence J,w |= q by A4, Th24; ::_thesis: verum end; hence J,u |= All (x,q) by Th29; ::_thesis: verum end; hence J,u |= p => (All (x,q)) by Th24; ::_thesis: verum end; theorem :: VALUAT_1:47 for Al being QC-alphabet for A being non empty set for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q proof let Al be QC-alphabet ; ::_thesis: for A being non empty set for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q let A be non empty set ; ::_thesis: for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q let x, y be bound_QC-variable of Al; ::_thesis: for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q let p, q be Element of CQC-WFF Al; ::_thesis: for J being interpretation of Al,A for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q let J be interpretation of Al,A; ::_thesis: for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q let s be QC-formula of Al; ::_thesis: ( p = s . x & q = s . y & not x in still_not-bound_in s & J |= p implies J |= q ) assume that A1: p = s . x and A2: q = s . y and A3: not x in still_not-bound_in s and A4: J |= p ; ::_thesis: J |= q now__::_thesis:_(_x_<>_y_implies_J_|=_q_) assume A5: x <> y ; ::_thesis: J |= q A6: now__::_thesis:_for_u_being_Element_of_Valuations_in_(Al,A)_holds_(Valid_(q,J))_._u_=_TRUE let u be Element of Valuations_in (Al,A); ::_thesis: (Valid (q,J)) . u = TRUE consider w being Element of Valuations_in (Al,A) such that A7: ( ( for z being bound_QC-variable of Al st z <> x holds w . z = u . z ) & w . x = u . y ) by Lm3; w . x = w . y by A7; then A8: (Valid (p,J)) . w = (Valid (q,J)) . w by A1, A2, Th30; J,w |= p by A4, Def8; then A9: (Valid (p,J)) . w = TRUE by Def7; not x in still_not-bound_in q by A2, A3, A5, Th31; hence (Valid (q,J)) . u = TRUE by A7, A8, A9, Th27; ::_thesis: verum end; now__::_thesis:_for_v_being_Element_of_Valuations_in_(Al,A)_holds_J,v_|=_q let v be Element of Valuations_in (Al,A); ::_thesis: J,v |= q (Valid (q,J)) . v = TRUE by A6; hence J,v |= q by Def7; ::_thesis: verum end; hence J |= q by Def8; ::_thesis: verum end; hence J |= q by A1, A2, A4; ::_thesis: verum end;