:: Similarity of Formulae
:: by Agata Darmochwa{\l} and Andrzej Trybulec
::
:: Received November 22, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users

definition

let A be QC-alphabet ;
let b be bound_QC-variable of A;

func x. b -> QC-symbol of A means :Def1: :: CQC_SIM1:def 1
x. it = b;

existence
ex b₁ being QC-symbol of A st x. b₁ = b by QC_LANG3:30;
uniqueness
for b₁, b₂ being QC-symbol of A st x. b₁ = b & x. b₂ = b holds
b₁ = b₂ by XTUPLE_0:1;

end;

:: deftheorem Def1 defines x. CQC_SIM1:def 1 :
for A being QC-alphabet
for b being bound_QC-variable of A
for b₃ being QC-symbol of A holds
( b₃ = x. b iff x. b₃ = b );

theorem Th1: :: CQC_SIM1:1

for x, y being set
for f being Function holds Im ((f +* (x .--> y)),x) = {y}

proof end;

theorem Th2: :: CQC_SIM1:2

for K, L, x, y being set
for f being Function holds (f +* (L --> y)) .: K c= (f .: K) \/ {y}

proof end;

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

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}

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

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

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

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)

proof end;

theorem Th9: :: CQC_SIM1:9

for l being FinSequence holds rng l = { (l . i) where i is Nat : ( 1 <= i & i <= len l ) }

proof end;

scheme :: CQC_SIM1:sch 1
QCFuncExN{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Element of F₂(), F₄( object ) -> Element of F₂(), F₅( object , object ) -> Element of F₂(), F₆( object , object , object ) -> Element of F₂(), F₇( object , object ) -> Element of F₂() } :

ex F being Function of (QC-WFF F₁()),F₂() st
( F . (VERUM F₁()) = F₃() & ( for p being Element of QC-WFF F₁() holds
( ( p is atomic implies F . p = F₄(p) ) & ( p is negative implies F . p = F₅((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F₆((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F₇((F . (the_scope_of p)),p) ) ) ) )

proof end;

scheme :: CQC_SIM1:sch 2
CQCF2FuncEx{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> non empty set , F₄() -> Element of Funcs (F₂(),F₃()), F₅( object , object , object ) -> Element of Funcs (F₂(),F₃()), F₆( object , object ) -> Element of Funcs (F₂(),F₃()), F₇( object , object , object , object ) -> Element of Funcs (F₂(),F₃()), F₈( object , object , object ) -> Element of Funcs (F₂(),F₃()) } :

ex F being Function of (CQC-WFF F₁()),(Funcs (F₂(),F₃())) st
( F . (VERUM F₁()) = F₄() & ( for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds F . (P ! l) = F₅(k,P,l) ) & ( for r, s being Element of CQC-WFF F₁()
for x being Element of bound_QC-variables F₁() holds
( F . ('not' r) = F₆((F . r),r) & F . (r '&' s) = F₇((F . r),(F . s),r,s) & F . (All (x,r)) = F₈(x,(F . r),r) ) ) )

proof end;

scheme :: CQC_SIM1:sch 3
CQCF2FUniq{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> non empty set , F₄() -> Function of (CQC-WFF F₁()),(Funcs (F₂(),F₃())), F₅() -> Function of (CQC-WFF F₁()),(Funcs (F₂(),F₃())), F₆() -> Function of F₂(),F₃(), F₇( object , object , object ) -> Function of F₂(),F₃(), F₈( object , object ) -> Function of F₂(),F₃(), F₉( object , object , object , object ) -> Function of F₂(),F₃(), F₁₀( object , object , object ) -> Function of F₂(),F₃() } :

F₄() = F₅()

provided

A1: F₄() . (VERUM F₁()) = F₆() and
A2: for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds F₄() . (P ! ll) = F₇(k,P,ll) and
A3: for r, s being Element of CQC-WFF F₁()
for x being Element of bound_QC-variables F₁() holds
( F₄() . ('not' r) = F₈((F₄() . r),r) & F₄() . (r '&' s) = F₉((F₄() . r),(F₄() . s),r,s) & F₄() . (All (x,r)) = F₁₀(x,(F₄() . r),r) ) and
A4: F₅() . (VERUM F₁()) = F₆() and
A5: for k being Nat
for ll being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds F₅() . (P ! ll) = F₇(k,P,ll) and
A6: for r, s being Element of CQC-WFF F₁()
for x being Element of bound_QC-variables F₁() holds
( F₅() . ('not' r) = F₈((F₅() . r),r) & F₅() . (r '&' s) = F₉((F₅() . r),(F₅() . s),r,s) & F₅() . (All (x,r)) = F₁₀(x,(F₅() . r),r) )

proof end;

theorem Th10: :: CQC_SIM1:10

for A being QC-alphabet
for p being Element of CQC-WFF A holds p is_subformula_of 'not' p

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 )

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)

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

proof end;

definition

let A be QC-alphabet ;
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
ex b₁ 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₁ . a = 'not' p

proof end;

uniqueness
for b₁, b₂ 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₁ . a = 'not' p ) & ( for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
b₂ . a = 'not' p ) holds
b₁ = b₂

proof end;

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₄ being Element of Funcs (D,(CQC-WFF A)) holds
( b₄ = NEGATIVE f iff for a being Element of D
for p being Element of CQC-WFF A st p = f . a holds
b₄ . a = 'not' p );

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;

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
ex b₁ 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₁ . (t,h) = p '&' q

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₂ . (t,h) = p '&' q ) holds
b₁ = b₂

