:: 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 ) )

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

definition

let A be QC-alphabet ;

let l be FinSequence of QC-variables A;

let f be Substitution of A;

ex b_{1} being FinSequence of QC-variables A st

( len b_{1} = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds

( ( l . k in dom f implies b_{1} . k = f . (l . k) ) & ( not l . k in dom f implies b_{1} . k = l . k ) ) ) )

for b_{1}, b_{2} being FinSequence of QC-variables A st len b_{1} = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds

( ( l . k in dom f implies b_{1} . k = f . (l . k) ) & ( not l . k in dom f implies b_{1} . k = l . k ) ) ) & len b_{2} = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds

( ( l . k in dom f implies b_{2} . k = f . (l . k) ) & ( not l . k in dom f implies b_{2} . k = l . k ) ) ) holds

b_{1} = b_{2}

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

ex b

( len b

( ( l . k in dom f implies b

proof end;

uniqueness for b

( ( l . k in dom f implies b

( ( l . k in dom f implies b

b

proof 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 b_{4} being FinSequence of QC-variables A holds

( b_{4} = Subst (l,f) iff ( len b_{4} = len l & ( for k being Element of NAT st 1 <= k & k <= len l holds

( ( l . k in dom f implies b_{4} . k = f . (l . k) ) & ( not l . k in dom f implies b_{4} . k = l . k ) ) ) ) );

for A being QC-alphabet

for l being FinSequence of QC-variables A

for f being Substitution of A

for b

( b

( ( l . k in dom f implies b

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;

coherence

Subst (l,f) is k -element

end;
let k be Element of NAT ;

let l be QC-variable_list of k,A;

let f be Substitution of A;

coherence

Subst (l,f) is k -element

proof 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

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

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 ) )

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 ;

{ s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } is Subset of (QC-WFF A)

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

{ s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } is Subset of (QC-WFF A)

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

for A being QC-alphabet holds CQC-WFF A = { s where s is QC-formula of A : ( Fixed s = {} & Free s = {} ) } ;

registration
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 = {} ) )

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 ;

ex b_{1} being QC-variable_list of k,A st b_{1} is bound_QC-variables A -valued

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

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

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

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

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

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

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 )

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 ) )

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

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

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 )

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

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

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

scheme :: CQC_LANG:sch 1

CQCInd{ F_{1}() -> QC-alphabet , P_{1}[ set ] } :

provided

CQCInd{ F

provided

A1:
for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( P_{1}[ VERUM F_{1}()] & P_{1}[P ! l] & ( P_{1}[r] implies P_{1}[ 'not' r] ) & ( P_{1}[r] & P_{1}[s] implies P_{1}[r '&' s] ) & ( P_{1}[r] implies P_{1}[ All (x,r)] ) )

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( P

proof end;

scheme :: CQC_LANG:sch 2

CQCFuncEx{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( set , set , set ) -> Element of F_{2}(), F_{5}( set ) -> Element of F_{2}(), F_{6}( set , set ) -> Element of F_{2}(), F_{7}( set , set ) -> Element of F_{2}() } :

CQCFuncEx{ F

ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( F . (VERUM F_{1}()) = F_{3}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{4}(k,P,l) & F . ('not' r) = F_{5}((F . r)) & F . (r '&' s) = F_{6}((F . r),(F . s)) & F . (All (x,r)) = F_{7}(x,(F . r)) ) ) )

( F . (VERUM F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

proof end;

scheme :: CQC_LANG:sch 3

CQCFuncUniq{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Function of (CQC-WFF F_{1}()),F_{2}(), F_{4}() -> Function of (CQC-WFF F_{1}()),F_{2}(), F_{5}() -> Element of F_{2}(), F_{6}( set , set , set ) -> Element of F_{2}(), F_{7}( set ) -> Element of F_{2}(), F_{8}( set , set ) -> Element of F_{2}(), F_{9}( set , set ) -> Element of F_{2}() } :

provided

CQCFuncUniq{ F

provided

A1:
( F_{3}() . (VERUM F_{1}()) = F_{5}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F_{3}() . (P ! l) = F_{6}(k,P,l) & F_{3}() . ('not' r) = F_{7}((F_{3}() . r)) & F_{3}() . (r '&' s) = F_{8}((F_{3}() . r),(F_{3}() . s)) & F_{3}() . (All (x,r)) = F_{9}(x,(F_{3}() . r)) ) ) )
and

A2: ( F_{4}() . (VERUM F_{1}()) = F_{5}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F_{4}() . (P ! l) = F_{6}(k,P,l) & F_{4}() . ('not' r) = F_{7}((F_{4}() . r)) & F_{4}() . (r '&' s) = F_{8}((F_{4}() . r),(F_{4}() . s)) & F_{4}() . (All (x,r)) = F_{9}(x,(F_{4}() . r)) ) ) )

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F

A2: ( F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F

proof end;

scheme :: CQC_LANG:sch 4

CQCDefcorrectness{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of CQC-WFF F_{1}(), F_{4}() -> Element of F_{2}(), F_{5}( set , set , set ) -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}( set , set ) -> Element of F_{2}(), F_{8}( set , set ) -> Element of F_{2}() } :

CQCDefcorrectness{ F

( ex d being Element of F_{2}() ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d = F . F_{3}() & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{7}((F . r),(F . s)) & F . (All (x,r)) = F_{8}(x,(F . r)) ) ) ) & ( for d1, d2 being Element of F_{2}() st ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d1 = F . F_{3}() & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{7}((F . r),(F . s)) & F . (All (x,r)) = F_{8}(x,(F . r)) ) ) ) & ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d2 = F . F_{3}() & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{7}((F . r),(F . s)) & F . (All (x,r)) = F_{8}(x,(F . r)) ) ) ) holds

