:: CQC_SIM1 semantic presentation

theorem Th1: :: CQC_SIM1:1

for b₁, b₂ being set
for b₃ being Function holds (b₃ +* ({b₁} --> b₂)) .: {b₁} = {b₂}

proof end;

theorem Th2: :: CQC_SIM1:2

for b₁, b₂, b₃, b₄ being set
for b₅ being Function holds (b₅ +* (b₂ --> b₄)) .: b₁ c= (b₅ .: b₁) \/ {b₄}

proof end;

theorem Th3: :: CQC_SIM1:3

for b₁, b₂ being set
for b₃ being Function
for b₄ being set holds (b₃ +* ({b₁} --> b₂)) .: (b₄ \ {b₁}) = b₃ .: (b₄ \ {b₁})

proof end;

theorem Th4: :: CQC_SIM1:4

for b₁, b₂ being set
for b₃ being Function
for b₄ being set st not b₂ in b₃ .: (b₄ \ {b₁}) holds
(b₃ +* ({b₁} --> b₂)) .: (b₄ \ {b₁}) = ((b₃ +* ({b₁} --> b₂)) .: b₄) \ {b₂}

proof end;

theorem Th5: :: CQC_SIM1:5

for b₁ being Element of CQC-WFF st b₁ is atomic holds
ex b₂ being Element of NAT ex b₃ being QC-pred_symbol of b₂ex b₄ being CQC-variable_list of b₂ st b₁ = b₃ ! b₄

proof end;

theorem Th6: :: CQC_SIM1:6

for b₁ being Element of CQC-WFF st b₁ is negative holds
ex b₂ being Element of CQC-WFF st b₁ = 'not' b₂

proof end;

theorem Th7: :: CQC_SIM1:7

for b₁ being Element of CQC-WFF st b₁ is conjunctive holds
ex b₂, b₃ being Element of CQC-WFF st b₁ = b₂ '&' b₃

proof end;

theorem Th8: :: CQC_SIM1:8

for b₁ being Element of CQC-WFF st b₁ is universal holds
ex b₂ being Element of bound_QC-variables ex b₃ being Element of CQC-WFF st b₁ = All b₂,b₃

proof end;

theorem Th9: :: CQC_SIM1:9

for b₁ being FinSequence holds rng b₁ = { (b₁ . b₂) where B is Element of NAT : ( 1 <= b₂ & b₂ <= len b₁ ) }

proof end;

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

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

proof end;

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

ex b₁ being Function of CQC-WFF , Funcs F₁(),F₂() st
( b₁ . VERUM = F₃() & ( for b₂ being Element of NAT
for b₃ being CQC-variable_list of b₂
for b₄ being QC-pred_symbol of b₂ holds b₁ . (b₄ ! b₃) = F₄(b₂,b₄,b₃) ) & ( for b₂, b₃ being Element of CQC-WFF
for b₄ being Element of bound_QC-variables holds
( b₁ . ('not' b₂) = F₅((b₁ . b₂),b₂) & b₁ . (b₂ '&' b₃) = F₆((b₁ . b₂),(b₁ . b₃),b₂,b₃) & b₁ . (All b₄,b₂) = F₇(b₄,(b₁ . b₂),b₂) ) ) )

proof end;

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

F₃() = F₄()

provided

E7: F₃() . VERUM = F₅() and
E8: for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds F₃() . (b₃ ! b₂) = F₆(b₁,b₃,b₂) and
E9: for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of bound_QC-variables holds
( F₃() . ('not' b₁) = F₇((F₃() . b₁),b₁) & F₃() . (b₁ '&' b₂) = F₈((F₃() . b₁),(F₃() . b₂),b₁,b₂) & F₃() . (All b₃,b₁) = F₉(b₃,(F₃() . b₁),b₁) ) and
E10: F₄() . VERUM = F₅() and
E11: for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds F₄() . (b₃ ! b₂) = F₆(b₁,b₃,b₂) and
E12: for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of bound_QC-variables holds
( F₄() . ('not' b₁) = F₇((F₄() . b₁),b₁) & F₄() . (b₁ '&' b₂) = F₈((F₄() . b₁),(F₄() . b₂),b₁,b₂) & F₄() . (All b₃,b₁) = F₉(b₃,(F₄() . b₁),b₁) )