proof end;

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₅ being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b₅ = 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₅ . (t,h) = p '&' q );

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;

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
ex b₁ 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₁ . (t,h) = All ((x. t),p)

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₂ . (t,h) = All ((x. t),p) ) holds
b₁ = b₂

proof end;

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₄ being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b₄ = 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₄ . (t,h) = All ((x. t),p) );

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

proof end;

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;

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
ex b₁ 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₁ . (t,h) = P ! (h * l)

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₂ . (t,h) = P ! (h * l) ) holds
b₁ = b₂

proof end;

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₅ being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b₅ = 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₅ . (t,h) = P ! (h * l) );

deffunc H₁( set , set , set ) -> Element of NAT = 0 ;

deffunc H₂( Element of NAT ) -> Element of NAT = $1;

deffunc H₃( Element of NAT , Element of NAT ) -> Element of NAT = $1 + $2;

deffunc H₄( set , Element of NAT ) -> Element of NAT = $2 + 1;

definition

let A be QC-alphabet ;
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
existence
ex b₁ being Element of NAT ex F being Function of (CQC-WFF A),NAT st
( b₁ = 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₁, b₂ being Element of NAT st ex F being Function of (CQC-WFF A),NAT st
( b₁ = 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₂ = 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₁ = b₂;

proof end;

end;

:: deftheorem Def6 defines QuantNbr CQC_SIM1:def 6 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for b₃ being Element of NAT holds
( b₃ = QuantNbr p iff ex F being Function of (CQC-WFF A),NAT st
( b₃ = 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 ) ) ) );

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

proof end;

end;

definition

let A be QC-alphabet ;

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
ex b₁ being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st
( b₁ . (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₁ . (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₁ . ('not' r) = NEGATIVE (b₁ . r) & b₁ . (r '&' s) = CON ((b₁ . r),(b₁ . s),(QuantNbr r)) & b₁ . (All (x,r)) = UNIVERSAL (x,(b₁ . r)) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st b₁ . (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₁ . (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₁ . ('not' r) = NEGATIVE (b₁ . r) & b₁ . (r '&' s) = CON ((b₁ . r),(b₁ . s),(QuantNbr r)) & b₁ . (All (x,r)) = UNIVERSAL (x,(b₁ . r)) ) ) & b₂ . (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₂ . (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₂ . ('not' r) = NEGATIVE (b₂ . r) & b₂ . (r '&' s) = CON ((b₂ . r),(b₂ . s),(QuantNbr r)) & b₂ . (All (x,r)) = UNIVERSAL (x,(b₂ . r)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines SepFunc CQC_SIM1:def 7 :
for A being QC-alphabet
for b₂ being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) holds
( b₂ = SepFunc A iff ( b₂ . (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₂ . (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₂ . ('not' r) = NEGATIVE (b₂ . r) & b₂ . (r '&' s) = CON ((b₂ . r),(b₂ . s),(QuantNbr r)) & b₂ . (All (x,r)) = UNIVERSAL (x,(b₂ . r)) ) ) ) );

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

func SepFunc (p,t,f) -> Element of CQC-WFF A equals :: CQC_SIM1:def 8
((SepFunc A) . p) . [t,f];

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

end;

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

theorem :: CQC_SIM1:14

for A being QC-alphabet holds QuantNbr (VERUM A) = 0

proof end;

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

proof end;

theorem :: CQC_SIM1:16

for A being QC-alphabet
for p being Element of CQC-WFF A holds QuantNbr ('not' p) = QuantNbr p

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)

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

proof end;

theorem Th19: :: CQC_SIM1:19

for A being QC-alphabet
for p being Element of QC-WFF A holds still_not-bound_in p is finite

proof end;

scheme :: CQC_SIM1:sch 4
MaxFinDomElem{ F₁() -> non empty set , F₂() -> set , P₁[ object , object ] } :

ex x being Element of F₁() st
( x in F₂() & ( for y being Element of F₁() st y in F₂() holds
P₁[x,y] ) )

provided

A1: ( F₂() is finite & F₂() <> {} & F₂() c= F₁() ) and
A2: for x, y being Element of F₁() holds
( P₁[x,y] or P₁[y,x] ) and
A3: for x, y, z being Element of F₁() st P₁[x,y] & P₁[y,z] holds
P₁[x,z]

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)

proof end;

end;

definition

let A be QC-alphabet ;
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 } is Subset of (QC-symbols A)

proof end;

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

registration

let A be QC-alphabet ;
let p be Element of CQC-WFF A;

cluster NBI p -> non empty ;

coherence
not NBI p is empty

proof end;

end;

definition

let A be QC-alphabet ;
let p be Element of CQC-WFF A;

func index p -> QC-symbol of A equals :: CQC_SIM1:def 10
min (NBI p);

coherence
min (NBI p) is QC-symbol of A ;

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

theorem Th20: :: CQC_SIM1:20

for A being QC-alphabet
for p being Element of CQC-WFF A holds
( index p = 0 A iff p is closed )

proof end;

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

proof end;

theorem Th22: :: CQC_SIM1:22

for A being QC-alphabet holds index (VERUM A) = 0 A

proof end;

theorem Th23: :: CQC_SIM1:23

for A being QC-alphabet
for p being Element of CQC-WFF A holds index ('not' p) = 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) )

