:: CQC_SIM1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: CQC_SIM1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being Function holds (f +* ({x} --> y)) .: {x} = {y}
proof end;

theorem Th2: :: CQC_SIM1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st p is atomic holds
ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being CQC-variable_list of k st p = P ! ll
proof end;

theorem :: CQC_SIM1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st p is negative holds
ex q being Element of CQC-WFF st p = 'not' q
proof end;

theorem :: CQC_SIM1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st p is conjunctive holds
ex q, r being Element of CQC-WFF st p = q '&' r
proof end;

theorem :: CQC_SIM1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st p is universal holds
ex x being Element of bound_QC-variables ex q being Element of CQC-WFF st p = All x,q
proof end;

theorem Th9: :: CQC_SIM1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being FinSequence holds rng l = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) }
proof end;

scheme :: CQC_SIM1:sch 1
QCFuncExN{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> Element of F1(), F4( set , set ) -> Element of F1(), F5( set , set , set ) -> Element of F1(), F6( set , set ) -> Element of F1() } :
ex F being Function of QC-WFF ,F1() st
( F . VERUM = F2() & ( for p being Element of QC-WFF holds
( ( p is atomic implies F . p = F3(p) ) & ( p is negative implies F . p = F4((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F5((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F6((F . (the_scope_of p)),p) ) ) ) )
proof end;

scheme :: CQC_SIM1:sch 2
CQCF2FuncEx{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of Funcs F1(),F2(), F4( set , set , set ) -> Element of Funcs F1(),F2(), F5( set , set ) -> Element of Funcs F1(),F2(), F6( set , set , set , set ) -> Element of Funcs F1(),F2(), F7( set , set , set ) -> Element of Funcs F1(),F2() } :
ex F being Function of CQC-WFF , Funcs F1(),F2() st
( F . VERUM = F3() & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds F . (P ! l) = F4(k,P,l) ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F . ('not' r) = F5((F . r),r) & F . (r '&' s) = F6((F . r),(F . s),r,s) & F . (All x,r) = F7(x,(F . r),r) ) ) )
proof end;

scheme :: CQC_SIM1:sch 3
CQCF2FUniq{ F1() -> non empty set , F2() -> non empty set , F3() -> Function of CQC-WFF , Funcs F1(),F2(), F4() -> Function of CQC-WFF , Funcs F1(),F2(), F5() -> Function of F1(),F2(), F6( set , set , set ) -> Function of F1(),F2(), F7( set , set ) -> Function of F1(),F2(), F8( set , set , set , set ) -> Function of F1(),F2(), F9( set , set , set ) -> Function of F1(),F2() } :
F3() = F4()
provided
A1: F3() . VERUM = F5() and
A2: for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds F3() . (P ! ll) = F6(k,P,ll) and
A3: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F3() . ('not' r) = F7((F3() . r),r) & F3() . (r '&' s) = F8((F3() . r),(F3() . s),r,s) & F3() . (All x,r) = F9(x,(F3() . r),r) ) and
A4: F4() . VERUM = F5() and
A5: for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds F4() . (P ! ll) = F6(k,P,ll) and
A6: for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( F4() . ('not' r) = F7((F4() . r),r) & F4() . (r '&' s) = F8((F4() . r),(F4() . s),r,s) & F4() . (All x,r) = F9(x,(F4() . r),r) )
proof end;

theorem Th10: :: CQC_SIM1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds p is_subformula_of 'not' p
proof end;

theorem Th11: :: CQC_SIM1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds
( p is_subformula_of p '&' q & q is_subformula_of p '&' q )
proof end;

theorem Th12: :: CQC_SIM1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being Element of bound_QC-variables holds p is_subformula_of All x,p
proof end;

theorem Th13: :: CQC_SIM1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Element of NAT
for l being CQC-variable_list of k
for i being Element of NAT st 1 <= i & i <= len l holds
l . i in bound_QC-variables
proof end;

definition
let D be non empty set ;
let f be Function of D, CQC-WFF ;
func NEGATIVE f -> Element of Funcs D,CQC-WFF means :Def1: :: CQC_SIM1:def 1
for a being Element of D
for p being Element of CQC-WFF st p = f . a holds
it . a = 'not' p;
existence
ex b1 being Element of Funcs D,CQC-WFF st
for a being Element of D
for p being Element of CQC-WFF st p = f . a holds
b1 . a = 'not' p
proof end;
uniqueness
for b1, b2 being Element of Funcs D,CQC-WFF st ( for a being Element of D
for p being Element of CQC-WFF st p = f . a holds
b1 . a = 'not' p ) & ( for a being Element of D
for p being Element of CQC-WFF st p = f . a holds
b2 . a = 'not' p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines NEGATIVE CQC_SIM1:def 1 :
for D being non empty set
for f being Function of D, CQC-WFF
for b3 being Element of Funcs D,CQC-WFF holds
( b3 = NEGATIVE f iff for a being Element of D
for p being Element of CQC-WFF st p = f . a holds
b3 . a = 'not' p );

definition
let f, g be Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):], CQC-WFF ;
let n be Nat;
func CON f,g,n -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def2: :: CQC_SIM1:def 2
for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . [k,h] & q = g . [(k + n),h] holds
it . [k,h] = p '&' q;
existence
ex b1 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st
for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . [k,h] & q = g . [(k + n),h] holds
b1 . [k,h] = p '&' q
proof end;
uniqueness
for b1, b2 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st ( for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . [k,h] & q = g . [(k + n),h] holds
b1 . [k,h] = p '&' q ) & ( for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . [k,h] & q = g . [(k + n),h] holds
b2 . [k,h] = p '&' q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines CON CQC_SIM1:def 2 :
for f, g being Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):], CQC-WFF
for n being Nat
for b4 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF holds
( b4 = CON f,g,n iff for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p, q being Element of CQC-WFF st p = f . [k,h] & q = g . [(k + n),h] holds
b4 . [k,h] = p '&' q );