proof end;

theorem Th10: :: CQC_SIM1:10

for b₁ being Element of CQC-WFF holds b₁ is_subformula_of 'not' b₁

proof end;

theorem Th11: :: CQC_SIM1:11

for b₁, b₂ being Element of CQC-WFF holds
( b₁ is_subformula_of b₁ '&' b₂ & b₂ is_subformula_of b₁ '&' b₂ )

proof end;

theorem Th12: :: CQC_SIM1:12

for b₁ being Element of CQC-WFF
for b₂ being Element of bound_QC-variables holds b₁ is_subformula_of All b₂,b₁

proof end;

theorem Th13: :: CQC_SIM1:13

for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being Element of NAT st 1 <= b₃ & b₃ <= len b₂ holds
b₂ . b₃ in bound_QC-variables

proof end;

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, CQC-WFF ;
func NEGATIVE c₂ -> Element of Funcs a₁,CQC-WFF means :Def1: :: CQC_SIM1:def 1
for b₁ being Element of a₁
for b₂ being Element of CQC-WFF st b₂ = a₂ . b₁ holds
a₃ . b₁ = 'not' b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines NEGATIVE CQC_SIM1:def 1 :

definition

let c₁, c₂ be Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):], CQC-WFF ;
let c₃ be Nat;
func CON c₁,c₂,c₃ -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def2: :: CQC_SIM1:def 2
for b₁ being Element of NAT
for b₂ being Element of Funcs bound_QC-variables ,bound_QC-variables
for b₃, b₄ being Element of CQC-WFF st b₃ = a₁ . [b₁,b₂] & b₄ = a₂ . [(b₁ + a₃),b₂] holds
a₄ . [b₁,b₂] = b₃ '&' b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines CON CQC_SIM1:def 2 :

Lemma13: for b₁ being Element of bound_QC-variables
for b₂ being Element of NAT
for b₃ being Element of Funcs bound_QC-variables ,bound_QC-variables holds b₃ +* ({b₁} --> (x. b₂)) is Function of bound_QC-variables , bound_QC-variables

proof end;

definition

let c₁ be Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):], CQC-WFF ;
let c₂ be bound_QC-variable;
func UNIVERSAL c₂,c₁ -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def3: :: CQC_SIM1:def 3
for b₁ being Element of NAT
for b₂ being Element of Funcs bound_QC-variables ,bound_QC-variables
for b₃ being Element of CQC-WFF st b₃ = a₁ . [(b₁ + 1),(b₂ +* ({a₂} --> (x. b₁)))] holds
a₃ . [b₁,b₂] = All (x. b₁),b₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines UNIVERSAL CQC_SIM1:def 3 :

Lemma15: for b₁ being Element of NAT
for b₂ being FinSequence of bound_QC-variables st len b₂ = b₁ holds
b₂ is CQC-variable_list of b₁

proof end;

Lemma16: for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁ holds b₂ is FinSequence of bound_QC-variables

proof end;

definition

let c₁ be Element of NAT ;
let c₂ be CQC-variable_list of c₁;
let c₃ be Element of Funcs bound_QC-variables ,bound_QC-variables ;
redefine func * as c₃ * c₂ -> CQC-variable_list of a₁;
coherence

proof end;

end;

definition

