:: by Agata Darmochwa{\l} and Andrzej Trybulec

::

:: Received November 22, 1991

:: Copyright (c) 1991-2019 Association of Mizar Users

definition

let A be QC-alphabet ;

let b be bound_QC-variable of A;

existence

ex b_{1} being QC-symbol of A st x. b_{1} = b
by QC_LANG3:30;

uniqueness

for b_{1}, b_{2} being QC-symbol of A st x. b_{1} = b & x. b_{2} = b holds

b_{1} = b_{2}
by XTUPLE_0:1;

end;
let b be bound_QC-variable of A;

existence

ex b

uniqueness

for b

b

:: deftheorem Def1 defines x. CQC_SIM1:def 1 :

for A being QC-alphabet

for b being bound_QC-variable of A

for b_{3} being QC-symbol of A holds

( b_{3} = x. b iff x. b_{3} = b );

for A being QC-alphabet

for b being bound_QC-variable of A

for b

( b

theorem Th3: :: CQC_SIM1:3

for x, y being set

for g being Function

for A being set holds (g +* (x .--> y)) .: (A \ {x}) = g .: (A \ {x})

for g being Function

for A being set holds (g +* (x .--> y)) .: (A \ {x}) = g .: (A \ {x})

proof end;

theorem Th4: :: CQC_SIM1:4

for x, y being set

for g being Function

for A being set st not y in g .: (A \ {x}) holds

(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}

for g being Function

for A being set st not y in g .: (A \ {x}) holds

(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}

proof end;

theorem Th5: :: CQC_SIM1:5

for A being QC-alphabet

for p being Element of CQC-WFF A st p is atomic holds

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll

for p being Element of CQC-WFF A st p is atomic holds

ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll

proof end;

theorem :: CQC_SIM1:6

for A being QC-alphabet

for p being Element of CQC-WFF A st p is negative holds

ex q being Element of CQC-WFF A st p = 'not' q

for p being Element of CQC-WFF A st p is negative holds

ex q being Element of CQC-WFF A st p = 'not' q

proof end;

theorem :: CQC_SIM1:7

for A being QC-alphabet

for p being Element of CQC-WFF A st p is conjunctive holds

ex q, r being Element of CQC-WFF A st p = q '&' r

for p being Element of CQC-WFF A st p is conjunctive holds

ex q, r being Element of CQC-WFF A st p = q '&' r

proof end;

theorem :: CQC_SIM1:8

for A being QC-alphabet

for p being Element of CQC-WFF A st p is universal holds

ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q)

for p being Element of CQC-WFF A st p is universal holds

ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q)

proof end;

scheme :: CQC_SIM1:sch 1

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

