:: Consequences of the Sequent Calculus :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin definition let m, n be natural number ; 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 natural number holds seq (m,n) = { k where k is Element of NAT : ( 1 + m <= k & k <= n + m ) } ; definition let m, n be natural number ; :: original:seq redefine func seq (m,n) -> Subset of NAT; coherence seq (m,n) is Subset of NAT proofend; end; theorem Th1: :: CALCUL_2:1 for c, a, b being natural number holds ( c in seq (a,b) iff ( 1 + a <= c & c <= b + a ) ) proofend; theorem Th2: :: CALCUL_2:2 for a being natural number holds seq (a,0) = {} proofend; theorem Th3: :: CALCUL_2:3 for b, a being natural number holds ( b = 0 or b + a in seq (a,b) ) proofend; theorem Th4: :: CALCUL_2:4 for b1, b2, a being natural number holds ( b1 <= b2 iff seq (a,b1) c= seq (a,b2) ) proofend; theorem Th5: :: CALCUL_2:5 for a, b being natural number holds (seq (a,b)) \/ {((a + b) + 1)} = seq (a,(b + 1)) proofend; theorem Th6: :: CALCUL_2:6 for m, n being Element of NAT holds seq (m,n),n are_equipotent proofend; registration let m, n be Element of NAT ; cluster seq (m,n) -> finite ; coherence seq (m,n) is finite proofend; 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) proofend; theorem :: CALCUL_2:8 for n, m being Element of NAT holds Seg n misses seq (n,m) proofend; theorem :: CALCUL_2:9 for f, g being FinSequence holds dom (f ^ g) = (dom f) \/ (seq ((len f),(len g))) proofend; theorem Th10: :: CALCUL_2:10 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds len (Sgm (seq ((len g),(len f)))) = len f proofend; theorem Th11: :: CALCUL_2:11 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds dom (Sgm (seq ((len g),(len f)))) = dom f proofend; theorem Th12: :: CALCUL_2:12 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f)) proofend; theorem Th13: :: CALCUL_2:13 for Al being QC-alphabet for i being Element of NAT for g, f 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 proofend; theorem Th14: :: CALCUL_2:14 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds seq ((len g),(len f)) c= dom (g ^ f) proofend; theorem Th15: :: CALCUL_2:15 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f)) proofend; theorem Th16: :: CALCUL_2:16 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds Seq ((g ^ f) | (seq ((len g),(len f)))) = (Sgm (seq ((len g),(len f)))) * (g ^ f) proofend; theorem Th17: :: CALCUL_2:17 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al holds dom (Seq ((g ^ f) | (seq ((len g),(len f))))) = dom f proofend; 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 proofend; 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 proofend; 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 proofend; 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*> proofend; begin 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 ) ) proofend; 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 Element of 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 Element of 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 ) ) ) proofend; 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 Element of 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 Element of 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 proofend; 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 Element of 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*> proofend; 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*> proofend; 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*> proofend; 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*> proofend; 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*> proofend; 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*> proofend; 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)*> proofend; theorem Th28: :: CALCUL_2:28 for Al being QC-alphabet for g, f being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds |- f ^ <*(Impl (Rev g))*> proofend; 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*> proofend; 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*> proofend; begin 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*> proofend; 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 proofend; 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*> proofend;