:: Similarity of Formulae :: by Agata Darmochwa{\l} and Andrzej Trybulec :: :: Received November 22, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users begin 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 b1 being QC-symbol of A st x. b1 = b by QC_LANG3:30; uniqueness for b1, b2 being QC-symbol of A st x. b1 = b & x. b2 = b holds b1 = b2 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 b3 being QC-symbol of A holds ( b3 = x. b iff x. b3 = b ); theorem Th1: :: CQC_SIM1:1 for x, y being set for f being Function holds Im ((f +* (x .--> y)),x) = {y} proofend; 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} proofend; 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}) proofend; 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} proofend; 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 Element of NAT ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll proofend; 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 proofend; 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 proofend; 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) proofend; theorem Th9: :: CQC_SIM1:9 for l being FinSequence holds rng l = { (l . i) where i is Element of NAT : ( 1 <= i & i <= len l ) } proofend; scheme :: CQC_SIM1:sch 1 QCFuncExN{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( set ) -> Element of F2(), F5( set , set ) -> Element of F2(), F6( set , set , set ) -> Element of F2(), F7( set , set ) -> Element of F2() } : ex F being Function of (QC-WFF F1()),F2() st ( F . (VERUM F1()) = F3() & ( for p being Element of QC-WFF F1() holds ( ( p is atomic implies F . p = F4(p) ) & ( p is negative implies F . p = F5((F . (the_argument_of p)),p) ) & ( p is conjunctive implies F . p = F6((F . (the_left_argument_of p)),(F . (the_right_argument_of p)),p) ) & ( p is universal implies F . p = F7((F . (the_scope_of p)),p) ) ) ) ) proofend; scheme :: CQC_SIM1:sch 2 CQCF2FuncEx{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> non empty set , F4() -> Element of Funcs (F2(),F3()), F5( set , set , set ) -> Element of Funcs (F2(),F3()), F6( set , set ) -> Element of Funcs (F2(),F3()), F7( set , set , set , set ) -> Element of Funcs (F2(),F3()), F8( set , set , set ) -> Element of Funcs (F2(),F3()) } : ex F being Function of (CQC-WFF F1()),(Funcs (F2(),F3())) st ( F . (VERUM F1()) = F4() & ( for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds F . (P ! l) = F5(k,P,l) ) & ( for r, s being Element of CQC-WFF F1() for x being Element of bound_QC-variables F1() holds ( F . ('not' r) = F6((F . r),r) & F . (r '&' s) = F7((F . r),(F . s),r,s) & F . (All (x,r)) = F8(x,(F . r),r) ) ) ) proofend; scheme :: CQC_SIM1:sch 3 CQCF2FUniq{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> non empty set , F4() -> Function of (CQC-WFF F1()),(Funcs (F2(),F3())), F5() -> Function of (CQC-WFF F1()),(Funcs (F2(),F3())), F6() -> Function of F2(),F3(), F7( set , set , set ) -> Function of F2(),F3(), F8( set , set ) -> Function of F2(),F3(), F9( set , set , set , set ) -> Function of F2(),F3(), F10( set , set , set ) -> Function of F2(),F3() } : F4() = F5() provided A1: F4() . (VERUM F1()) = F6() and A2: for k being Element of NAT for ll being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds F4() . (P ! ll) = F7(k,P,ll) and A3: for r, s being Element of CQC-WFF F1() for x being Element of bound_QC-variables F1() holds ( F4() . ('not' r) = F8((F4() . r),r) & F4() . (r '&' s) = F9((F4() . r),(F4() . s),r,s) & F4() . (All (x,r)) = F10(x,(F4() . r),r) ) and A4: F5() . (VERUM F1()) = F6() and A5: for k being Element of NAT for ll being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds F5() . (P ! ll) = F7(k,P,ll) and A6: for r, s being Element of CQC-WFF F1() for x being Element of bound_QC-variables F1() holds ( F5() . ('not' r) = F8((F5() . r),r) & F5() . (r '&' s) = F9((F5() . r),(F5() . s),r,s) & F5() . (All (x,r)) = F10(x,(F5() . r),r) ) proofend; 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 proofend; 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 ) proofend; 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) proofend; theorem Th13: :: CQC_SIM1:13 for A being QC-alphabet for k being Element of NAT for l being CQC-variable_list of k,A for i being Element of NAT st 1 <= i & i <= len l holds l . i in bound_QC-variables A proofend; 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 b1 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 b1 . a = 'not' p proofend; uniqueness for b1, b2 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 b1 . a = 'not' p ) & ( for a being Element of D for p being Element of CQC-WFF A st p = f . a holds b2 . a = 'not' p ) holds b1 = b2 proofend; 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 b4 being Element of Funcs (D,(CQC-WFF A)) holds ( b4 = NEGATIVE f iff for a being Element of D for p being Element of CQC-WFF A st p = f . a holds b4 . 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 Element of 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 b1 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 b1 . (t,h) = p '&' q proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (t,h) = p '&' q ) holds b1 = b2 proofend; 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 Element of NAT for b5 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds ( b5 = 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 b5 . (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) proofend; 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 b1 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 b1 . (t,h) = All ((x. t),p) proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (t,h) = All ((x. t),p) ) holds b1 = b2 proofend; 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 b4 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds ( b4 = 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 b4 . (t,h) = All ((x. t),p) ); Lm2: for A being QC-alphabet for k being Element of NAT for f being CQC-variable_list of k,A holds f is FinSequence of bound_QC-variables A proofend; definition let A be QC-alphabet ; let k be Element of 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 funcf * l -> CQC-variable_list of k,A; coherence l * f is CQC-variable_list of k,A proofend; end; definition let A be QC-alphabet ; let k be Element of 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 b1 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 b1 . (t,h) = P ! (h * l) proofend; uniqueness for b1, b2 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 b1 . (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 b2 . (t,h) = P ! (h * l) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines ATOMIC CQC_SIM1:def_5_:_ for A being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,A for l being CQC-variable_list of k,A for b5 being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds ( b5 = 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 b5 . (t,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 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 Element of 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 b1 being Element of NAT ex F being Function of (CQC-WFF A),NAT st ( b1 = 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 Element of 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 b1, b2 being Element of NAT st ex F being Function of (CQC-WFF A),NAT st ( b1 = 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 Element of 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 ( b2 = 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 Element of 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 b1 = b2; proofend; end; :: deftheorem Def6 defines QuantNbr CQC_SIM1:def_6_:_ for A being QC-alphabet for p being Element of CQC-WFF A for b3 being Element of NAT holds ( b3 = QuantNbr p iff ex F being Function of (CQC-WFF A),NAT st ( b3 = 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 Element of 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 funcf . 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)) proofend; 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 Element of 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 b1 being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st ( b1 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds b1 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A for x being Element of bound_QC-variables A 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)) ) ) ) proofend; uniqueness for b1, b2 being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) st b1 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds b1 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A for x being Element of bound_QC-variables A 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 A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds b2 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A for x being Element of bound_QC-variables A 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 proofend; end; :: deftheorem Def7 defines SepFunc CQC_SIM1:def_7_:_ for A being QC-alphabet for b2 being Function of (CQC-WFF A),(Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A))) holds ( b2 = SepFunc A iff ( b2 . (VERUM A) = [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] --> (VERUM A) & ( for k being Element of NAT for l being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds b2 . (P ! l) = ATOMIC (P,l) ) & ( for r, s being Element of CQC-WFF A for x being Element of bound_QC-variables A 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)) ) ) ) ); 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 proofend; theorem :: CQC_SIM1:15 for A being QC-alphabet for k being Element of NAT for ll being CQC-variable_list of k,A for P being QC-pred_symbol of k,A holds QuantNbr (P ! ll) = 0 proofend; theorem :: CQC_SIM1:16 for A being QC-alphabet for p being Element of CQC-WFF A holds QuantNbr ('not' p) = QuantNbr p proofend; 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) proofend; 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 proofend; 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 proofend; 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] proofend; 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) proofend; 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) proofend; 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 proofend; 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 ) proofend; 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 proofend; theorem Th22: :: CQC_SIM1:22 for A being QC-alphabet holds index (VERUM A) = 0 A proofend; theorem Th23: :: CQC_SIM1:23 for A being QC-alphabet for p being Element of CQC-WFF A holds index ('not' p) = index p proofend; 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) ) proofend; 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 proofend; scheme :: CQC_SIM1:sch 5 CQCInd{ F1() -> QC-alphabet , P1[ set ] } : for r being Element of CQC-WFF F1() holds P1[r] provided A1: P1[ VERUM F1()] and A2: for k being Element of NAT for l being CQC-variable_list of k,F1() for P being QC-pred_symbol of k,F1() holds P1[P ! l] and A3: for r being Element of CQC-WFF F1() st P1[r] holds P1[ 'not' r] and A4: for r, s being Element of CQC-WFF F1() st P1[r] & P1[s] holds P1[r '&' s] and A5: for r being Element of CQC-WFF F1() for x being bound_QC-variable of F1() st P1[r] holds P1[ All (x,r)] proofend; theorem Th26: :: CQC_SIM1:26 for A being QC-alphabet for k being Element of 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 proofend; 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 proofend; 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) proofend; 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) proofend; 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))):]; predX is_Sep-closed_on p means :Def12: :: 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 Finite_Subset of (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 Finite_Subset of (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 Finite_Subset of (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 Def12 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 Finite_Subset of (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 Finite_Subset of (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 Finite_Subset of (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 b1 being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st ( b1 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 b1 c= D ) ) proofend; uniqueness for b1, b2 being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st b1 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 b1 c= D ) & b2 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 b2 c= D ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines SepQuadruples CQC_SIM1:def_13_:_ for A being QC-alphabet for p being Element of CQC-WFF A for b3 being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] holds ( b3 = SepQuadruples p iff ( b3 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 b3 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 proofend; 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 Finite_Subset of (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 proofend; 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 Finite_Subset of (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 ) proofend; 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 Finite_Subset of (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 proofend; theorem Th34: :: CQC_SIM1:34 for A being QC-alphabet for t being QC-symbol of A for q, p being Element of CQC-WFF A for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) for K being Finite_Subset of (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 ) ) ) proofend; scheme :: CQC_SIM1:sch 6 Sepregression{ F1() -> QC-alphabet , F2() -> Element of CQC-WFF F1(), P1[ set , set , set , set ] } : for q being Element of CQC-WFF F1() for t being QC-symbol of F1() for K being Finite_Subset of (bound_QC-variables F1()) for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [q,t,K,f] in SepQuadruples F2() holds P1[q,t,K,f] provided A1: P1[F2(), index F2(), {}. (bound_QC-variables F1()), id (bound_QC-variables F1())] and A2: for q being Element of CQC-WFF F1() for t being QC-symbol of F1() for K being Finite_Subset of (bound_QC-variables F1()) for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [('not' q),t,K,f] in SepQuadruples F2() & P1[ 'not' q,t,K,f] holds P1[q,t,K,f] and A3: for q, r being Element of CQC-WFF F1() for t being QC-symbol of F1() for K being Finite_Subset of (bound_QC-variables F1()) for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(q '&' r),t,K,f] in SepQuadruples F2() & P1[q '&' r,t,K,f] holds ( P1[q,t,K,f] & P1[r,t + (QuantNbr q),K,f] ) and A4: for q being Element of CQC-WFF F1() for x being bound_QC-variable of F1() for t being QC-symbol of F1() for K being Finite_Subset of (bound_QC-variables F1()) for f being Element of Funcs ((bound_QC-variables F1()),(bound_QC-variables F1())) st [(All (x,q)),t,K,f] in SepQuadruples F2() & P1[ All (x,q),t,K,f] holds P1[q,t ++ ,K \/ {x},f +* (x .--> (x. t))] proofend; 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 Finite_Subset of (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 proofend; 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))]} proofend; theorem :: CQC_SIM1:37 for A being QC-alphabet for k being Element of 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))]} proofend; 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 Finite_Subset of (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 proofend; theorem Th39: :: CQC_SIM1:39 for A being QC-alphabet for t, u being QC-symbol of A for q, p being Element of CQC-WFF A for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) for K being Finite_Subset of (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: K holds u < t proofend; theorem :: CQC_SIM1:40 for A being QC-alphabet for t being QC-symbol of A for q, p being Element of CQC-WFF A for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) for K being Finite_Subset of (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds not x. t in f .: K proofend; theorem Th41: :: CQC_SIM1:41 for A being QC-alphabet for t, u being QC-symbol of A for q, p being Element of CQC-WFF A for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) for K being Finite_Subset of (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in p) holds u < t proofend; theorem Th42: :: CQC_SIM1:42 for A being QC-alphabet for t, u being QC-symbol of A for q, p being Element of CQC-WFF A for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) for K being Finite_Subset of (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds u < t proofend; theorem Th43: :: CQC_SIM1:43 for A being QC-alphabet for t being QC-symbol of A for q, p being Element of CQC-WFF A for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)) for K being Finite_Subset of (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p holds not x. t in f .: (still_not-bound_in q) proofend; 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) proofend; theorem :: CQC_SIM1:45 for A being QC-alphabet for p being Element of CQC-WFF A holds index p = index (SepVar p) proofend; definition let A be QC-alphabet ; let p, q be Element of CQC-WFF A; predp,q are_similar means :Def14: :: 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 Def14 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 proofend;