proof end;

definition

let A be QC-alphabet ;
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))) is Element of CQC-WFF A ;

end;

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

theorem :: CQC_SIM1:25

for A being QC-alphabet holds SepVar (VERUM A) = VERUM A

proof end;

scheme :: CQC_SIM1:sch 5
CQCInd{ F₁() -> QC-alphabet , P₁[ object ] } :

for r being Element of CQC-WFF F₁() holds P₁[r]

provided

A1: P₁[ VERUM F₁()] and
A2: for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds P₁[P ! l] and
A3: for r being Element of CQC-WFF F₁() st P₁[r] holds
P₁[ 'not' r] and
A4: for r, s being Element of CQC-WFF F₁() st P₁[r] & P₁[s] holds
P₁[r '&' s] and
A5: for r being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁() st P₁[r] holds
P₁[ All (x,r)]

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

proof end;

theorem :: CQC_SIM1:27

for A being QC-alphabet
for p being Element of CQC-WFF A st p is atomic holds
SepVar p = p

proof end;

theorem Th28: :: CQC_SIM1:28

for A being QC-alphabet
for p being Element of CQC-WFF A holds SepVar ('not' p) = 'not' (SepVar p)

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)

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

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

end;

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

definition

let A be QC-alphabet ;
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
ex b₁ 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₁ 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₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ 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₁ 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₁ c= D ) & b₂ 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₂ c= D ) holds
b₁ = b₂ ;

end;

:: deftheorem Def13 defines SepQuadruples CQC_SIM1:def 13 :
for A being QC-alphabet
for p being Element of CQC-WFF A
for b₃ 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₃ = SepQuadruples p iff ( b₃ 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₃ c= D ) ) );

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

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

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 )

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

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

proof end;

scheme :: CQC_SIM1:sch 6
Sepregression{ F₁() -> QC-alphabet , F₂() -> Element of CQC-WFF F₁(), P₁[ object , object , object , object ] } :

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₁()),(bound_QC-variables F₁())) st [q,t,K,f] in SepQuadruples F₂() holds
P₁[q,t,K,f]

provided

A1: P₁[F₂(), index F₂(), {}. (bound_QC-variables F₁()), id (bound_QC-variables F₁())] and
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₁()),(bound_QC-variables F₁())) st [('not' q),t,K,f] in SepQuadruples F₂() & P₁[ 'not' q,t,K,f] holds
P₁[q,t,K,f] and
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₁()),(bound_QC-variables F₁())) st [(q '&' r),t,K,f] in SepQuadruples F₂() & P₁[q '&' r,t,K,f] holds
( P₁[q,t,K,f] & P₁[r,t + (QuantNbr q),K,f] ) and
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₁()),(bound_QC-variables F₁())) st [(All (x,q)),t,K,f] in SepQuadruples F₂() & P₁[ All (x,q),t,K,f] holds
P₁[q,t ++ ,K \/ {x},f +* (x .--> (x. t))]

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

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

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

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

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

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

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

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)

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)

proof end;

theorem :: CQC_SIM1:45

for A being QC-alphabet
for p being Element of CQC-WFF A holds index p = index (SepVar p)

proof end;

definition

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

pred p,q are_similar means :: CQC_SIM1:def 14
SepVar p = SepVar q;

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;

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

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 ;