let c₁ be Element of NAT ;
let c₂ be QC-pred_symbol of c₁;
let c₃ be CQC-variable_list of c₁;
func ATOMIC c₂,c₃ -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def4: :: CQC_SIM1:def 4
for b₁ being Element of NAT
for b₂ being Element of Funcs bound_QC-variables ,bound_QC-variables holds a₄ . [b₁,b₂] = a₂ ! (b₂ * a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines ATOMIC CQC_SIM1:def 4 :

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

deffunc H₂( Element of NAT ) -> Element of NAT = a₁;

deffunc H₃( Element of NAT , Element of NAT ) -> Element of NAT = a₁ + a₂;

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

definition

let c₁ be Element of CQC-WFF ;
func QuantNbr c₁ -> Element of NAT means :Def5: :: CQC_SIM1:def 5
ex b₁ being Function of CQC-WFF , NAT st
( a₂ = b₁ . a₁ & b₁ . VERUM = 0 & ( for b₂, b₃ being Element of CQC-WFF
for b₄ being Element of bound_QC-variables
for b₅ being Element of NAT
for b₆ being CQC-variable_list of b₅
for b₇ being QC-pred_symbol of b₅ holds
( b₁ . (b₇ ! b₆) = 0 & b₁ . ('not' b₂) = b₁ . b₂ & b₁ . (b₂ '&' b₃) = (b₁ . b₂) + (b₁ . b₃) & b₁ . (All b₄,b₂) = (b₁ . b₂) + 1 ) ) );
correctness

proof end;

end;

:: deftheorem Def5 defines QuantNbr CQC_SIM1:def 5 :

definition

let c₁ be Function of CQC-WFF , Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ;
let c₂ be Element of CQC-WFF ;
redefine func . as c₁ . c₂ -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ;
coherence

proof end;

end;

definition

func SepFunc -> Function of CQC-WFF , Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def6: :: CQC_SIM1:def 6
( a₁ . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds a₁ . (b₃ ! b₂) = ATOMIC b₃,b₂ ) & ( for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of bound_QC-variables holds
( a₁ . ('not' b₁) = NEGATIVE (a₁ . b₁) & a₁ . (b₁ '&' b₂) = CON (a₁ . b₁),(a₁ . b₂),(QuantNbr b₁) & a₁ . (All b₃,b₁) = UNIVERSAL b₃,(a₁ . b₁) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines SepFunc CQC_SIM1:def 6 :

definition

let c₁ be Element of CQC-WFF ;
let c₂ be Element of NAT ;
let c₃ be Element of Funcs bound_QC-variables ,bound_QC-variables ;
func SepFunc c₁,c₂,c₃ -> Element of CQC-WFF equals :: CQC_SIM1:def 7
(SepFunc . a₁) . [a₂,a₃];
correctness ;

end;

:: deftheorem Def7 defines SepFunc CQC_SIM1:def 7 :

deffunc H₅( Element of CQC-WFF ) -> Element of NAT = QuantNbr a₁;

theorem Th14: :: CQC_SIM1:14

QuantNbr VERUM = 0

proof end;

theorem Th15: :: CQC_SIM1:15

for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds QuantNbr (b₃ ! b₂) = 0

proof end;

theorem Th16: :: CQC_SIM1:16

for b₁ being Element of CQC-WFF holds QuantNbr ('not' b₁) = QuantNbr b₁

proof end;

theorem Th17: :: CQC_SIM1:17

for b₁, b₂ being Element of CQC-WFF holds QuantNbr (b₁ '&' b₂) = (QuantNbr b₁) + (QuantNbr b₂)

proof end;

theorem Th18: :: CQC_SIM1:18

for b₁ being Element of CQC-WFF
for b₂ being Element of bound_QC-variables holds QuantNbr (All b₂,b₁) = (QuantNbr b₁) + 1

proof end;

definition

let c₁ be non empty Subset of NAT ;
func min c₁ -> Nat means :Def8: :: CQC_SIM1:def 8
( a₂ in a₁ & ( for b₁ being Element of NAT st b₁ in a₁ holds
a₂ <= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines min CQC_SIM1:def 8 :

theorem Th19: :: CQC_SIM1:19

for b₁, b₂ being non empty Subset of NAT st b₁ c= b₂ holds
min b₂ <= min b₁

proof end;

theorem Th20: :: CQC_SIM1:20

for b₁ being Element of QC-WFF holds still_not-bound_in b₁ is finite

proof end;

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

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

provided

E23: ( F₂() is finite & F₂() <> {} & F₂() c= F₁() ) and
E24: for b₁, b₂ being Element of F₁() holds
( P₁[b₁,b₂] or P₁[b₂,b₁] ) and
E25: for b₁, b₂, b₃ being Element of F₁() st P₁[b₁,b₂] & P₁[b₂,b₃] holds
P₁[b₁,b₃]

proof end;

definition

let c₁ be Element of CQC-WFF ;
func NBI c₁ -> Subset of NAT equals :: CQC_SIM1:def 9
{ b₁ where B is Element of NAT : for b₁ being Element of NAT st b₁ <= b₂ holds
not x. b₂ in still_not-bound_in a₁ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines NBI CQC_SIM1:def 9 :

registration

let c₁ be Element of CQC-WFF ;
cluster NBI a₁ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be Element of CQC-WFF ;
func index c₁ -> Nat equals :: CQC_SIM1:def 10
min (NBI a₁);
coherence ;

end;

:: deftheorem Def10 defines index CQC_SIM1:def 10 :

theorem Th21: :: CQC_SIM1:21

for b₁ being Element of CQC-WFF holds
( index b₁ = 0 iff b₁ is closed )

proof end;

theorem Th22: :: CQC_SIM1:22

for b₁ being Element of CQC-WFF
for b₂ being Element of NAT st x. b₂ in still_not-bound_in b₁ holds
b₂ < index b₁

proof end;

theorem Th23: :: CQC_SIM1:23

index VERUM = 0 by Th21, QC_LANG3:24;

theorem Th24: :: CQC_SIM1:24

for b₁ being Element of CQC-WFF holds index ('not' b₁) = index b₁

proof end;

theorem Th25: :: CQC_SIM1:25

for b₁, b₂ being Element of CQC-WFF holds
( index b₁ <= index (b₁ '&' b₂) & index b₂ <= index (b₁ '&' b₂) )

proof end;

definition

let c₁ be non empty set ;
redefine func id as id c₁ -> Element of Funcs a₁,a₁;
coherence

proof end;

end;

definition

let c₁ be Element of CQC-WFF ;
func SepVar c₁ -> Element of CQC-WFF equals :: CQC_SIM1:def 11
SepFunc a₁,(index a₁),(id bound_QC-variables );
coherence ;

end;

:: deftheorem Def11 defines SepVar CQC_SIM1:def 11 :

theorem Th26: :: CQC_SIM1:26

SepVar VERUM = VERUM

proof end;

scheme :: CQC_SIM1:sch 5
s5{ P₁[ set ] } :

for b₁ being Element of CQC-WFF holds P₁[b₁]

provided

E27: P₁[ VERUM ] and
E28: for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds P₁[b₃ ! b₂] and
E29: for b₁ being Element of CQC-WFF st P₁[b₁] holds
P₁[ 'not' b₁] and
E30: for b₁, b₂ being Element of CQC-WFF st P₁[b₁] & P₁[b₂] holds
P₁[b₁ '&' b₂] and
E31: for b₁ being Element of CQC-WFF
for b₂ being Element of bound_QC-variables st P₁[b₁] holds
P₁[ All b₂,b₁]

proof end;

theorem Th27: :: CQC_SIM1:27

for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds SepVar (b₃ ! b₂) = b₃ ! b₂

proof end;

theorem Th28: :: CQC_SIM1:28

for b₁ being Element of CQC-WFF st b₁ is atomic holds
SepVar b₁ = b₁

proof end;

theorem Th29: :: CQC_SIM1:29

for b₁ being Element of CQC-WFF holds SepVar ('not' b₁) = 'not' (SepVar b₁)

proof end;

theorem Th30: :: CQC_SIM1:30

for b₁, b₂ being Element of CQC-WFF st b₁ is negative & b₂ = the_argument_of b₁ holds
SepVar b₁ = 'not' (SepVar b₂)

proof end;

definition

let c₁ be Element of CQC-WFF ;
let c₂ be Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):];
pred c₂ is_Sep-closed_on c₁ means :Def12: :: CQC_SIM1:def 12
( [a₁,(index a₁),({}. bound_QC-variables ),(id bound_QC-variables )] in a₂ & ( for b₁ being Element of CQC-WFF
for b₂ being Element of NAT
for b₃ being Finite_Subset of bound_QC-variables
for b₄ being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' b₁),b₂,b₃,b₄] in a₂ holds
[b₁,b₂,b₃,b₄] in a₂ ) & ( for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [(b₁ '&' b₂),b₃,b₄,b₅] in a₂ holds
( [b₁,b₃,b₄,b₅] in a₂ & [b₂,(b₃ + (QuantNbr b₁)),b₄,b₅] in a₂ ) ) & ( for b₁ being Element of CQC-WFF
for b₂ being Element of bound_QC-variables
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All b₂,b₁),b₃,b₄,b₅] in a₂ holds
[b₁,(b₃ + 1),(b₄ \/ {b₂}),(b₅ +* ({b₂} --> (x. b₃)))] in a₂ ) );

end;

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

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func { as {c₂} -> Element of Fin a₁;
coherence

proof end;

end;

definition

let c₁ be Element of CQC-WFF ;
func SepQuadruples c₁ -> Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] means :Def13: :: CQC_SIM1:def 13
( a₂ is_Sep-closed_on a₁ & ( for b₁ being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st b₁ is_Sep-closed_on a₁ holds
a₂ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines SepQuadruples CQC_SIM1:def 13 :

theorem Th31: :: CQC_SIM1:31

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

proof end;

theorem Th32: :: CQC_SIM1:32

for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' b₂),b₃,b₄,b₅] in SepQuadruples b₁ holds
[b₂,b₃,b₄,b₅] in SepQuadruples b₁

proof end;

theorem Th33: :: CQC_SIM1:33

for b₁, b₂, b₃ being Element of CQC-WFF
for b₄ being Element of NAT
for b₅ being Finite_Subset of bound_QC-variables
for b₆ being Element of Funcs bound_QC-variables ,bound_QC-variables st [(b₂ '&' b₃),b₄,b₅,b₆] in SepQuadruples b₁ holds
( [b₂,b₄,b₅,b₆] in SepQuadruples b₁ & [b₃,(b₄ + (QuantNbr b₂)),b₅,b₆] in SepQuadruples b₁ )

proof end;

theorem Th34: :: CQC_SIM1:34

for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of bound_QC-variables
for b₄ being Element of NAT
for b₅ being Finite_Subset of bound_QC-variables
for b₆ being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All b₃,b₂),b₄,b₅,b₆] in SepQuadruples b₁ holds
[b₂,(b₄ + 1),(b₅ \/ {b₃}),(b₆ +* ({b₃} --> (x. b₄)))] in SepQuadruples b₁

proof end;

theorem Th35: :: CQC_SIM1:35

for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of NAT
for b₄ being Element of Funcs bound_QC-variables ,bound_QC-variables
for b₅ being Finite_Subset of bound_QC-variables holds
( not [b₁,b₃,b₅,b₄] in SepQuadruples b₂ or [b₁,b₃,b₅,b₄] = [b₂,(index b₂),({}. bound_QC-variables ),(id bound_QC-variables )] or [('not' b₁),b₃,b₅,b₄] in SepQuadruples b₂ or ex b₆ being Element of CQC-WFF st [(b₁ '&' b₆),b₃,b₅,b₄] in SepQuadruples b₂ or ex b₆ being Element of CQC-WFF ex b₇ being Element of NAT st
( b₃ = b₇ + (QuantNbr b₆) & [(b₆ '&' b₁),b₇,b₅,b₄] in SepQuadruples b₂ ) or ex b₆ being Element of bound_QC-variables ex b₇ being Element of NAT ex b₈ being Element of Funcs bound_QC-variables ,bound_QC-variables st
( b₇ + 1 = b₃ & b₈ +* ({b₆} --> (x. b₇)) = b₄ & ( [(All b₆,b₁),b₇,b₅,b₈] in SepQuadruples b₂ or [(All b₆,b₁),b₇,(b₅ \ {b₆}),b₈] in SepQuadruples b₂ ) ) )

proof end;

scheme :: CQC_SIM1:sch 6
s6{ F₁() -> Element of CQC-WFF , P₁[ set , set , set , set ] } :

for b₁ being Element of CQC-WFF
for b₂ being Element of NAT
for b₃ being Finite_Subset of bound_QC-variables
for b₄ being Element of Funcs bound_QC-variables ,bound_QC-variables st [b₁,b₂,b₃,b₄] in SepQuadruples F₁() holds
P₁[b₁,b₂,b₃,b₄]

provided

E36: P₁[F₁(), index F₁(), {}. bound_QC-variables , id bound_QC-variables ] and
E37: for b₁ being Element of CQC-WFF
for b₂ being Element of NAT
for b₃ being Finite_Subset of bound_QC-variables
for b₄ being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' b₁),b₂,b₃,b₄] in SepQuadruples F₁() & P₁[ 'not' b₁,b₂,b₃,b₄] holds
P₁[b₁,b₂,b₃,b₄] and
E38: for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [(b₁ '&' b₂),b₃,b₄,b₅] in SepQuadruples F₁() & P₁[b₁ '&' b₂,b₃,b₄,b₅] holds
( P₁[b₁,b₃,b₄,b₅] & P₁[b₂,b₃ + (QuantNbr b₁),b₄,b₅] ) and
E39: for b₁ being Element of CQC-WFF
for b₂ being Element of bound_QC-variables
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All b₂,b₁),b₃,b₄,b₅] in SepQuadruples F₁() & P₁[ All b₂,b₁,b₃,b₄,b₅] holds
P₁[b₁,b₃ + 1,b₄ \/ {b₂},b₅ +* ({b₂} --> (x. b₃))]