QCFuncExN{ F

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

( F . (VERUM F_{1}()) = F_{3}() & ( for p being Element of QC-WFF F_{1}() holds

( ( p is atomic implies F . p = F_{4}(p) ) & ( p is negative implies F . p = F_{5}((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F_{6}((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F_{7}((F . (the_scope_of p)),p) ) ) ) )

( F . (VERUM F

( ( p is atomic implies F . p = F

proof end;

scheme :: CQC_SIM1:sch 2

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

CQCF2FuncEx{ F

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

( F . (VERUM F_{1}()) = F_{4}() & ( for k being 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) ) & ( for r, s being Element of CQC-WFF F_{1}()

for x being Element of bound_QC-variables F_{1}() holds

( F . ('not' r) = F_{6}((F . r),r) & F . (r '&' s) = F_{7}((F . r),(F . s),r,s) & F . (All (x,r)) = F_{8}(x,(F . r),r) ) ) )

( F . (VERUM F

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

for x being Element of bound_QC-variables F

( F . ('not' r) = F

proof end;

scheme :: CQC_SIM1:sch 3

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

provided

CQCF2FUniq{ F

provided

A1:
F_{4}() . (VERUM F_{1}()) = F_{6}()
and

A2: for k being Nat

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

for P being QC-pred_symbol of k,F_{1}() holds F_{4}() . (P ! ll) = F_{7}(k,P,ll)
and

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

for x being Element of bound_QC-variables F_{1}() holds

( F_{4}() . ('not' r) = F_{8}((F_{4}() . r),r) & F_{4}() . (r '&' s) = F_{9}((F_{4}() . r),(F_{4}() . s),r,s) & F_{4}() . (All (x,r)) = F_{10}(x,(F_{4}() . r),r) )
and

A4: F_{5}() . (VERUM F_{1}()) = F_{6}()
and

A5: for k being Nat

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

for P being QC-pred_symbol of k,F_{1}() holds F_{5}() . (P ! ll) = F_{7}(k,P,ll)
and

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

for x being Element of bound_QC-variables F_{1}() holds

( F_{5}() . ('not' r) = F_{8}((F_{5}() . r),r) & F_{5}() . (r '&' s) = F_{9}((F_{5}() . r),(F_{5}() . s),r,s) & F_{5}() . (All (x,r)) = F_{10}(x,(F_{5}() . r),r) )

A2: for k being Nat

for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

A3: for r, s being Element of CQC-WFF F

for x being Element of bound_QC-variables F

( F

A4: F

A5: for k being Nat

for ll being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

A6: for r, s being Element of CQC-WFF F

for x being Element of bound_QC-variables F

( F

proof end;

theorem Th11: :: CQC_SIM1:11

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( p is_subformula_of p '&' q & q is_subformula_of p '&' q )

for p, q being Element of CQC-WFF A holds

( p is_subformula_of p '&' q & q is_subformula_of p '&' q )

proof end;

theorem Th12: :: CQC_SIM1:12

for A being QC-alphabet

for p being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds p is_subformula_of All (x,p)

for p being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds p is_subformula_of All (x,p)

proof end;

theorem Th13: :: CQC_SIM1:13

for A being QC-alphabet

for k being Nat

for l being CQC-variable_list of k,A

for i being Nat st 1 <= i & i <= len l holds

l . i in bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for i being Nat st 1 <= i & i <= len l holds

l . i in bound_QC-variables A

proof end;

definition

let A be QC-alphabet ;

let D be non empty set ;

let f be Function of D,(CQC-WFF A);

ex b_{1} being Element of Funcs (D,(CQC-WFF A)) st

for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

b_{1} . a = 'not' p

for b_{1}, b_{2} being Element of Funcs (D,(CQC-WFF A)) st ( for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

b_{1} . a = 'not' p ) & ( for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

b_{2} . a = 'not' p ) holds

b_{1} = b_{2}

end;
let D be non empty set ;

let f be Function of D,(CQC-WFF A);

func NEGATIVE f -> Element of Funcs (D,(CQC-WFF A)) means :Def2: :: CQC_SIM1:def 2

for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

it . a = 'not' p;

existence for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

it . a = 'not' p;

ex b

for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

b

proof end;

uniqueness for b

for p being Element of CQC-WFF A st p = f . a holds

b

for p being Element of CQC-WFF A st p = f . a holds

b

b

proof end;

:: deftheorem Def2 defines NEGATIVE CQC_SIM1:def 2 :

for A being QC-alphabet

for D being non empty set

for f being Function of D,(CQC-WFF A)

for b_{4} being Element of Funcs (D,(CQC-WFF A)) holds

( b_{4} = NEGATIVE f iff for a being Element of D

for p being Element of CQC-WFF A st p = f . a holds

b_{4} . a = 'not' p );

for A being QC-alphabet

for D being non empty set

for f being Function of D,(CQC-WFF A)

for b

( b

for p being Element of CQC-WFF A st p = f . a holds

b

definition

let A be QC-alphabet ;

let f, g be Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A);

let n be Nat;

ex b_{1} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b_{1} . (t,h) = p '&' q

for b_{1}, b_{2} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st ( for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b_{1} . (t,h) = p '&' q ) & ( for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b_{2} . (t,h) = p '&' q ) holds

b_{1} = b_{2}

end;
let f, g be Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A);

let n be Nat;

func CON (f,g,n) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) means :Def3: :: CQC_SIM1:def 3

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

it . (t,h) = p '&' q;

existence for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

it . (t,h) = p '&' q;

ex b

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b

proof end;

uniqueness for b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b

b

proof end;

:: deftheorem Def3 defines CON CQC_SIM1:def 3 :

for A being QC-alphabet

for f, g being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)

for n being Nat

for b_{5} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds

( b_{5} = CON (f,g,n) iff for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b_{5} . (t,h) = p '&' q );

for A being QC-alphabet

for f, g being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)

for n being Nat

for b

( b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p, q being Element of CQC-WFF A st p = f . (t,h) & q = g . ((t + n),h) holds

b

Lm1: for A being QC-alphabet

for t being QC-symbol of A

for x being Element of bound_QC-variables A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds h +* (x .--> (x. t)) is Function of (bound_QC-variables A),(bound_QC-variables A)

proof end;

definition

let A be QC-alphabet ;

let f be Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A);

let x be bound_QC-variable of A;

ex b_{1} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b_{1} . (t,h) = All ((x. t),p)

for b_{1}, b_{2} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st ( for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b_{1} . (t,h) = All ((x. t),p) ) & ( for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b_{2} . (t,h) = All ((x. t),p) ) holds

b_{1} = b_{2}

end;
let f be Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A);

let x be bound_QC-variable of A;

func UNIVERSAL (x,f) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) means :Def4: :: CQC_SIM1:def 4

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

it . (t,h) = All ((x. t),p);

existence for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

it . (t,h) = All ((x. t),p);

ex b

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b

proof end;

uniqueness for b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b

b

proof end;

:: deftheorem Def4 defines UNIVERSAL CQC_SIM1:def 4 :

for A being QC-alphabet

for f being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)

for x being bound_QC-variable of A

for b_{4} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds

( b_{4} = UNIVERSAL (x,f) iff for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b_{4} . (t,h) = All ((x. t),p) );

for A being QC-alphabet

for f being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)

for x being bound_QC-variable of A

for b

( b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds

b

Lm2: for A being QC-alphabet

for k being Nat

for f being CQC-variable_list of k,A holds f is FinSequence of bound_QC-variables A

proof end;

definition

let A be QC-alphabet ;

let k be Nat;

let l be CQC-variable_list of k,A;

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A));

:: original: *

redefine func f * l -> CQC-variable_list of k,A;

coherence

l * f is CQC-variable_list of k,A

end;
let k be Nat;

let l be CQC-variable_list of k,A;

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A));

:: original: *

redefine func f * l -> CQC-variable_list of k,A;

coherence

l * f is CQC-variable_list of k,A

proof end;

definition

let A be QC-alphabet ;

let k be Nat;

let P be QC-pred_symbol of k,A;

let l be CQC-variable_list of k,A;

ex b_{1} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b_{1} . (t,h) = P ! (h * l)

for b_{1}, b_{2} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) st ( for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b_{1} . (t,h) = P ! (h * l) ) & ( for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b_{2} . (t,h) = P ! (h * l) ) holds

b_{1} = b_{2}

end;
let k be Nat;

let P be QC-pred_symbol of k,A;

let l be CQC-variable_list of k,A;

func ATOMIC (P,l) -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) means :Def5: :: CQC_SIM1:def 5

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds it . (t,h) = P ! (h * l);

existence for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds it . (t,h) = P ! (h * l);

ex b

for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b

proof end;

uniqueness for b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b

b

proof end;

:: deftheorem Def5 defines ATOMIC CQC_SIM1:def 5 :

for A being QC-alphabet

for k being Nat

for P being QC-pred_symbol of k,A

for l being CQC-variable_list of k,A

for b_{5} being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds

( b_{5} = ATOMIC (P,l) iff for t being QC-symbol of A

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b_{5} . (t,h) = P ! (h * l) );

for A being QC-alphabet

for k being Nat

for P being QC-pred_symbol of k,A

for l being CQC-variable_list of k,A

for b

( b

for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds b

deffunc H

deffunc H

deffunc H

deffunc H

definition

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

existence

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

( b_{1} = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) );

uniqueness

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

( b_{1} = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) & ex F being Function of (CQC-WFF A),NAT st

( b_{2} = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) holds

b_{1} = b_{2};

end;
let p be Element of CQC-WFF A;

func QuantNbr p -> Element of NAT means :Def6: :: CQC_SIM1:def 6

ex F being Function of (CQC-WFF A),NAT st

( it = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) );

correctness ex F being Function of (CQC-WFF A),NAT st

( it = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) );