Lm1: for x being Element of bound_QC-variables
for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds h +* ({x} --> (x. k)) is Function of bound_QC-variables , bound_QC-variables
proof end;

definition
let f be Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):], CQC-WFF ;
let x be bound_QC-variable;
func UNIVERSAL x,f -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def3: :: CQC_SIM1:def 3
for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p being Element of CQC-WFF st p = f . [(k + 1),(h +* ({x} --> (x. k)))] holds
it . [k,h] = All (x. k),p;
existence
ex b1 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st
for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p being Element of CQC-WFF st p = f . [(k + 1),(h +* ({x} --> (x. k)))] holds
b1 . [k,h] = All (x. k),p
proof end;
uniqueness
for b1, b2 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st ( for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p being Element of CQC-WFF st p = f . [(k + 1),(h +* ({x} --> (x. k)))] holds
b1 . [k,h] = All (x. k),p ) & ( for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p being Element of CQC-WFF st p = f . [(k + 1),(h +* ({x} --> (x. k)))] holds
b2 . [k,h] = All (x. k),p ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines UNIVERSAL CQC_SIM1:def 3 :
for f being Function of [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):], CQC-WFF
for x being bound_QC-variable
for b3 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF holds
( b3 = UNIVERSAL x,f iff for k being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables
for p being Element of CQC-WFF st p = f . [(k + 1),(h +* ({x} --> (x. k)))] holds
b3 . [k,h] = All (x. k),p );

Lm2: for k being Element of NAT
for f being FinSequence of bound_QC-variables st len f = k holds
f is CQC-variable_list of k
proof end;

Lm3: for k being Element of NAT
for f being CQC-variable_list of k holds f is FinSequence of bound_QC-variables
proof end;

definition
let k be Element of NAT ;
let l be CQC-variable_list of k;
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ;
:: original: *
redefine func f * l -> CQC-variable_list of k;
coherence
l * f is CQC-variable_list of k
proof end;
end;