proof end;

theorem Th36: :: CQC_SIM1:36

for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [b₂,b₃,b₄,b₅] in SepQuadruples b₁ holds
b₂ is_subformula_of b₁

proof end;

theorem Th37: :: CQC_SIM1:37

SepQuadruples VERUM = {[VERUM ,0,({}. bound_QC-variables ),(id bound_QC-variables )]}

proof end;

theorem Th38: :: CQC_SIM1:38

for b₁ being Element of NAT
for b₂ being CQC-variable_list of b₁
for b₃ being QC-pred_symbol of b₁ holds SepQuadruples (b₃ ! b₂) = {[(b₃ ! b₂),(index (b₃ ! b₂)),({}. bound_QC-variables ),(id bound_QC-variables )]}

proof end;

theorem Th39: :: CQC_SIM1:39

for b₁, b₂ being Element of CQC-WFF
for b₃ being Element of NAT
for b₄ being Finite_Subset of bound_QC-variables
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables st [b₂,b₃,b₄,b₅] in SepQuadruples b₁ holds
still_not-bound_in b₂ c= (still_not-bound_in b₁) \/ b₄

proof end;

theorem Th40: :: CQC_SIM1:40

for b₁, b₂ being Element of CQC-WFF
for b₃, b₄ being Element of NAT
for b₅ being Element of Funcs bound_QC-variables ,bound_QC-variables
for b₆ being Finite_Subset of bound_QC-variables st [b₁,b₃,b₆,b₅] in SepQuadruples b₂ & x. b₄ in b₅ .: b₆ holds
b₄ < b₃

proof end;

theorem Th41: :: CQC_SIM1:41

theorem Th42: :: CQC_SIM1:42

proof end;

theorem Th43: :: CQC_SIM1:43

proof end;

theorem Th44: :: CQC_SIM1:44

theorem Th45: :: CQC_SIM1:45

for b₁ being Element of CQC-WFF holds still_not-bound_in b₁ = still_not-bound_in (SepVar b₁)

proof end;

theorem Th46: :: CQC_SIM1:46

for b₁ being Element of CQC-WFF holds index b₁ = index (SepVar b₁)

proof end;

definition

let c₁, c₂ be Element of CQC-WFF ;
pred c₁,c₂ are_similar means :Def14: :: CQC_SIM1:def 14
SepVar a₁ = SepVar a₂;
reflexivity ;
symmetry ;

end;

:: deftheorem Def14 defines are_similar CQC_SIM1:def 14 :

theorem Th47: :: CQC_SIM1:47

canceled;

theorem Th48: :: CQC_SIM1:48

canceled;

theorem Th49: :: CQC_SIM1:49

for b₁, b₂, b₃ being Element of CQC-WFF st b₁,b₂ are_similar & b₂,b₃ are_similar holds
b₁,b₃ are_similar

proof end;