existence

ex b

( b

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) );

uniqueness

for b

( b

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) & ex F being Function of (CQC-WFF A),NAT st

( b

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) holds

b

proof end;

:: deftheorem Def6 defines QuantNbr CQC_SIM1:def 6 :

for A being QC-alphabet

for p being Element of CQC-WFF A

for b_{3} being Element of NAT holds

( b_{3} = QuantNbr p iff ex F being Function of (CQC-WFF A),NAT st

( b_{3} = F . p & F . (VERUM A) = 0 & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) );

for A being QC-alphabet

for p being Element of CQC-WFF A

for b

( b

( b

for x being Element of bound_QC-variables A

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds

( F . (P ! l) = 0 & F . ('not' r) = F . r & F . (r '&' s) = (F . r) + (F . s) & F . (All (x,r)) = (F . r) + 1 ) ) ) );

definition

let A be QC-alphabet ;

let f be Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)));

let x be Element of CQC-WFF A;

:: original: .

redefine func f . x -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A));

coherence

f . x is Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))

end;
let f be Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)));

let x be Element of CQC-WFF A;

:: original: .

redefine func f . x -> Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A));

coherence

f . x is Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))

proof end;

definition

let A be QC-alphabet ;

ex b_{1} being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st

( b_{1} . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b_{1} . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds

( b_{1} . ('not' r) = NEGATIVE (b_{1} . r) & b_{1} . (r '&' s) = CON ((b_{1} . r),(b_{1} . s),(QuantNbr r)) & b_{1} . (All (x,r)) = UNIVERSAL (x,(b_{1} . r)) ) ) )

