:: Consequences of the Sequent Calculus :: by Patrick Braselmann and Peter Koepke :: :: Received September 25, 2004 :: Copyright (c) 2004-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, CQC_LANG, FINSEQ_1, ARYTM_3, XXREAL_0, TARSKI, CARD_1, XBOOLE_0, NAT_1, FINSET_1, RELAT_1, ORDINAL4, FUNCT_1, CALCUL_1, FUNCT_2, CQC_THE1, QC_LANG1, XBOOLEAN, FINSEQ_5, ARYTM_1, FINSEQ_2, CALCUL_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, CARD_1, NUMBERS, XXREAL_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, QC_LANG1, CQC_LANG, FINSET_1, FINSEQ_5, FINSEQ_2, RELSET_1, FUNCT_2, WELLORD2, CALCUL_1; constructors PARTFUN1, WELLORD2, XXREAL_0, REAL_1, NAT_1, INT_1, FINSEQ_2, FINSEQ_5, CALCUL_1, RELSET_1, QC_LANG1; registrations FUNCT_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, CQC_LANG, FUNCT_2, FINSEQ_2, CARD_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: f is Subsequence of g^f reserve Al for QC-alphabet; reserve p,q,p1,p2,q1 for Element of CQC-WFF(Al), k,m,n,i for Element of NAT, f, f1,f2,g for FinSequence of CQC-WFF(Al), a,b,b1,b2,c for Nat; definition let m,n be Nat; func seq(m,n) -> set equals :: CALCUL_2:def 1 {k : 1+m <= k & k <= n+m }; end; definition let m,n be Nat; redefine func seq(m,n) -> Subset of NAT; end; theorem :: CALCUL_2:1 c in seq(a,b) iff 1+a <= c & c <= b+a; theorem :: CALCUL_2:2 seq(a,0) = {}; theorem :: CALCUL_2:3 b = 0 or b+a in seq(a,b); theorem :: CALCUL_2:4 b1 <= b2 iff seq(a,b1) c= seq(a,b2); theorem :: CALCUL_2:5 seq(a,b) \/ {a+b+1} = seq(a,b+1); theorem :: CALCUL_2:6 seq(m,n),n are_equipotent; registration let m,n; cluster seq(m,n) -> finite; end; registration let Al; let f; cluster len f -> finite; end; theorem :: CALCUL_2:7 seq(m,n) c= Seg (m+n); theorem :: CALCUL_2:8 Seg n misses seq(n,m); theorem :: CALCUL_2:9 for f,g be FinSequence holds dom(f^g) = dom f \/ seq(len f,len g); theorem :: CALCUL_2:10 len Sgm(seq(len g,len f)) = len f; theorem :: CALCUL_2:11 dom Sgm(seq(len g,len f)) = dom f; theorem :: CALCUL_2:12 rng Sgm(seq(len g,len f)) = seq(len g,len f); theorem :: CALCUL_2:13 i in dom Sgm(seq(len g,len f)) implies Sgm(seq(len g,len f)).i = len g+i; theorem :: CALCUL_2:14 seq(len g,len f) c= dom (g^f); theorem :: CALCUL_2:15 dom((g^f)|seq(len g,len f)) = seq(len g,len f); theorem :: CALCUL_2:16 Seq((g^f)|seq(len g,len f)) = Sgm(seq(len g,len f)) * (g^f); theorem :: CALCUL_2:17 dom Seq((g^f)|seq(len g,len f)) = dom f; theorem :: CALCUL_2:18 f is_Subsequence_of g^f; definition let D be non empty set, 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; end; reserve P for Permutation of dom f; theorem :: CALCUL_2:19 dom Per(f,P) = dom f; theorem :: CALCUL_2:20 |- f^<*p*> implies |- g^f^<*p*>; begin :: The Ordering of the Antecedent is Irrelevant definition let Al,f; func Begin(f) -> Element of CQC-WFF(Al) means :: CALCUL_2:def 3 it = f.1 if 1 <= len f otherwise it = VERUM(Al); end; definition let Al,f; assume 1 <= len f; func Impl(f) -> Element of CQC-WFF(Al) means :: 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 st p = f.(n+1) & q = F.n & F.(n+1) = p => q; end; :: Some details about the calculus in CALCUL_1 theorem :: CALCUL_2:21 |- f^<*p*>^<*p*>; theorem :: CALCUL_2:22 |- f^<*p '&' q*> implies |- f^<*p*>; theorem :: CALCUL_2:23 |- f^<*p '&' q*> implies |- f^<*q*>; theorem :: CALCUL_2:24 |- f^<*p*> & |- f^<*p*>^<*q*> implies |- f^<*q*>; theorem :: CALCUL_2:25 |- f^<*p*> & |- f^<*'not' p*> implies |- f^<*q*>; theorem :: CALCUL_2:26 |- f^<*p*>^<*q*> & |- f^<*'not' p*>^<*q*> implies |- f^<*q*>; theorem :: CALCUL_2:27 |- f^<*p*>^<*q*> implies |- f^<*p => q*>; theorem :: CALCUL_2:28 1 <= len g & |- f^g implies |- f^<*Impl(Rev g)*>; theorem :: CALCUL_2:29 |- Per(f,P)^<*Impl(Rev (f^<*p*>))*> implies |- Per(f,P)^<*p*>; theorem :: CALCUL_2:30 |- f^<*p*> implies |- Per(f,P)^<*p*>; begin :: Multiple Occurrence in the Antecedent is Irrelevant notation let n; let c be set; synonym IdFinS(c,n) for n |-> c; end; theorem :: CALCUL_2:31 for c being set st 1 <= n holds rng IdFinS(c,n) = rng <*c*>; definition let D be non empty set, n be Element of NAT, p be Element of D; redefine func IdFinS(p,n) -> FinSequence of D; end; theorem :: CALCUL_2:32 1 <= n & |- f^IdFinS(p,n)^<*q*> implies |- f^<*p*>^<*q*>;