:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

definition

let m, n be Nat;

{ k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } is set ;

end;
func seq (m,n) -> set equals :: CALCUL_2:def 1

{ k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } ;

coherence { k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } ;

{ k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } is set ;

:: deftheorem defines seq CALCUL_2:def 1 :

for m, n being Nat holds seq (m,n) = { k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } ;

for m, n being Nat holds seq (m,n) = { k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } ;

definition

let m, n be Nat;

:: original: seq

redefine func seq (m,n) -> Subset of NAT;

coherence

seq (m,n) is Subset of NAT

end;
:: original: seq

redefine func seq (m,n) -> Subset of NAT;

coherence

seq (m,n) is Subset of NAT

proof end;

registration
end;

registration
end;

theorem Th10: :: CALCUL_2:10

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds len (Sgm (seq ((len g),(len f)))) = len f

for f, g being FinSequence of CQC-WFF Al holds len (Sgm (seq ((len g),(len f)))) = len f

proof end;

theorem Th11: :: CALCUL_2:11

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds dom (Sgm (seq ((len g),(len f)))) = dom f

for f, g being FinSequence of CQC-WFF Al holds dom (Sgm (seq ((len g),(len f)))) = dom f

proof end;

theorem Th12: :: CALCUL_2:12

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))

for f, g being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))

proof end;

theorem Th13: :: CALCUL_2:13

for Al being QC-alphabet

for i being Element of NAT

for f, g being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds

(Sgm (seq ((len g),(len f)))) . i = (len g) + i

for i being Element of NAT

for f, g being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds

(Sgm (seq ((len g),(len f)))) . i = (len g) + i

proof end;

theorem Th14: :: CALCUL_2:14

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds seq ((len g),(len f)) c= dom (g ^ f)

for f, g being FinSequence of CQC-WFF Al holds seq ((len g),(len f)) c= dom (g ^ f)

proof end;

theorem Th15: :: CALCUL_2:15

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))

for f, g being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))

proof end;

theorem Th16: :: CALCUL_2:16

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)

for f, g being FinSequence of CQC-WFF Al holds Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f)

proof end;

theorem Th17: :: CALCUL_2:17

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al holds dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f

for f, g being FinSequence of CQC-WFF Al holds dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f

proof end;

definition

let D be non empty set ;

let f be FinSequence of D;

let P be Permutation of (dom f);

coherence

P * f is FinSequence of D

end;
let f be FinSequence of D;

let P be Permutation of (dom f);

coherence

P * f is FinSequence of D

proof end;

:: deftheorem defines Per CALCUL_2:def 2 :

for D being non empty set

for f being FinSequence of D

for P being Permutation of (dom f) holds Per (f,P) = P * f;

for D being non empty set

for f being FinSequence of D

for P being Permutation of (dom f) holds Per (f,P) = P * f;

theorem Th19: :: CALCUL_2:19

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f

for f being FinSequence of CQC-WFF Al

for P being Permutation of (dom f) holds dom (Per (f,P)) = dom f

proof end;

theorem Th20: :: CALCUL_2:20

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds

|- (g ^ f) ^ <*p*>

for p being Element of CQC-WFF Al

for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds

|- (g ^ f) ^ <*p*>

proof end;

definition

let Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

( ( 1 <= len f implies ex b_{1} being Element of CQC-WFF Al st b_{1} = f . 1 ) & ( not 1 <= len f implies ex b_{1} being Element of CQC-WFF Al st b_{1} = VERUM Al ) )

for b_{1}, b_{2} being Element of CQC-WFF Al holds

( ( 1 <= len f & b_{1} = f . 1 & b_{2} = f . 1 implies b_{1} = b_{2} ) & ( not 1 <= len f & b_{1} = VERUM Al & b_{2} = VERUM Al implies b_{1} = b_{2} ) )
;

consistency

for b_{1} being Element of CQC-WFF Al holds verum
;

end;
let f be FinSequence of CQC-WFF Al;

func Begin f -> Element of CQC-WFF Al means :Def3: :: CALCUL_2:def 3

it = f . 1 if 1 <= len f

otherwise it = VERUM Al;

existence it = f . 1 if 1 <= len f

otherwise it = VERUM Al;