for b_{1}, b_{2} being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st b_{1} . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b_{1} . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds

( b_{1} . ('not' r) = NEGATIVE (b_{1} . r) & b_{1} . (r '&' s) = CON ((b_{1} . r),(b_{1} . s),(QuantNbr r)) & b_{1} . (All (x,r)) = UNIVERSAL (x,(b_{1} . r)) ) ) & b_{2} . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b_{2} . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds

( b_{2} . ('not' r) = NEGATIVE (b_{2} . r) & b_{2} . (r '&' s) = CON ((b_{2} . r),(b_{2} . s),(QuantNbr r)) & b_{2} . (All (x,r)) = UNIVERSAL (x,(b_{2} . r)) ) ) holds

b_{1} = b_{2}

end;
func SepFunc A -> Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) means :Def7: :: CQC_SIM1:def 7

( it . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds it . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds

( it . ('not' r) = NEGATIVE (it . r) & it . (r '&' s) = CON ((it . r),(it . s),(QuantNbr r)) & it . (All (x,r)) = UNIVERSAL (x,(it . r)) ) ) );

existence ( it . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds it . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds

( it . ('not' r) = NEGATIVE (it . r) & it . (r '&' s) = CON ((it . r),(it . s),(QuantNbr r)) & it . (All (x,r)) = UNIVERSAL (x,(it . r)) ) ) );

ex b

( b

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b

for x being Element of bound_QC-variables A holds

( b

proof end;

uniqueness for b

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b

for x being Element of bound_QC-variables A holds

( b

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b

for x being Element of bound_QC-variables A holds

( b

b

proof end;

:: deftheorem Def7 defines SepFunc CQC_SIM1:def 7 :

for A being QC-alphabet

for b_{2} being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) holds

( b_{2} = SepFunc A iff ( b_{2} . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b_{2} . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds

( b_{2} . ('not' r) = NEGATIVE (b_{2} . r) & b_{2} . (r '&' s) = CON ((b_{2} . r),(b_{2} . s),(QuantNbr r)) & b_{2} . (All (x,r)) = UNIVERSAL (x,(b_{2} . r)) ) ) ) );

for A being QC-alphabet

for b

( b

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds b

for x being Element of bound_QC-variables A holds

( b

definition

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

let t be QC-symbol of A;

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A));

correctness

coherence

((SepFunc A) . p) . [t,f] is Element of CQC-WFF A;

;

end;
let p be Element of CQC-WFF A;

let t be QC-symbol of A;

let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A));