definition
let k be Element of NAT ;
let P be QC-pred_symbol of k;
let l be CQC-variable_list of k;
func ATOMIC P,l -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF means :Def4: :: CQC_SIM1:def 4
for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds it . [n,h] = P ! (h * l);
existence
ex b1 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st
for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds b1 . [n,h] = P ! (h * l)
proof end;
uniqueness
for b1, b2 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st ( for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds b1 . [n,h] = P ! (h * l) ) & ( for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds b2 . [n,h] = P ! (h * l) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines ATOMIC CQC_SIM1:def 4 :
for k being Element of NAT
for P being QC-pred_symbol of k
for l being CQC-variable_list of k
for b4 being Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF holds
( b4 = ATOMIC P,l iff for n being Element of NAT
for h being Element of Funcs bound_QC-variables ,bound_QC-variables holds b4 . [n,h] = P ! (h * l) );

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

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

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

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

definition
let p be Element of CQC-WFF ;
func QuantNbr p -> Element of NAT means :Def5: :: CQC_SIM1:def 5
 ex F being Function of CQC-WFF , NAT st
( it = F . p & F . VERUM = 0 & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k 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 b1 being Element of NAT ex F being Function of CQC-WFF , NAT st
( b1 = F . p & F . VERUM = 0 & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k 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 b1, b2 being Element of NAT st ex F being Function of CQC-WFF , NAT st
( b1 = F . p & F . VERUM = 0 & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k 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 , NAT st
( b2 = F . p & F . VERUM = 0 & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k 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
b1 = b2;
proof end;
end;

:: deftheorem Def5 defines QuantNbr CQC_SIM1:def 5 :
for p being Element of CQC-WFF
for b2 being Element of NAT holds
( b2 = QuantNbr p iff ex F being Function of CQC-WFF , NAT st
( b2 = F . p & F . VERUM = 0 & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k 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 f be Function of CQC-WFF , Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ;
let x be Element of CQC-WFF ;
:: original: .
redefine func f . x -> Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF ;
coherence
f . x is Element of Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF
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
( it . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds it . (P ! l) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables 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 b1 being Function of CQC-WFF , Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st
( b1 . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds b1 . (P ! l) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( b1 . ('not' r) = NEGATIVE (b1 . r) & b1 . (r '&' s) = CON (b1 . r),(b1 . s),(QuantNbr r) & b1 . (All x,r) = UNIVERSAL x,(b1 . r) ) ) )
proof end;
uniqueness
for b1, b2 being Function of CQC-WFF , Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF st b1 . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds b1 . (P ! l) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( b1 . ('not' r) = NEGATIVE (b1 . r) & b1 . (r '&' s) = CON (b1 . r),(b1 . s),(QuantNbr r) & b1 . (All x,r) = UNIVERSAL x,(b1 . r) ) ) & b2 . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds b2 . (P ! l) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( b2 . ('not' r) = NEGATIVE (b2 . r) & b2 . (r '&' s) = CON (b2 . r),(b2 . s),(QuantNbr r) & b2 . (All x,r) = UNIVERSAL x,(b2 . r) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines SepFunc CQC_SIM1:def 6 :
for b1 being Function of CQC-WFF , Funcs [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):],CQC-WFF holds
( b1 = SepFunc iff ( b1 . VERUM = [:NAT ,(Funcs bound_QC-variables ,bound_QC-variables ):] --> VERUM & ( for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds b1 . (P ! l) = ATOMIC P,l ) & ( for r, s being Element of CQC-WFF
for x being Element of bound_QC-variables holds
( b1 . ('not' r) = NEGATIVE (b1 . r) & b1 . (r '&' s) = CON (b1 . r),(b1 . s),(QuantNbr r) & b1 . (All x,r) = UNIVERSAL x,(b1 . r) ) ) ) );

definition
let p be Element of CQC-WFF ;
let k be Element of NAT ;
let f be Element of Funcs bound_QC-variables ,bound_QC-variables ;
func SepFunc p,k,f -> Element of CQC-WFF equals :: CQC_SIM1:def 7
(SepFunc . p) . [k,f];
correctness
coherence
(SepFunc . p) . [k,f] is Element of CQC-WFF ;
;
end;

:: deftheorem defines SepFunc CQC_SIM1:def 7 :
for p being Element of CQC-WFF
for k being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables holds SepFunc p,k,f = (SepFunc . p) . [k,f];

deffunc H5( Element of CQC-WFF ) -> Element of NAT = QuantNbr $1;

theorem :: CQC_SIM1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
QuantNbr VERUM = 0
proof end;

theorem :: CQC_SIM1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds QuantNbr (P ! ll) = 0
proof end;

theorem :: CQC_SIM1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds QuantNbr ('not' p) = QuantNbr p
proof end;

theorem :: CQC_SIM1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds QuantNbr (p '&' q) = (QuantNbr p) + (QuantNbr q)
proof end;

theorem :: CQC_SIM1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for x being Element of bound_QC-variables holds QuantNbr (All x,p) = (QuantNbr p) + 1
proof end;

definition
let A be non empty Subset of NAT ;
func min A -> Nat means :Def8: :: CQC_SIM1:def 8
( it in A & ( for k being Element of NAT st k in A holds
it <= k ) );
existence
ex b1 being Nat st
( b1 in A & ( for k being Element of NAT st k in A holds
b1 <= k ) )
proof end;
uniqueness
for b1, b2 being Nat st b1 in A & ( for k being Element of NAT st k in A holds
b1 <= k ) & b2 in A & ( for k being Element of NAT st k in A holds
b2 <= k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines min CQC_SIM1:def 8 :
for A being non empty Subset of NAT
for b2 being Nat holds
( b2 = min A iff ( b2 in A & ( for k being Element of NAT st k in A holds
b2 <= k ) ) );

theorem Th19: :: CQC_SIM1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty Subset of NAT st A c= B holds
min B <= min A
proof end;

theorem Th20: :: CQC_SIM1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of QC-WFF holds still_not-bound_in p is finite
proof end;

scheme :: CQC_SIM1:sch 4
MaxFinDomElem{ F1() -> non empty set , F2() -> set , P1[ set , set ] } :
ex x being Element of F1() st
( x in F2() & ( for y being Element of F1() st y in F2() holds
P1[x,y] ) )
provided
A1: ( F2() is finite & F2() <> {} & F2() c= F1() ) and
A2: for x, y being Element of F1() holds
( P1[x,y] or P1[y,x] ) and
A3: for x, y, z being Element of F1() st P1[x,y] & P1[y,z] holds
P1[x,z]
proof end;

definition
let p be Element of CQC-WFF ;
func NBI p -> Subset of NAT equals :: CQC_SIM1:def 9
{ k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;
coherence
{ k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } is Subset of NAT
proof end;
end;

:: deftheorem defines NBI CQC_SIM1:def 9 :
for p being Element of CQC-WFF holds NBI p = { k where k is Element of NAT : for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p } ;

registration
let p be Element of CQC-WFF ;
cluster NBI p -> non empty ;
coherence
not NBI p is empty
proof end;
end;

definition
let p be Element of CQC-WFF ;
func index p -> Nat equals :: CQC_SIM1:def 10
 min (NBI p);
coherence
min (NBI p) is Nat ;
end;

:: deftheorem defines index CQC_SIM1:def 10 :
for p being Element of CQC-WFF holds index p = min (NBI p);

theorem Th21: :: CQC_SIM1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds
( index p = 0 iff p is closed )
proof end;

theorem Th22: :: CQC_SIM1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for i being Element of NAT st x. i in still_not-bound_in p holds
i < index p
proof end;

theorem Th23: :: CQC_SIM1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
index VERUM = 0 by Th21, QC_LANG3:24;

theorem Th24: :: CQC_SIM1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds index ('not' p) = index p
proof end;

theorem :: CQC_SIM1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF holds
( index p <= index (p '&' q) & index q <= index (p '&' q) )
proof end;

definition
let X be non empty 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 p be Element of CQC-WFF ;
func SepVar p -> Element of CQC-WFF equals :: CQC_SIM1:def 11
 SepFunc p,(index p),(id bound_QC-variables );
coherence
SepFunc p,(index p),(id bound_QC-variables ) is Element of CQC-WFF ;
end;

:: deftheorem defines SepVar CQC_SIM1:def 11 :
for p being Element of CQC-WFF holds SepVar p = SepFunc p,(index p),(id bound_QC-variables );

theorem :: CQC_SIM1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
SepVar VERUM = VERUM
proof end;

scheme :: CQC_SIM1:sch 5
CQCInd{ P1[ set ] } :
for r being Element of CQC-WFF holds P1[r]
provided
A1: P1[ VERUM ] and
A2: for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds P1[P ! l] and
A3: for r being Element of CQC-WFF st P1[r] holds
P1[ 'not' r] and
A4: for r, s being Element of CQC-WFF st P1[r] & P1[s] holds
P1[r '&' s] and
A5: for r being Element of CQC-WFF
for x being Element of bound_QC-variables st P1[r] holds
P1[ All x,r]
proof end;

theorem Th27: :: CQC_SIM1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of k holds SepVar (P ! ll) = P ! ll
proof end;

theorem :: CQC_SIM1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF st p is atomic holds
SepVar p = p
proof end;

theorem Th29: :: CQC_SIM1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds SepVar ('not' p) = 'not' (SepVar p)
proof end;

theorem :: CQC_SIM1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF st p is negative & q = the_argument_of p holds
SepVar p = 'not' (SepVar q)
proof end;

definition
let p be Element of CQC-WFF ;
let X be Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):];
pred X is_Sep-closed_on p means :Def12: :: CQC_SIM1:def 12
( [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in X & ( for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in X holds
[q,k,K,f] in X ) & ( for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* ({x} --> (x. k)))] in X ) );
end;

:: deftheorem Def12 defines is_Sep-closed_on CQC_SIM1:def 12 :
for p being Element of CQC-WFF
for X being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
( X is_Sep-closed_on p iff ( [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in X & ( for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in X holds
[q,k,K,f] in X ) & ( for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in X holds
( [q,k,K,f] in X & [r,(k + (QuantNbr q)),K,f] in X ) ) & ( for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in X holds
[q,(k + 1),(K \/ {x}),(f +* ({x} --> (x. k)))] in X ) ) );

definition
let D be non empty set ;
let x be Element of D;
:: original: {
redefine func {x} -> Element of Fin D;
coherence
{x} is Element of Fin D
proof end;
end;

definition
let p be Element of CQC-WFF ;
func SepQuadruples p -> Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] means :Def13: :: CQC_SIM1:def 13
( it is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
it c= D ) );
existence
ex b1 being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st
( b1 is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st b1 is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
b1 c= D ) & b2 is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines SepQuadruples CQC_SIM1:def 13 :
for p being Element of CQC-WFF
for b2 being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] holds
( b2 = SepQuadruples p iff ( b2 is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
b2 c= D ) ) );

theorem Th31: :: CQC_SIM1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] in SepQuadruples p
proof end;

theorem Th32: :: CQC_SIM1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in SepQuadruples p holds
[q,k,K,f] in SepQuadruples p
proof end;

theorem Th33: :: CQC_SIM1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples p holds
( [q,k,K,f] in SepQuadruples p & [r,(k + (QuantNbr q)),K,f] in SepQuadruples p )
proof end;

theorem Th34: :: CQC_SIM1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples p holds
[q,(k + 1),(K \/ {x}),(f +* ({x} --> (x. k)))] in SepQuadruples p
proof end;

theorem Th35: :: CQC_SIM1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for k being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables holds
( not [q,k,K,f] in SepQuadruples p or [q,k,K,f] = [p,(index p),({}. bound_QC-variables ),(id bound_QC-variables )] or [('not' q),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF st [(q '&' r),k,K,f] in SepQuadruples p or ex r being Element of CQC-WFF ex l being Element of NAT st
( k = l + (QuantNbr r) & [(r '&' q),l,K,f] in SepQuadruples p ) or ex x being Element of bound_QC-variables ex l being Element of NAT ex h being Element of Funcs bound_QC-variables ,bound_QC-variables st
( l + 1 = k & h +* ({x} --> (x. l)) = f & ( [(All x,q),l,K,h] in SepQuadruples p or [(All x,q),l,(K \ {x}),h] in SepQuadruples p ) ) )
proof end;

scheme :: CQC_SIM1:sch 6
Sepregression{ F1() -> Element of CQC-WFF , P1[ set , set , set , set ] } :
for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples F1() holds
P1[q,k,K,f]
provided
A1: P1[F1(), index F1(), {}. bound_QC-variables , id bound_QC-variables ] and
A2: for q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [('not' q),k,K,f] in SepQuadruples F1() & P1[ 'not' q,k,K,f] holds
P1[q,k,K,f] and
A3: for q, r being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(q '&' r),k,K,f] in SepQuadruples F1() & P1[q '&' r,k,K,f] holds
( P1[q,k,K,f] & P1[r,k + (QuantNbr q),K,f] ) and
A4: for q being Element of CQC-WFF
for x being Element of bound_QC-variables
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [(All x,q),k,K,f] in SepQuadruples F1() & P1[ All x,q,k,K,f] holds
P1[q,k + 1,K \/ {x},f +* ({x} --> (x. k))]
proof end;

theorem Th36: :: CQC_SIM1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples p holds
q is_subformula_of p
proof end;

theorem :: CQC_SIM1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
SepQuadruples VERUM = {[VERUM ,0,({}. bound_QC-variables ),(id bound_QC-variables )]}
proof end;

theorem :: CQC_SIM1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Element of NAT
for l being CQC-variable_list of k
for P being QC-pred_symbol of k holds SepQuadruples (P ! l) = {[(P ! l),(index (P ! l)),({}. bound_QC-variables ),(id bound_QC-variables )]}
proof end;

theorem Th39: :: CQC_SIM1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of CQC-WFF
for k being Element of NAT
for K being Finite_Subset of bound_QC-variables
for f being Element of Funcs bound_QC-variables ,bound_QC-variables st [q,k,K,f] in SepQuadruples p holds
still_not-bound_in q c= (still_not-bound_in p) \/ K
proof end;

theorem Th40: :: CQC_SIM1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for m, i being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: K holds
i < m
proof end;

theorem :: CQC_SIM1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for m being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p holds
not x. m in f .: K by Th40;

theorem Th42: :: CQC_SIM1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for m, i being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in p) holds
i < m
proof end;

theorem Th43: :: CQC_SIM1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for m, i being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in q) holds
i < m
proof end;

theorem :: CQC_SIM1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of CQC-WFF
for m being Element of NAT
for f being Element of Funcs bound_QC-variables ,bound_QC-variables
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p holds
not x. m in f .: (still_not-bound_in q) by Th43;

theorem Th45: :: CQC_SIM1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds still_not-bound_in p = still_not-bound_in (SepVar p)
proof end;

theorem :: CQC_SIM1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF holds index p = index (SepVar p)
proof end;

definition
let p, q be Element of CQC-WFF ;
pred p,q are_similar means :Def14: :: CQC_SIM1:def 14
 SepVar p = SepVar q;
reflexivity
for p being Element of CQC-WFF holds SepVar p = SepVar p ;
symmetry
for p, q being Element of CQC-WFF st SepVar p = SepVar q holds
SepVar q = SepVar p ;
end;

:: deftheorem Def14 defines are_similar CQC_SIM1:def 14 :
for p, q being Element of CQC-WFF holds
( p,q are_similar iff SepVar p = SepVar q );

theorem :: CQC_SIM1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_SIM1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CQC_SIM1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of CQC-WFF st p,q are_similar & q,r are_similar holds
p,r are_similar
proof end;