( ( 1 <= len f implies ex b

proof end;

uniqueness for b

( ( 1 <= len f & b

consistency

for b

:: deftheorem Def3 defines Begin CALCUL_2:def 3 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for b_{3} being Element of CQC-WFF Al holds

( ( 1 <= len f implies ( b_{3} = Begin f iff b_{3} = f . 1 ) ) & ( not 1 <= len f implies ( b_{3} = Begin f iff b_{3} = VERUM Al ) ) );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al

for b

( ( 1 <= len f implies ( b

definition

let Al be QC-alphabet ;

let f be FinSequence of CQC-WFF Al;

assume A1: 1 <= len f ;

ex b_{1} being Element of CQC-WFF Al ex F being FinSequence of CQC-WFF Al st

( b_{1} = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) )

for b_{1}, b_{2} being Element of CQC-WFF Al st ex F being FinSequence of CQC-WFF Al st

( b_{1} = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) & ex F being FinSequence of CQC-WFF Al st

( b_{2} = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) holds

b_{1} = b_{2}

end;
let f be FinSequence of CQC-WFF Al;

assume A1: 1 <= len f ;

func Impl f -> Element of CQC-WFF Al means :Def4: :: CALCUL_2:def 4

ex F being FinSequence of CQC-WFF Al st

( it = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) );

existence ex F being FinSequence of CQC-WFF Al st

( it = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) );

ex b

( b

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) )

proof end;

uniqueness for b

( b

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) & ex F being FinSequence of CQC-WFF Al st

( b

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) holds

b

proof end;

:: deftheorem Def4 defines Impl CALCUL_2:def 4 :

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al st 1 <= len f holds

for b_{3} being Element of CQC-WFF Al holds

( b_{3} = Impl f iff ex F being FinSequence of CQC-WFF Al st

( b_{3} = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) );

for Al being QC-alphabet

for f being FinSequence of CQC-WFF Al st 1 <= len f holds

for b

( b

( b

ex p, q being Element of CQC-WFF Al st

( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) );

:: Some details about the calculus in CALCUL_1

theorem Th21: :: CALCUL_2:21

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al holds |- (f ^ <*p*>) ^ <*p*>

proof end;

theorem Th22: :: CALCUL_2:22

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds

|- f ^ <*p*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds

|- f ^ <*p*>

proof end;

theorem Th23: :: CALCUL_2:23

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds

|- f ^ <*q*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds

|- f ^ <*q*>

proof end;

theorem Th24: :: CALCUL_2:24

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> holds

|- f ^ <*q*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> holds

|- f ^ <*q*>

proof end;

theorem Th25: :: CALCUL_2:25

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- f ^ <*('not' p)*> holds

|- f ^ <*q*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> & |- f ^ <*('not' p)*> holds

|- f ^ <*q*>

proof end;

theorem Th26: :: CALCUL_2:26

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds

|- f ^ <*q*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds

|- f ^ <*q*>

proof end;

theorem Th27: :: CALCUL_2:27

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds

|- f ^ <*(p => q)*>

for p, q being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> holds

|- f ^ <*(p => q)*>

proof end;

theorem Th28: :: CALCUL_2:28

for Al being QC-alphabet

for f, g being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds

|- f ^ <*(Impl (Rev g))*>

for f, g being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds

|- f ^ <*(Impl (Rev g))*>

proof end;

theorem Th29: :: CALCUL_2:29

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al

for P being Permutation of (dom f) st |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds

|- (Per (f,P)) ^ <*p*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al

for P being Permutation of (dom f) st |- (Per (f,P)) ^ <*(Impl (Rev (f ^ <*p*>)))*> holds

|- (Per (f,P)) ^ <*p*>

proof end;

theorem :: CALCUL_2:30

for Al being QC-alphabet

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al

for P being Permutation of (dom f) st |- f ^ <*p*> holds

|- (Per (f,P)) ^ <*p*>

for p being Element of CQC-WFF Al

for f being FinSequence of CQC-WFF Al

for P being Permutation of (dom f) st |- f ^ <*p*> holds

|- (Per (f,P)) ^ <*p*>

proof end;

definition

let D be non empty set ;

let n be Element of NAT ;

let p be Element of D;

:: original: IdFinS

redefine func IdFinS (p,n) -> FinSequence of D;

coherence

IdFinS (p,n) is FinSequence of D

end;
let n be Element of NAT ;

let p be Element of D;

:: original: IdFinS

redefine func IdFinS (p,n) -> FinSequence of D;

coherence

IdFinS (p,n) is FinSequence of D

proof end;

theorem :: CALCUL_2:32

for Al being QC-alphabet

for p, q being Element of CQC-WFF Al

for n being Element of NAT

for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds

|- (f ^ <*p*>) ^ <*q*>

for p, q being Element of CQC-WFF Al

for n being Element of NAT

for f being FinSequence of CQC-WFF Al st 1 <= n & |- (f ^ (IdFinS (p,n))) ^ <*q*> holds

|- (f ^ <*p*>) ^ <*q*>

proof end;