d1 = d2 ) )

( d = F . F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

( d1 = F . F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

( d2 = F . F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

d1 = d2 ) )

proof end;

scheme :: CQC_LANG:sch 5

CQCDefVERUM{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Element of F_{2}(), F_{5}( set , set , set ) -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}( set , set ) -> Element of F_{2}(), F_{8}( set , set ) -> Element of F_{2}() } :

provided

CQCDefVERUM{ F

provided

A1:
for p being Element of CQC-WFF F_{1}()

for d being Element of F_{2}() holds

( d = F_{3}(p) iff ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d = F . p & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{7}((F . r),(F . s)) & F . (All (x,r)) = F_{8}(x,(F . r)) ) ) ) )

for d being Element of F

( d = F

( d = F . p & F . (VERUM F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

proof end;

scheme :: CQC_LANG:sch 6

CQCDefatomic{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( set ) -> Element of F_{2}(), F_{5}( set , set , set ) -> Element of F_{2}(), F_{6}() -> Element of NAT , F_{7}() -> QC-pred_symbol of F_{6}(),F_{1}(), F_{8}() -> CQC-variable_list of F_{6}(),F_{1}(), F_{9}( set ) -> Element of F_{2}(), F_{10}( set , set ) -> Element of F_{2}(), F_{11}( set , set ) -> Element of F_{2}() } :

provided

CQCDefatomic{ F

provided

A1:
for p being Element of CQC-WFF F_{1}()

for d being Element of F_{2}() holds

( d = F_{4}(p) iff ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d = F . p & F . (VERUM F_{1}()) = F_{3}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{9}((F . r)) & F . (r '&' s) = F_{10}((F . r),(F . s)) & F . (All (x,r)) = F_{11}(x,(F . r)) ) ) ) )

for d being Element of F

( d = F

( d = F . p & F . (VERUM F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

proof end;

scheme :: CQC_LANG:sch 7

CQCDefnegative{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Element of F_{2}(), F_{5}( set , set , set ) -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}() -> Element of CQC-WFF F_{1}(), F_{8}( set , set ) -> Element of F_{2}(), F_{9}( set , set ) -> Element of F_{2}() } :

provided

CQCDefnegative{ F

provided

A1:
for p being Element of CQC-WFF F_{1}()

for d being Element of F_{2}() holds

( d = F_{3}(p) iff ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d = F . p & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{8}((F . r),(F . s)) & F . (All (x,r)) = F_{9}(x,(F . r)) ) ) ) )

for d being Element of F

( d = F

( d = F . p & F . (VERUM F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

proof end;

scheme :: CQC_LANG:sch 8

QCDefconjunctive{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Element of F_{2}(), F_{5}( set , set , set ) -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}( set , set ) -> Element of F_{2}(), F_{8}() -> Element of CQC-WFF F_{1}(), F_{9}() -> Element of CQC-WFF F_{1}(), F_{10}( set , set ) -> Element of F_{2}() } :

provided

QCDefconjunctive{ F

provided

A1:
for p being Element of CQC-WFF F_{1}()

for d being Element of F_{2}() holds

( d = F_{3}(p) iff ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d = F . p & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{7}((F . r),(F . s)) & F . (All (x,r)) = F_{10}(x,(F . r)) ) ) ) )

for d being Element of F

( d = F

( d = F . p & F . (VERUM F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

proof end;

scheme :: CQC_LANG:sch 9

QCDefuniversal{ F_{1}() -> QC-alphabet , F_{2}() -> non empty set , F_{3}( set ) -> Element of F_{2}(), F_{4}() -> Element of F_{2}(), F_{5}( set , set , set ) -> Element of F_{2}(), F_{6}( set ) -> Element of F_{2}(), F_{7}( set , set ) -> Element of F_{2}(), F_{8}( set , set ) -> Element of F_{2}(), F_{9}() -> bound_QC-variable of F_{1}(), F_{10}() -> Element of CQC-WFF F_{1}() } :

provided

QCDefuniversal{ F

provided

A1:
for p being Element of CQC-WFF F_{1}()

for d being Element of F_{2}() holds

( d = F_{3}(p) iff ex F being Function of (CQC-WFF F_{1}()),F_{2}() st

( d = F . p & F . (VERUM F_{1}()) = F_{4}() & ( for r, s being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}()

for k being Element of NAT

for l being CQC-variable_list of k,F_{1}()

for P being QC-pred_symbol of k,F_{1}() holds

( F . (P ! l) = F_{5}(k,P,l) & F . ('not' r) = F_{6}((F . r)) & F . (r '&' s) = F_{7}((F . r),(F . s)) & F . (All (x,r)) = F_{8}(x,(F . r)) ) ) ) )

for d being Element of F

( d = F

( d = F . p & F . (VERUM F

for x being bound_QC-variable of F

for k being Element of NAT

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

( F . (P ! l) = F

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;

ex b_{1} being Element of QC-WFF A ex F being Function of (QC-WFF A),(QC-WFF A) st

( b_{1} = 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))))) ) ) ) )

for b_{1}, b_{2} being Element of QC-WFF A st ex F being Function of (QC-WFF A),(QC-WFF A) st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}
by Lm2;

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

ex b

( b

( 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 b

( b

( 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

( b

( 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

b

:: 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 b_{4} being Element of QC-WFF A holds

( b_{4} = p . x iff ex F being Function of (QC-WFF A),(QC-WFF A) st

( b_{4} = 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))))) ) ) ) ) );

for A being QC-alphabet

for p being Element of QC-WFF A

for x being bound_QC-variable of A

for b

( b

( b

( 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 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)))

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)))

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)

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)

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)

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)

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

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))

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)

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))

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

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

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

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

:: from AMI_1, 2006.03.14, A.T.

:: from SCMPDS_9, 2006.03.26, A.T.

theorem :: CQC_LANG:32

theorem :: CQC_LANG:33