:: A Classical First Order Language :: by Czes{\l}aw Byli\'nski :: :: Received May 11, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for A being QC-alphabet for x being bound_QC-variable of A holds not x in fixed_QC-variables A proofend; theorem Th1: :: CQC_LANG:1 for A being QC-alphabet for x being set holds ( x in QC-variables A iff ( x in fixed_QC-variables A or x in free_QC-variables A or x in bound_QC-variables A ) ) proofend; definition let A be QC-alphabet ; mode Substitution of A is PartFunc of (free_QC-variables A),(QC-variables A); end; definition let A be QC-alphabet ; let l be FinSequence of QC-variables A; let f be Substitution of A; func Subst (l,f) -> FinSequence of QC-variables A means :Def1: :: CQC_LANG:def 1 ( len it = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom f implies it . k = f . (l . k) ) & ( not l . k in dom f implies it . k = l . k ) ) ) ); existence ex b1 being FinSequence of QC-variables A st ( len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom f implies b1 . k = f . (l . k) ) & ( not l . k in dom f implies b1 . k = l . k ) ) ) ) proofend; uniqueness for b1, b2 being FinSequence of QC-variables A st len b1 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom f implies b1 . k = f . (l . k) ) & ( not l . k in dom f implies b1 . k = l . k ) ) ) & len b2 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom f implies b2 . k = f . (l . k) ) & ( not l . k in dom f implies b2 . k = l . k ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Subst CQC_LANG:def_1_:_ for A being QC-alphabet for l being FinSequence of QC-variables A for f being Substitution of A for b4 being FinSequence of QC-variables A holds ( b4 = Subst (l,f) iff ( len b4 = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds ( ( l . k in dom f implies b4 . k = f . (l . k) ) & ( not l . k in dom f implies b4 . k = l . k ) ) ) ) ); registration let A be QC-alphabet ; let k be Element of NAT ; let l be QC-variable_list of k,A; let f be Substitution of A; cluster Subst (l,f) -> k -element ; coherence Subst (l,f) is k -element proofend; end; theorem Th2: :: CQC_LANG:2 for A being QC-alphabet for x being bound_QC-variable of A for a being free_QC-variable of A holds a .--> x is Substitution of A proofend; definition let A be QC-alphabet ; let a be free_QC-variable of A; let x be bound_QC-variable of A; :: original:.--> redefine funca .--> x -> Substitution of A; coherence a .--> x is Substitution of A by Th2; end; theorem Th3: :: CQC_LANG:3 for A being QC-alphabet for k being Element of NAT for f being Substitution of A for x being bound_QC-variable of A for a being free_QC-variable of A for l, ll being FinSequence of QC-variables A st f = a .--> x & ll = Subst (l,f) & 1 <= k & k <= len l holds ( ( l . k = a implies ll . k = x ) & ( l . k <> a implies ll . k = l . k ) ) proofend; definition let A be QC-alphabet ; func CQC-WFF A -> Subset of (QC-WFF A) equals :: CQC_LANG:def 2 { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ; coherence { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } is Subset of (QC-WFF A) proofend; end; :: deftheorem defines CQC-WFF CQC_LANG:def_2_:_ for A being QC-alphabet holds CQC-WFF A = { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ; registration let A be QC-alphabet ; cluster CQC-WFF A -> non empty ; coherence not CQC-WFF A is empty proofend; end; theorem Th4: :: CQC_LANG:4 for A being QC-alphabet for p being Element of QC-WFF A holds ( p is Element of CQC-WFF A iff ( Fixed p = {} & Free p = {} ) ) proofend; registration let A be QC-alphabet ; let k be Element of NAT ; cluster Relation-like NAT -defined QC-variables A -valued bound_QC-variables A -valued Function-like k -element FinSequence-like for FinSequence of QC-variables A; existence ex b1 being QC-variable_list of k,A st b1 is bound_QC-variables A -valued proofend; end; definition let A be QC-alphabet ; let k be Element of NAT ; mode CQC-variable_list of k,A is bound_QC-variables A -valued QC-variable_list of k,A; end; theorem Th5: :: CQC_LANG:5 for A being QC-alphabet for k being Element of NAT for l being QC-variable_list of k,A holds ( l is CQC-variable_list of k,A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) ) proofend; theorem Th6: :: CQC_LANG:6 for A being QC-alphabet holds VERUM A is Element of CQC-WFF A proofend; theorem Th7: :: CQC_LANG:7 for A being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A holds ( P ! l is Element of CQC-WFF A iff ( { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables A ) } = {} & { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables A ) } = {} ) ) proofend; definition let k be Element of NAT ; let A be QC-alphabet ; let P be QC-pred_symbol of k,A; let l be CQC-variable_list of k,A; :: original:! redefine funcP ! l -> Element of CQC-WFF A; coherence P ! l is Element of CQC-WFF A proofend; end; theorem Th8: :: CQC_LANG:8 for A being QC-alphabet for p being Element of QC-WFF A holds ( 'not' p is Element of CQC-WFF A iff p is Element of CQC-WFF A ) proofend; theorem Th9: :: CQC_LANG:9 for A being QC-alphabet for p, q being Element of QC-WFF A holds ( p '&' q is Element of CQC-WFF A iff ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) ) proofend; definition let A be QC-alphabet ; :: original:VERUM redefine func VERUM A -> Element of CQC-WFF A; coherence VERUM A is Element of CQC-WFF A by Th6; let r be Element of CQC-WFF A; :: original:'not' redefine func 'not' r -> Element of CQC-WFF A; coherence 'not' r is Element of CQC-WFF A by Th8; let s be Element of CQC-WFF A; :: original:'&' redefine funcr '&' s -> Element of CQC-WFF A; coherence r '&' s is Element of CQC-WFF A by Th9; end; theorem Th10: :: CQC_LANG:10 for A being QC-alphabet for r, s being Element of CQC-WFF A holds r => s is Element of CQC-WFF A proofend; theorem Th11: :: CQC_LANG:11 for A being QC-alphabet for r, s being Element of CQC-WFF A holds r 'or' s is Element of CQC-WFF A proofend; theorem Th12: :: CQC_LANG:12 for A being QC-alphabet for r, s being Element of CQC-WFF A holds r <=> s is Element of CQC-WFF A proofend; definition let A be QC-alphabet ; let r, s be Element of CQC-WFF A; :: original:=> redefine funcr => s -> Element of CQC-WFF A; coherence r => s is Element of CQC-WFF A by Th10; :: original:'or' redefine funcr 'or' s -> Element of CQC-WFF A; coherence r 'or' s is Element of CQC-WFF A by Th11; :: original:<=> redefine funcr <=> s -> Element of CQC-WFF A; coherence r <=> s is Element of CQC-WFF A by Th12; end; theorem Th13: :: CQC_LANG:13 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds ( All (x,p) is Element of CQC-WFF A iff p is Element of CQC-WFF A ) proofend; definition let A be QC-alphabet ; let x be bound_QC-variable of A; let r be Element of CQC-WFF A; :: original:All redefine func All (x,r) -> Element of CQC-WFF A; coherence All (x,r) is Element of CQC-WFF A by Th13; end; theorem Th14: :: CQC_LANG:14 for A being QC-alphabet for x being bound_QC-variable of A for r being Element of CQC-WFF A holds Ex (x,r) is Element of CQC-WFF A proofend; definition let A be QC-alphabet ; let x be bound_QC-variable of A; let r be Element of CQC-WFF A; :: original:Ex redefine func Ex (x,r) -> Element of CQC-WFF A; coherence Ex (x,r) is Element of CQC-WFF A by Th14; end; scheme :: CQC_LANG:sch 1 CQCInd{ F1() -> QC-alphabet , P1[ set ] } : for r being Element of CQC-WFF F1() holds P1[r] provided A1: for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( P1[ VERUM F1()] & P1[P ! l] & ( P1[r] implies P1[ 'not' r] ) & ( P1[r] & P1[s] implies P1[r '&' s] ) & ( P1[r] implies P1[ All (x,r)] ) ) proofend; scheme :: CQC_LANG:sch 2 CQCFuncEx{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( set , set , set ) -> Element of F2(), F5( set ) -> Element of F2(), F6( set , set ) -> Element of F2(), F7( set , set ) -> Element of F2() } : ex F being Function of (CQC-WFF F1()),F2() st ( F . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F4(k,P,l) & F . ('not' r) = F5((F . r)) & F . (r '&' s) = F6((F . r),(F . s)) & F . (All (x,r)) = F7(x,(F . r)) ) ) ) proofend; scheme :: CQC_LANG:sch 3 CQCFuncUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Function of (CQC-WFF F1()),F2(), F4() -> Function of (CQC-WFF F1()),F2(), F5() -> Element of F2(), F6( set , set , set ) -> Element of F2(), F7( set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9( set , set ) -> Element of F2() } : F3() = F4() provided A1: ( F3() . (VERUM F1()) = F5() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F3() . (P ! l) = F6(k,P,l) & F3() . ('not' r) = F7((F3() . r)) & F3() . (r '&' s) = F8((F3() . r),(F3() . s)) & F3() . (All (x,r)) = F9(x,(F3() . r)) ) ) ) and A2: ( F4() . (VERUM F1()) = F5() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F4() . (P ! l) = F6(k,P,l) & F4() . ('not' r) = F7((F4() . r)) & F4() . (r '&' s) = F8((F4() . r),(F4() . s)) & F4() . (All (x,r)) = F9(x,(F4() . r)) ) ) ) proofend; scheme :: CQC_LANG:sch 4 CQCDefcorrectness{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of CQC-WFF F1(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8( set , set ) -> Element of F2() } : ( ex d being Element of F2() ex F being Function of (CQC-WFF F1()),F2() st ( d = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ( for d1, d2 being Element of F2() st ex F being Function of (CQC-WFF F1()),F2() st ( d1 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F1()),F2() st ( d2 = F . F3() & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) holds d1 = d2 ) ) proofend; scheme :: CQC_LANG:sch 5 CQCDefVERUM{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8( set , set ) -> Element of F2() } : F3((VERUM F1())) = F4() provided A1: for p being Element of CQC-WFF F1() for d being Element of F2() holds ( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st ( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) ) proofend; scheme :: CQC_LANG:sch 6 CQCDefatomic{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( set ) -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6() -> Element of NAT , F7() -> QC-pred_symbol of F6(),F1(), F8() -> CQC-variable_list of F6(),F1(), F9( set ) -> Element of F2(), F10( set , set ) -> Element of F2(), F11( set , set ) -> Element of F2() } : F4((F7() ! F8())) = F5(F6(),F7(),F8()) provided A1: for p being Element of CQC-WFF F1() for d being Element of F2() holds ( d = F4(p) iff ex F being Function of (CQC-WFF F1()),F2() st ( d = F . p & F . (VERUM F1()) = F3() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F9((F . r)) & F . (r '&' s) = F10((F . r),(F . s)) & F . (All (x,r)) = F11(x,(F . r)) ) ) ) ) proofend; scheme :: CQC_LANG:sch 7 CQCDefnegative{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7() -> Element of CQC-WFF F1(), F8( set , set ) -> Element of F2(), F9( set , set ) -> Element of F2() } : F3(('not' F7())) = F6(F3(F7())) provided A1: for p being Element of CQC-WFF F1() for d being Element of F2() holds ( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st ( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F8((F . r),(F . s)) & F . (All (x,r)) = F9(x,(F . r)) ) ) ) ) proofend; scheme :: CQC_LANG:sch 8 QCDefconjunctive{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8() -> Element of CQC-WFF F1(), F9() -> Element of CQC-WFF F1(), F10( set , set ) -> Element of F2() } : F3((F8() '&' F9())) = F7(F3(F8()),F3(F9())) provided A1: for p being Element of CQC-WFF F1() for d being Element of F2() holds ( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st ( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F10(x,(F . r)) ) ) ) ) proofend; scheme :: CQC_LANG:sch 9 QCDefuniversal{ F1() -> QC-alphabet , F2() -> non empty set , F3( set ) -> Element of F2(), F4() -> Element of F2(), F5( set , set , set ) -> Element of F2(), F6( set ) -> Element of F2(), F7( set , set ) -> Element of F2(), F8( set , set ) -> Element of F2(), F9() -> bound_QC-variable of F1(), F10() -> Element of CQC-WFF F1() } : F3((All (F9(),F10()))) = F8(F9(),F3(F10())) provided A1: for p being Element of CQC-WFF F1() for d being Element of F2() holds ( d = F3(p) iff ex F being Function of (CQC-WFF F1()),F2() st ( d = F . p & F . (VERUM F1()) = F4() & ( for r, s being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds ( F . (P ! l) = F5(k,P,l) & F . ('not' r) = F6((F . r)) & F . (r '&' s) = F7((F . r),(F . s)) & F . (All (x,r)) = F8(x,(F . r)) ) ) ) ) proofend; Lm2: for A being QC-alphabet for x being bound_QC-variable of A for F1, F2 being Function of (QC-WFF A),(QC-WFF A) st ( for q being Element of QC-WFF A holds ( F1 . (VERUM A) = VERUM A & ( q is atomic implies F1 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F1 . q = 'not' (F1 . (the_argument_of q)) ) & ( q is conjunctive implies F1 . q = (F1 . (the_left_argument_of q)) '&' (F1 . (the_right_argument_of q)) ) & ( q is universal implies F1 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F1 . (the_scope_of q))))) ) ) ) & ( for q being Element of QC-WFF A holds ( F2 . (VERUM A) = VERUM A & ( q is atomic implies F2 . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F2 . q = 'not' (F2 . (the_argument_of q)) ) & ( q is conjunctive implies F2 . q = (F2 . (the_left_argument_of q)) '&' (F2 . (the_right_argument_of q)) ) & ( q is universal implies F2 . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F2 . (the_scope_of q))))) ) ) ) holds F1 = F2 proofend; definition let A be QC-alphabet ; let p be Element of QC-WFF A; let x be bound_QC-variable of A; funcp . x -> Element of QC-WFF A means :Def3: :: CQC_LANG:def 3 ex F being Function of (QC-WFF A),(QC-WFF A) st ( it = F . p & ( for q being Element of QC-WFF A holds ( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ); existence ex b1 being Element of QC-WFF A ex F being Function of (QC-WFF A),(QC-WFF A) st ( b1 = F . p & ( for q being Element of QC-WFF A holds ( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) proofend; uniqueness for b1, b2 being Element of QC-WFF A st ex F being Function of (QC-WFF A),(QC-WFF A) st ( b1 = F . p & ( for q being Element of QC-WFF A holds ( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) & ex F being Function of (QC-WFF A),(QC-WFF A) st ( b2 = F . p & ( for q being Element of QC-WFF A holds ( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) holds b1 = b2 by Lm2; end; :: deftheorem Def3 defines . CQC_LANG:def_3_:_ for A being QC-alphabet for p being Element of QC-WFF A for x being bound_QC-variable of A for b4 being Element of QC-WFF A holds ( b4 = p . x iff ex F being Function of (QC-WFF A),(QC-WFF A) st ( b4 = F . p & ( for q being Element of QC-WFF A holds ( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) ); theorem Th15: :: CQC_LANG:15 for A being QC-alphabet for x being bound_QC-variable of A holds (VERUM A) . x = VERUM A proofend; theorem Th16: :: CQC_LANG:16 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st p is atomic holds p . x = (the_pred_symbol_of p) ! (Subst ((the_arguments_of p),((A a. 0) .--> x))) proofend; theorem Th17: :: CQC_LANG:17 for A being QC-alphabet for k being Element of NAT for x being bound_QC-variable of A for P being QC-pred_symbol of k,A for l being QC-variable_list of k,A holds (P ! l) . x = P ! (Subst (l,((A a. 0) .--> x))) proofend; theorem Th18: :: CQC_LANG:18 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st p is negative holds p . x = 'not' ((the_argument_of p) . x) proofend; theorem Th19: :: CQC_LANG:19 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds ('not' p) . x = 'not' (p . x) proofend; theorem Th20: :: CQC_LANG:20 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st p is conjunctive holds p . x = ((the_left_argument_of p) . x) '&' ((the_right_argument_of p) . x) proofend; theorem Th21: :: CQC_LANG:21 for A being QC-alphabet for x being bound_QC-variable of A for p, q being Element of QC-WFF A holds (p '&' q) . x = (p . x) '&' (q . x) proofend; Lm3: for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st p is universal holds p . x = IFEQ ((bound_in p),x,p,(All ((bound_in p),((the_scope_of p) . x)))) proofend; theorem Th22: :: CQC_LANG:22 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st p is universal & bound_in p = x holds p . x = p proofend; theorem Th23: :: CQC_LANG:23 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st p is universal & bound_in p <> x holds p . x = All ((bound_in p),((the_scope_of p) . x)) proofend; theorem Th24: :: CQC_LANG:24 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds (All (x,p)) . x = All (x,p) proofend; theorem Th25: :: CQC_LANG:25 for A being QC-alphabet for x, y being bound_QC-variable of A for p being Element of QC-WFF A st x <> y holds (All (x,p)) . y = All (x,(p . y)) proofend; theorem Th26: :: CQC_LANG:26 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A st Free p = {} holds p . x = p proofend; theorem :: CQC_LANG:27 for A being QC-alphabet for x being bound_QC-variable of A for r being Element of CQC-WFF A holds r . x = r proofend; theorem :: CQC_LANG:28 for A being QC-alphabet for x being bound_QC-variable of A for p being Element of QC-WFF A holds Fixed (p . x) = Fixed p proofend; begin theorem :: CQC_LANG:29 for i, j, k being set holds (i,j) :-> k = [i,j] .--> k ; theorem :: CQC_LANG:30 for i, j, k being set holds ((i,j) :-> k) . (i,j) = k by FUNCT_4:80; :: from AMI_1, 2006.03.14, A.T. theorem :: CQC_LANG:31 for a, b, c being set holds (a,a) --> (b,c) = a .--> c by FUNCT_4:81; :: from SCMPDS_9, 2006.03.26, A.T. theorem :: CQC_LANG:32 for f being Function for a, b, c being set st a <> c holds (f +* (a .--> b)) . c = f . c by FUNCT_4:83; theorem :: CQC_LANG:33 for f being Function for a, b, c, d being set st a <> b holds ( (f +* ((a,b) --> (c,d))) . a = c & (f +* ((a,b) --> (c,d))) . b = d ) by FUNCT_4:84;