correctness

coherence

((SepFunc A) . p) . [t,f] is Element of CQC-WFF A;

;

:: deftheorem defines SepFunc CQC_SIM1:def 8 :

for A being QC-alphabet

for p being Element of CQC-WFF A

for t being QC-symbol of A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds SepFunc (p,t,f) = ((SepFunc A) . p) . [t,f];

for A being QC-alphabet

for p being Element of CQC-WFF A

for t being QC-symbol of A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) holds SepFunc (p,t,f) = ((SepFunc A) . p) . [t,f];

theorem :: CQC_SIM1:15

for A being QC-alphabet

for k being Nat

for ll being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0

for k being Nat

for ll being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0

proof end;

theorem :: CQC_SIM1:17

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds QuantNbr (p '&' q) = (QuantNbr p) + (QuantNbr q)

for p, q being Element of CQC-WFF A holds QuantNbr (p '&' q) = (QuantNbr p) + (QuantNbr q)

proof end;

theorem :: CQC_SIM1:18

for A being QC-alphabet

for p being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds QuantNbr (All (x,p)) = (QuantNbr p) + 1

for p being Element of CQC-WFF A

for x being Element of bound_QC-variables A holds QuantNbr (All (x,p)) = (QuantNbr p) + 1

proof end;

scheme :: CQC_SIM1:sch 4

MaxFinDomElem{ F_{1}() -> non empty set , F_{2}() -> set , P_{1}[ object , object ] } :

MaxFinDomElem{ F

ex x being Element of F_{1}() st

( x in F_{2}() & ( for y being Element of F_{1}() st y in F_{2}() holds

P_{1}[x,y] ) )

provided( x in F

P

A1:
( F_{2}() is finite & F_{2}() <> {} & F_{2}() c= F_{1}() )
and

A2: for x, y being Element of F_{1}() holds

( P_{1}[x,y] or P_{1}[y,x] )
and

A3: for x, y, z being Element of F_{1}() st P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]

A2: for x, y being Element of F

( P

A3: for x, y, z being Element of F

P

proof end;

definition

let X be set ;

:: original: id

redefine func id X -> Element of Funcs (X,X);

coherence

id X is Element of Funcs (X,X)

end;
:: original: id

redefine func id X -> Element of Funcs (X,X);

coherence

id X is Element of Funcs (X,X)

proof end;

definition

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

{ t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds

not x. u in still_not-bound_in p } is Subset of (QC-symbols A)

end;
let p be Element of CQC-WFF A;

func NBI p -> Subset of (QC-symbols A) equals :: CQC_SIM1:def 9

{ t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds

not x. u in still_not-bound_in p } ;

coherence { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds

not x. u in still_not-bound_in p } ;

{ t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds

not x. u in still_not-bound_in p } is Subset of (QC-symbols A)

proof end;

:: deftheorem defines NBI CQC_SIM1:def 9 :

for A being QC-alphabet

for p being Element of CQC-WFF A holds NBI p = { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds

not x. u in still_not-bound_in p } ;

for A being QC-alphabet

for p being Element of CQC-WFF A holds NBI p = { t where t is QC-symbol of A : for u being QC-symbol of A st t <= u holds

not x. u in still_not-bound_in p } ;

registration
end;

definition
end;

:: deftheorem defines index CQC_SIM1:def 10 :

for A being QC-alphabet

for p being Element of CQC-WFF A holds index p = min (NBI p);

for A being QC-alphabet

for p being Element of CQC-WFF A holds index p = min (NBI p);

theorem Th21: :: CQC_SIM1:21

for A being QC-alphabet

for t being QC-symbol of A

for p being Element of CQC-WFF A st x. t in still_not-bound_in p holds

t < index p

for t being QC-symbol of A

for p being Element of CQC-WFF A st x. t in still_not-bound_in p holds

t < index p

proof end;

theorem :: CQC_SIM1:24

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( index p <= index (p '&' q) & index q <= index (p '&' q) )

for p, q being Element of CQC-WFF A holds

( index p <= index (p '&' q) & index q <= index (p '&' q) )

proof end;

definition

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

SepFunc (p,(index p),(id (bound_QC-variables A))) is Element of CQC-WFF A ;

end;
let p be Element of CQC-WFF A;

func SepVar p -> Element of CQC-WFF A equals :: CQC_SIM1:def 11

SepFunc (p,(index p),(id (bound_QC-variables A)));

coherence SepFunc (p,(index p),(id (bound_QC-variables A)));

SepFunc (p,(index p),(id (bound_QC-variables A))) is Element of CQC-WFF A ;

:: deftheorem defines SepVar CQC_SIM1:def 11 :

for A being QC-alphabet

for p being Element of CQC-WFF A holds SepVar p = SepFunc (p,(index p),(id (bound_QC-variables A)));

for A being QC-alphabet

for p being Element of CQC-WFF A holds SepVar p = SepFunc (p,(index p),(id (bound_QC-variables A)));

scheme :: CQC_SIM1:sch 5

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

provided

CQCInd{ F

provided

A1:
P_{1}[ VERUM F_{1}()]
and

A2: for k being Nat

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

for P being QC-pred_symbol of k,F_{1}() holds P_{1}[P ! l]
and

A3: for r being Element of CQC-WFF F_{1}() st P_{1}[r] holds

P_{1}[ 'not' r]
and

A4: for r, s being Element of CQC-WFF F_{1}() st P_{1}[r] & P_{1}[s] holds

P_{1}[r '&' s]
and

A5: for r being Element of CQC-WFF F_{1}()

for x being bound_QC-variable of F_{1}() st P_{1}[r] holds

P_{1}[ All (x,r)]

A2: for k being Nat

for l being CQC-variable_list of k,F

for P being QC-pred_symbol of k,F

A3: for r being Element of CQC-WFF F

P

A4: for r, s being Element of CQC-WFF F

P

A5: for r being Element of CQC-WFF F

for x being bound_QC-variable of F

P

proof end;

theorem Th26: :: CQC_SIM1:26

for A being QC-alphabet

for k being Nat

for ll being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds SepVar (P ! ll) = P ! ll

for k being Nat

for ll being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds SepVar (P ! ll) = P ! ll

proof end;

theorem :: CQC_SIM1:29

for A being QC-alphabet

for p, q being Element of CQC-WFF A st p is negative & q = the_argument_of p holds

SepVar p = 'not' (SepVar q)

for p, q being Element of CQC-WFF A st p is negative & q = the_argument_of p holds

SepVar p = 'not' (SepVar q)

proof end;

definition

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

let X be Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):];

end;
let p be Element of CQC-WFF A;

let X be Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):];

