:: 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
proof end;

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 ) )
proof end;

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 ) ) ) )
proof end;
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
proof end;
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
proof end;
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
proof end;

definition
let A be QC-alphabet ;
let a be free_QC-variable of A;
let x be bound_QC-variable of A;
:: original: .-->
redefine func a .--> 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 ) )
proof end;

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)
proof end;
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
proof end;
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 = {} ) )
proof end;

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
proof end;
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 ) } = {} ) )
proof end;

theorem Th6: :: CQC_LANG:6
for A being QC-alphabet holds VERUM A is Element of CQC-WFF A
proof end;

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 ) } = {} ) )
proof end;

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 func P ! l -> Element of CQC-WFF A;
coherence
P ! l is Element of CQC-WFF A
proof end;
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 )
proof end;

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 ) )
proof end;

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 func r '&' 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
proof end;

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
proof end;

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
proof end;

definition
let A be QC-alphabet ;
let r, s be Element of CQC-WFF A;
:: original: =>
redefine func r => s -> Element of CQC-WFF A;
coherence
r => s is Element of CQC-WFF A by Th10;
:: original: 'or'
redefine func r 'or' s -> Element of CQC-WFF A;
coherence
r 'or' s is Element of CQC-WFF A by Th11;
:: original: <=>
redefine func r <=> 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 )
proof end;

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
proof end;

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)] ) )
proof end;

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)) ) ) )
proof end;

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)) ) ) )
proof end;

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 ) )
proof end;

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)) ) ) ) )
proof end;

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)) ) ) ) )
proof end;

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)) ) ) ) )
proof end;

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)) ) ) ) )
proof end;

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)) ) ) ) )
proof end;

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
proof end;

definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
let x be bound_QC-variable of A;
func p . 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))))) ) ) ) )
proof end;
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
proof end;

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)))
proof end;

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)))
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

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))))
proof end;

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
proof end;

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))
proof end;

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)
proof end;

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))
proof end;

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
proof end;

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
proof end;

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
proof end;

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;