:: Consequences of the Sequent Calculus
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


definition
let m, n be Nat;
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 ) } is set ;
end;

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

definition
let m, n be Nat;
:: original: seq
redefine func seq (m,n) -> Subset of NAT;
coherence
seq (m,n) is Subset of NAT
proof end;
end;

theorem Th1: :: CALCUL_2:1
for a, b, c being Nat holds
( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) )
proof end;

theorem Th2: :: CALCUL_2:2
for a being Nat holds seq (a,0) = {}
proof end;

theorem Th3: :: CALCUL_2:3
for a, b being Nat holds
( b = 0 or b + a in seq (a,b) )
proof end;

theorem Th4: :: CALCUL_2:4
for a, b1, b2 being Nat holds
( b1 <= b2 iff seq (a,b1) c= seq (a,b2) )
proof end;

theorem Th5: :: CALCUL_2:5
for a, b being Nat holds (seq (a,b)) \/ {((a + b) + 1)} = seq (a,(b + 1))
proof end;

theorem Th6: :: CALCUL_2:6
for m, n being Element of NAT holds seq (m,n),n are_equipotent
proof end;

registration
let m, n be Element of NAT ;
cluster seq (m,n) -> finite ;
coherence
seq (m,n) is finite
proof end;
end;

registration
let Al be QC-alphabet ;
let f be FinSequence of CQC-WFF Al;
cluster card f -> finite ;
coherence
len f is finite ;
end;

theorem Th7: :: CALCUL_2:7
for m, n being Element of NAT holds seq (m,n) c= Seg (m + n)
proof end;

theorem :: CALCUL_2:8
for m, n being Element of NAT holds Seg n misses seq (n,m)
proof end;

theorem :: CALCUL_2:9
for f, g being FinSequence holds dom (f ^ g) = (dom f) \/ (seq ((len f),(len g)))
proof 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
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
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))
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
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)
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))
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)
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
proof end;

theorem Th18: :: CALCUL_2:18
for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds f is_Subsequence_of g ^ f
proof end;

definition
let D be non empty set ;
let f be FinSequence of D;
let P be Permutation of (dom f);
func Per (f,P) -> FinSequence of D equals :: CALCUL_2:def 2
P * f;
coherence
P * f is FinSequence of D
proof end;
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;

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
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*>
proof end;

definition
let Al be QC-alphabet ;
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
( ( 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = f . 1 ) & ( not 1 <= len f implies ex b1 being Element of CQC-WFF Al st b1 = VERUM Al ) )
proof end;
uniqueness
for b1, b2 being Element of CQC-WFF Al holds
( ( 1 <= len f & b1 = f . 1 & b2 = f . 1 implies b1 = b2 ) & ( not 1 <= len f & b1 = VERUM Al & b2 = VERUM Al implies b1 = b2 ) ) ;
consistency
for b1 being Element of CQC-WFF Al holds verum ;
end;

:: deftheorem Def3 defines Begin CALCUL_2:def 3 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al
for b3 being Element of CQC-WFF Al holds
( ( 1 <= len f implies ( b3 = Begin f iff b3 = f . 1 ) ) & ( not 1 <= len f implies ( b3 = Begin f iff b3 = VERUM Al ) ) );

definition
let Al be QC-alphabet ;
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 b1 being Element of CQC-WFF Al ex F being FinSequence of CQC-WFF Al st
( b1 = 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 ) ) )
proof end;
uniqueness
for b1, b2 being Element of CQC-WFF Al st ex F being FinSequence of CQC-WFF Al st
( b1 = 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
( b2 = 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
b1 = b2
proof end;
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 b3 being Element of CQC-WFF Al holds
( b3 = Impl f iff ex F being FinSequence of CQC-WFF Al st
( b3 = 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 ) ) ) );

:: 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*>
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*>
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*>
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*>
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*>
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*>
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)*>
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))*>
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*>
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*>
proof end;

notation
let n be Element of NAT ;
let c be set ;
synonym IdFinS (c,n) for n |-> c;
end;

theorem Th31: :: CALCUL_2:31
for n being Element of NAT
for c being set st 1 <= n holds
rng (IdFinS (c,n)) = rng <*c*>
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
proof end;
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*>
proof end;