pred X is_Sep-closed_on p means :: CQC_SIM1:def 12

( [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in X holds

[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds

( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) );

( [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in X holds

[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds

( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) );

:: deftheorem defines is_Sep-closed_on CQC_SIM1:def 12 :

for A being QC-alphabet

for p being Element of CQC-WFF A

for X being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds

( X is_Sep-closed_on p iff ( [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in X holds

[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds

( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) ) );

for A being QC-alphabet

for p being Element of CQC-WFF A

for X being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds

( X is_Sep-closed_on p iff ( [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in X & ( for q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in X holds

[q,t,K,f] in X ) & ( for q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in X holds

( [q,t,K,f] in X & [r,(t + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in X holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in X ) ) );

definition

let A be QC-alphabet ;

let p be Element of CQC-WFF A;

ex b_{1} being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st

( b_{1} is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds

b_{1} c= D ) )

for b_{1}, b_{2} being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st b_{1} is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds

b_{1} c= D ) & b_{2} is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds

b_{2} c= D ) holds

b_{1} = b_{2}
;

end;
let p be Element of CQC-WFF A;

func SepQuadruples p -> Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] means :Def13: :: CQC_SIM1:def 13

( it is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds

it c= D ) );

existence ( it is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

:: deftheorem Def13 defines SepQuadruples CQC_SIM1:def 13 :

for A being QC-alphabet

for p being Element of CQC-WFF A

for b_{3} being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds

( b_{3} = SepQuadruples p iff ( b_{3} is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds

b_{3} c= D ) ) );

for A being QC-alphabet

for p being Element of CQC-WFF A

for b

( b

b

theorem Th30: :: CQC_SIM1:30

for A being QC-alphabet

for p being Element of CQC-WFF A holds [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in SepQuadruples p

for p being Element of CQC-WFF A holds [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] in SepQuadruples p

proof end;

theorem Th31: :: CQC_SIM1:31

for A being QC-alphabet

for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in SepQuadruples p holds

[q,t,K,f] in SepQuadruples p

for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [('not' q),t,K,f] in SepQuadruples p holds

[q,t,K,f] in SepQuadruples p

proof end;

theorem Th32: :: CQC_SIM1:32

for A being QC-alphabet

for p, q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p holds

( [q,t,K,f] in SepQuadruples p & [r,(t + (QuantNbr q)),K,f] in SepQuadruples p )

for p, q, r being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(q '&' r),t,K,f] in SepQuadruples p holds

( [q,t,K,f] in SepQuadruples p & [r,(t + (QuantNbr q)),K,f] in SepQuadruples p )

proof end;

theorem Th33: :: CQC_SIM1:33

for A being QC-alphabet

for p, q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in SepQuadruples p

for p, q being Element of CQC-WFF A

for x being Element of bound_QC-variables A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [(All (x,q)),t,K,f] in SepQuadruples p holds

[q,(t ++),(K \/ {x}),(f +* (x .--> (x. t)))] in SepQuadruples p

proof end;

theorem Th34: :: CQC_SIM1:34

for A being QC-alphabet

for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) holds

( not [q,t,K,f] in SepQuadruples p or [q,t,K,f] = [p,(index p),({}. (bound_QC-variables A)),(id (bound_QC-variables A))] or [('not' q),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A st [(q '&' r),t,K,f] in SepQuadruples p or ex r being Element of CQC-WFF A ex u being QC-symbol of A st

( t = u + (QuantNbr r) & [(r '&' q),u,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables A ex u being QC-symbol of A ex h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st

( u ++ = t & h +* ({x} --> (x. u)) = f & ( [(All (x,q)),u,K,h] in SepQuadruples p or [(All (x,q)),u,(K \ {x}),h] in SepQuadruples p ) ) )

proof end;

scheme :: CQC_SIM1:sch 6

Sepregression{ F_{1}() -> QC-alphabet , F_{2}() -> Element of CQC-WFF F_{1}(), P_{1}[ object , object , object , object ] } :

Sepregression{ F

for q being Element of CQC-WFF F_{1}()

for t being QC-symbol of F_{1}()

for K being Element of Fin (bound_QC-variables F_{1}())

for f being Element of Funcs ((bound_QC-variables F_{1}()),(bound_QC-variables F_{1}())) st [q,t,K,f] in SepQuadruples F_{2}() holds

P_{1}[q,t,K,f]

providedfor t being QC-symbol of F

for K being Element of Fin (bound_QC-variables F

for f being Element of Funcs ((bound_QC-variables F

P

A1:
P_{1}[F_{2}(), index F_{2}(), {}. (bound_QC-variables F_{1}()), id (bound_QC-variables F_{1}())]
and

A2: for q being Element of CQC-WFF F_{1}()

for t being QC-symbol of F_{1}()

for K being Element of Fin (bound_QC-variables F_{1}())

for f being Element of Funcs ((bound_QC-variables F_{1}()),(bound_QC-variables F_{1}())) st [('not' q),t,K,f] in SepQuadruples F_{2}() & P_{1}[ 'not' q,t,K,f] holds

P_{1}[q,t,K,f]
and

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

for t being QC-symbol of F_{1}()

for K being Element of Fin (bound_QC-variables F_{1}())

for f being Element of Funcs ((bound_QC-variables F_{1}()),(bound_QC-variables F_{1}())) st [(q '&' r),t,K,f] in SepQuadruples F_{2}() & P_{1}[q '&' r,t,K,f] holds

( P_{1}[q,t,K,f] & P_{1}[r,t + (QuantNbr q),K,f] )
and

A4: for q being Element of CQC-WFF F_{1}()

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

for t being QC-symbol of F_{1}()

for K being Element of Fin (bound_QC-variables F_{1}())

for f being Element of Funcs ((bound_QC-variables F_{1}()),(bound_QC-variables F_{1}())) st [(All (x,q)),t,K,f] in SepQuadruples F_{2}() & P_{1}[ All (x,q),t,K,f] holds

P_{1}[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

A2: for q being Element of CQC-WFF F

for t being QC-symbol of F

for K being Element of Fin (bound_QC-variables F

for f being Element of Funcs ((bound_QC-variables F

P

A3: for q, r being Element of CQC-WFF F

for t being QC-symbol of F

for K being Element of Fin (bound_QC-variables F

for f being Element of Funcs ((bound_QC-variables F

( P

A4: for q being Element of CQC-WFF F

for x being bound_QC-variable of F

for t being QC-symbol of F

for K being Element of Fin (bound_QC-variables F

for f being Element of Funcs ((bound_QC-variables F

P

proof end;

theorem Th35: :: CQC_SIM1:35

for A being QC-alphabet

for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

q is_subformula_of p

for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

q is_subformula_of p

proof end;

theorem :: CQC_SIM1:36

for A being QC-alphabet holds SepQuadruples (VERUM A) = {[(VERUM A),(0 A),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}

proof end;

theorem :: CQC_SIM1:37

for A being QC-alphabet

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}

for k being Nat

for l being CQC-variable_list of k,A

for P being QC-pred_symbol of k,A holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. (bound_QC-variables A)),(id (bound_QC-variables A))]}

proof end;

theorem Th38: :: CQC_SIM1:38

for A being QC-alphabet

for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

still_not-bound_in q c= (still_not-bound_in p) \/ K

for p, q being Element of CQC-WFF A

for t being QC-symbol of A

for K being Element of Fin (bound_QC-variables A)

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) st [q,t,K,f] in SepQuadruples p holds

still_not-bound_in q c= (still_not-bound_in p) \/ K

proof end;

theorem Th39: :: CQC_SIM1:39

for A being QC-alphabet

for t, u being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds

u < t

for t, u being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds

u < t

proof end;

theorem :: CQC_SIM1:40

for A being QC-alphabet

for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds

not x. t in f .: K

for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds

not x. t in f .: K

proof end;

theorem Th41: :: CQC_SIM1:41

for A being QC-alphabet

for t, u being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in p) holds

u < t

for t, u being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in p) holds

u < t

proof end;

theorem Th42: :: CQC_SIM1:42

for A being QC-alphabet

for t, u being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds

u < t

for t, u being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds

u < t

proof end;

theorem Th43: :: CQC_SIM1:43

for A being QC-alphabet

for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds

not x. t in f .: (still_not-bound_in q)

for t being QC-symbol of A

for p, q being Element of CQC-WFF A

for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))

for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds

not x. t in f .: (still_not-bound_in q)

proof end;

theorem Th44: :: CQC_SIM1:44

for A being QC-alphabet

for p being Element of CQC-WFF A holds still_not-bound_in p = still_not-bound_in (SepVar p)

for p being Element of CQC-WFF A holds still_not-bound_in p = still_not-bound_in (SepVar p)

proof end;

definition

let A be QC-alphabet ;

let p, q be Element of CQC-WFF A;

reflexivity

for p being Element of CQC-WFF A holds SepVar p = SepVar p ;

symmetry

for p, q being Element of CQC-WFF A st SepVar p = SepVar q holds

SepVar q = SepVar p ;

end;
let p, q be Element of CQC-WFF A;

reflexivity

for p being Element of CQC-WFF A holds SepVar p = SepVar p ;

symmetry

for p, q being Element of CQC-WFF A st SepVar p = SepVar q holds

SepVar q = SepVar p ;

:: deftheorem defines are_similar CQC_SIM1:def 14 :

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( p,q are_similar iff SepVar p = SepVar q );

for A being QC-alphabet

for p, q being Element of CQC-WFF A holds

( p,q are_similar iff SepVar p = SepVar q );

theorem :: CQC_SIM1:46

for A being QC-alphabet

for p, q, r being Element of CQC-WFF A st p,q are_similar & q,r are_similar holds

p,r are_similar ;

for p, q, r being Element of CQC-WFF A st p,q are_similar & q,r are_similar holds

p,r are_similar ;