:: Consequences of the Sequent Calculus
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2026 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, NUMBER09;
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;
definitions TARSKI, XBOOLE_0;
equalities FINSEQ_2, ORDINAL1;
expansions TARSKI;
theorems TARSKI, FINSEQ_1, FINSEQ_3, FUNCT_1, XBOOLE_0, FINSEQ_2, RELAT_1,
NAT_1, XBOOLE_1, FUNCT_2, CALCUL_1, QC_LANG2, CARD_1, ORDINAL1, FUNCT_4,
FINSEQ_5, INT_1, XREAL_1, XXREAL_0, FUNCOP_1, AFINSQ_1;
schemes NAT_1, RECDEF_1;
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 for Element of NAT,
f,f1,f2,g for FinSequence of CQC-WFF(Al),
a,b,b1,b2,c,i,n for Nat;
definition
let m,n be Nat;
func seq(m,n) -> set equals
{ k : 1+m <= k & k <= n+m };
coherence;
end;
definition
let m,n be Nat;
redefine func seq(m,n) -> Subset of NAT; :: redefines seq (CALCUL_2, definition)
coherence
proof
set X = seq(m,n);
X c= NAT
proof
let x be object;
assume x in X;
then ex i being Element of NAT st x = i & 1+m <= i & i <= n+m;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th1:
c in seq(a,b) iff 1+a <= c & c <= b+a
proof
A1: c in { m where m is Element of NAT: 1+a <= m & m <= b+a }
iff ex m being Element of NAT st c = m & 1+a <= m & m <= b+a;
c is Element of NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
theorem Th2:
seq(a,0) = {}
proof
hereby
set x =the Element of seq(a,0);
assume
A1: seq(a,0) <> {};
then reconsider x as Element of NAT by TARSKI:def 3;
1+a <= x & x <= 0+a by A1,Th1;
hence contradiction by NAT_1:13;
end;
end;
theorem Th3:
b = 0 or b+a in seq(a,b)
proof
assume b <> 0;
then ex c be Nat st b = c + 1 by NAT_1:6;
then 1 <= b by NAT_1:11;
then b+a is Element of NAT & 1+a <= b+a by ORDINAL1:def 12,XREAL_1:6;
hence thesis;
end;
theorem Th4:
b1 <= b2 iff seq(a,b1) c= seq(a,b2)
proof
thus b1 <= b2 implies seq(a,b1) c= seq(a,b2)
proof
assume b1 <= b2;
then
A1: b1+a <= b2+a by XREAL_1:6;
let b be object such that
A2: b in seq(a,b1);
reconsider c = b as Element of NAT by A2;
c <= b1+a by A2,Th1;
then
A3: c <= b2+a by A1,XXREAL_0:2;
1+a <= c by A2,Th1;
hence thesis by A3;
end;
assume
A4: seq(a,b1) c= seq(a,b2);
now
assume b1 <> 0;
then b1+a in seq(a,b1) by Th3;
then b1+a <= b2+a by A4,Th1;
hence thesis by XREAL_1:6;
end;
hence thesis;
end;
theorem Th5:
seq(a,b) \/ {a+b+1} = seq(a,b+1)
proof
thus seq(a,b) \/ {a+b+1} c= seq(a,b+1)
proof
b+0 <= b+1 by XREAL_1:7;
then
A1: seq(a,b) c= seq(a,b+1) by Th4;
let x be object;
assume x in seq(a,b) \/ {a+b+1};
then x in seq(a,b) or x in {a+b+1} by XBOOLE_0:def 3;
then x in seq(a,b+1) or x = a+(b+1) by A1,TARSKI:def 1;
hence thesis by Th3;
end;
let x be object such that
A2: x in seq(a,b+1);
reconsider x as Element of NAT by A2;
x <= b+1+a by A2,Th1;
then
A3: x <= a+b or x = a+b+1 by NAT_1:8;
1+a <= x by A2,Th1;
then x in seq(a,b) or x in {a+b+1} by A3,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th6:
seq(a,b),b are_equipotent
proof
defpred P[Nat] means seq(a,$1),$1 are_equipotent;
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: seq(a,n),n are_equipotent;
reconsider i = a+n as Nat;
A3: Segm(n+1) = Segm n \/ { n } by AFINSQ_1:2;
A4: now
assume seq(a,n) meets { i+1 };
then consider x being object such that
A5: x in seq(a,n) and
A6: x in { i+1 } by XBOOLE_0:3;
A7: not i+1 <= i by NAT_1:13;
x = i+1 by A6,TARSKI:def 1;
hence contradiction by A5,A7,Th1;
end;
A8: now
assume n meets { n };
then consider x being object such that
A9: x in n and
A10: x in { n } by XBOOLE_0:3;
A: x = n by A10,TARSKI:def 1;
reconsider x as set by TARSKI:1;
not x in x;
hence contradiction by A,A9;
end;
seq(a,n+1) = seq(a,n) \/ { i+1 } & { i+1 },{ n } are_equipotent
by Th5,CARD_1:28;
hence thesis by A2,A3,A8,A4,CARD_1:31;
end;
A11: P[0] by Th2;
for n being Nat holds P[n] from NAT_1:sch 2(A11,A1);
hence thesis;
end;
registration
let a,b;
cluster seq(a,b) -> finite;
coherence
proof
b is finite & b,seq(a,b) are_equipotent by Th6;
hence thesis by CARD_1:38;
end;
end;
registration
let Al;
let f;
cluster len f -> finite;
coherence;
end;
theorem Th7:
seq(a,b) c= Seg (a+b)
proof
let x be object;
A1: 1 <= 1+a by NAT_1:11;
assume
A2: x in seq(a,b);
then reconsider x as Element of NAT;
1+a <= x by A2,Th1;
then
A3: 1 <= x by A1,XXREAL_0:2;
x <= b+a by A2,Th1;
hence thesis by A3,FINSEQ_1:1;
end;
registration
let a,b;
cluster seq(a,b) -> included_in_Seg;
coherence
proof
seq(a,b) c= Seg (a+b) by Th7;
hence thesis by FINSEQ_1:def 13;
end;
end;
theorem
Seg a misses seq(a,b)
proof
assume Seg a meets seq(a,b);
then consider a1 being object such that
A1: a1 in Seg a and
A2: a1 in seq(a,b) by XBOOLE_0:3;
reconsider i = a1 as Element of NAT by A1;
i <= a & a+1 <= i by A1,A2,Th1,FINSEQ_1:1;
hence contradiction by NAT_1:13;
end;
theorem
for f,g be FinSequence holds dom(f^g) = dom f \/ seq(len f,len g)
proof
let f,g be FinSequence;
now
let a be object such that
A1: a in dom(f^g);
reconsider i = a as Element of NAT by A1;
A2: 1 <= i by A1,FINSEQ_3:25;
A3: i <= len(f^g) by A1,FINSEQ_3:25;
per cases;
suppose
A4: i <= len f;
A5: dom f c= dom f \/ seq(len f,len g) by XBOOLE_1:7;
i in dom f by A2,A4,FINSEQ_3:25;
hence a in dom f \/ seq(len f,len g) by A5;
end;
suppose
A6: len f < i;
A7: seq(len f,len g) c= dom f \/ seq(len f,len g) by XBOOLE_1:7;
A8: i <= len f+len g by A3,FINSEQ_1:22;
len f+1 <= i by A6,NAT_1:13;
then a in seq(len f,len g) by A8;
hence a in dom f \/ seq(len f,len g) by A7;
end;
end;
hence dom(f^g) c= dom f \/ seq(len f,len g);
let a be object such that
A9: a in dom f \/ seq(len f,len g);
per cases by A9,XBOOLE_0:def 3;
suppose
A10: a in dom f;
then reconsider i = a as Element of NAT;
A11: 1 <= i by A10,FINSEQ_3:25;
A12: len f <= len (f^g) by CALCUL_1:6;
i <= len f by A10,FINSEQ_3:25;
then i <= len (f^g) by A12,XXREAL_0:2;
hence thesis by A11,FINSEQ_3:25;
end;
suppose
A13: a in seq(len f,len g);
then reconsider i = a as Element of NAT;
i <= len g+len f by A13,Th1;
then
A14: i <= len (f^g) by FINSEQ_1:22;
A15: 1 <= 1+len f by NAT_1:11;
1+len f <= i by A13,Th1;
then 1 <= i by A15,XXREAL_0:2;
hence thesis by A14,FINSEQ_3:25;
end;
end;
theorem Th10:
len Sgm(seq(len g,len f)) = len f
proof
seq(len g,len f),len f are_equipotent by Th6;
then card seq(len g,len f) = card len f by CARD_1:5;
hence thesis by FINSEQ_3:39;
end;
theorem Th11:
dom Sgm(seq(len g,len f)) = dom f
proof
len Sgm(seq(len g,len f)) = len f by Th10;
hence thesis by FINSEQ_3:29;
end;
theorem Th12:
rng Sgm(seq(len g,len f)) = seq(len g,len f) by FINSEQ_1:def 14;
theorem Th13:
i in dom Sgm(seq(len g,len f)) implies Sgm(seq(len g,len f)).i = len g+i
proof
defpred P[Nat] means 1 <= $1 & $1 <= len f implies
for i being Nat st 1 <= i & i <= $1 holds Sgm(seq(len g,len f)).i = len g+i;
assume
A1: i in dom Sgm(seq(len g,len f));
then i in dom f by Th11;
then
A2: i <= len f by FINSEQ_3:25;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
assume that
A5: 1 <= k+1 and
A6: k+1 <= len f;
let n be Nat such that
A7: 1 <= n and
A8: n <= k+1;
A9: now
assume
A10: n = k+1;
dom Sgm(seq(len g,len f)) = dom f by Th11;
then n in dom Sgm(seq(len g,len f)) by A5,A6,A10,FINSEQ_3:25;
then Sgm(seq(len g,len f)).n in rng Sgm(seq(len g,len f)) by FUNCT_1:3;
then reconsider i = Sgm(seq(len g,len f)).n as Element of NAT;
A11: now
assume
A12: i < len g+(k+1);
A13: now
assume k <> 0;
then
A14: 0+1 <= k by NAT_1:13;
then
A15: Sgm(seq(len g,len f)).k = len g+k by A4,A6,NAT_1:13;
then reconsider j = Sgm(seq(len g,len f)).k as Nat;
A17: k < k+1 & k+1 <= len Sgm(seq(len g,len f)) by A6,Th10,NAT_1:13;
i < len g+k+1 by A12;
then i <= j by A15,NAT_1:13;
hence contradiction by A10,A14,A17,FINSEQ_1:def 14;
end;
now
1 <= len f by A5,A6,XXREAL_0:2;
then 1 in dom f by FINSEQ_3:25;
then
A18: 1 in dom Sgm(seq(len g,len f)) by Th11;
assume
A19: k = 0;
then not i in seq(len g,len f) by A12,Th1;
then not i in rng Sgm(seq(len g,len f)) by Th12;
hence contradiction by A10,A19,A18,FUNCT_1:3;
end;
hence contradiction by A13;
end;
now
1+len g <= 1+len g+k & len g+(k+1) <= len f+len g
by A6,NAT_1:11,XREAL_1:6;
then len g+(k+1) in seq(len g,len f);
then len g+(k+1) in rng Sgm(seq(len g,len f)) by Th12;
then consider l being Nat such that
A20: l in dom Sgm(seq(len g,len f)) and
A21: Sgm(seq(len g,len f)).l = len g+(k+1) by FINSEQ_2:10;
assume
A22: i > len g+(k+1);
A23: now
A24: now
assume
A25: l <= k;
now
assume 1 <= l;
then len g+(k+1) = len g+l by A4,A6,A21,A25,NAT_1:13
,XXREAL_0:2;
hence contradiction by A25,NAT_1:13;
end;
hence contradiction by A20,FINSEQ_3:25;
end;
assume l <= k+1;
hence contradiction by A10,A22,A21,A24,NAT_1:8;
end;
A26: 1 <= n & seq(len g,len f) c= Seg (len g+len f) by A10,Th7,NAT_1:11;
l <= len Sgm(seq(len g,len f)) by A20,FINSEQ_3:25;
hence contradiction by A10,A22,A21,A23,A26,FINSEQ_1:def 14;
end;
hence thesis by A10,A11,XXREAL_0:1;
end;
n <= k implies thesis by A4,A6,A7,NAT_1:13,XXREAL_0:2;
hence thesis by A8,A9,NAT_1:8;
end;
A27: P[0];
A28: for n being Nat holds P[n] from NAT_1:sch 2(A27,A3);
1 <= i by A1,FINSEQ_3:25;
hence thesis by A2,A28;
end;
theorem Th14:
seq(len g,len f) c= dom (g^f)
proof
let a be object such that
A1: a in seq(len g,len f);
reconsider n = a as Element of NAT by A1;
n <= len f+len g by A1,Th1;
then
A2: n <= len (g^f) by FINSEQ_1:22;
A3: 1 <= 1+len g by NAT_1:11;
1+len g <= n by A1,Th1;
then 1 <= n by A3,XXREAL_0:2;
hence a in dom (g^f) by A2,FINSEQ_3:25;
end;
theorem Th15:
dom((g^f)|seq(len g,len f)) = seq(len g,len f)
proof
dom((g^f)|seq(len g,len f)) = dom (g^f) /\ seq(len g,len f) by RELAT_1:61;
hence thesis by Th14,XBOOLE_1:28;
end;
theorem Th16:
Seq((g^f)|seq(len g,len f)) = Sgm(seq(len g,len f)) * (g^f)
proof
reconsider gf = (g^f)|seq(len g,len f) as FinSubsequence;
Seq(gf) = gf * Sgm(dom(gf)) by FINSEQ_1:def 15
.= gf * Sgm(seq(len g,len f)) by Th15
.= (((g^f)|rng Sgm(seq(len g,len f))) qua Function) * (Sgm(seq(len g,len
f)) qua Function) by Th12
.= ((g^f) qua Function) * (Sgm(seq(len g,len f))qua Function) by FUNCT_4:2;
hence thesis;
end;
theorem Th17:
dom Seq((g^f)|seq(len g,len f)) = dom f
proof
rng Sgm(seq(len g,len f)) = seq(len g,len f) by Th12;
then
A1: rng Sgm(seq(len g,len f)) c= dom (g^f) by Th14;
dom Seq((g^f)|seq(len g,len f)) = dom (Sgm(seq(len g,len f)) * (g^f))
by Th16;
then dom Seq((g^f)|seq(len g,len f)) = dom Sgm(seq(len g,len f))
by A1,RELAT_1:27;
hence thesis by Th11;
end;
theorem Th18:
f is_Subsequence_of g^f
proof
A1: for i be Nat st i in dom Seq((g^f)|seq(len g,len f)) holds Seq((g^f)|seq
(len g,len f)).i = f.i
proof
let i be Nat;
assume i in dom Seq((g^f)|seq(len g,len f));
then
A2: i in dom f by Th17;
then
A3: i in dom Sgm(seq(len g,len f)) by Th11;
Seq((g^f)|seq(len g,len f)).i = (Sgm(seq(len g,len f)) * (g^f)).i by Th16;
then Seq((g^f)|seq(len g,len f)).i = (g^f).(Sgm(seq(len g,len f)).i) by A3,
FUNCT_1:13;
then Seq((g^f)|seq(len g,len f)).i = (g^f).(len g+i) by A3,Th13;
hence thesis by A2,FINSEQ_1:def 7;
end;
dom Seq((g^f)|seq(len g,len f)) = dom f by Th17;
then Seq((g^f)|seq(len g,len f)) = f by A1,FINSEQ_1:13;
hence thesis by CALCUL_1:def 4;
end;
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
P*f;
coherence
proof
A1: rng P = dom f by FUNCT_2:def 3;
then dom (P*f) = dom P by RELAT_1:27;
then dom (P*f) = dom f by FUNCT_2:52;
then ex n being Nat st dom (P*f) = Seg n by FINSEQ_1:def 2;
then reconsider F = P*f as FinSequence by FINSEQ_1:def 2;
rng F = rng f by A1,RELAT_1:28;
hence thesis by FINSEQ_1:def 4;
end;
end;
reserve P for Permutation of dom f;
theorem Th19:
dom Per(f,P) = dom f
proof
rng P = dom f by FUNCT_2:def 3;
then dom (P*f) = dom P by RELAT_1:27;
hence thesis by FUNCT_2:52;
end;
theorem Th20:
|- f^<*p*> implies |- g^f^<*p*>
proof
Suc(f^<*p*>) = p by CALCUL_1:5;
then
A1: Suc(f^<*p*>) = Suc(g^f^<*p*>) by CALCUL_1:5;
Ant(f^<*p*>) = f by CALCUL_1:5;
then Ant(f^<*p*>) is_Subsequence_of g^f by Th18;
then
A2: Ant(f^<*p*>) is_Subsequence_of Ant(g^f^<*p*>) by CALCUL_1:5;
assume |- f^<*p*>;
hence thesis by A2,A1,CALCUL_1:36;
end;
begin :: The Ordering of the Antecedent is Irrelevant
definition
let Al,f;
func Begin(f) -> Element of CQC-WFF(Al) means
:Def3:
it = f.1 if 1 <= len f otherwise it = VERUM(Al);
existence
proof
1 <= len f implies ex p st p = f.1
proof
assume 1 <= len f;
then 1 in dom f by FINSEQ_3:25;
then f.1 in CQC-WFF(Al) by FINSEQ_2:11;
hence thesis;
end;
hence thesis;
end;
uniqueness;
consistency;
end;
definition
let Al,f;
assume
A1: 1 <= len f;
func Impl(f) -> Element of CQC-WFF(Al) means
:Def4:
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;
existence
proof
defpred P[Nat,set,set] means ex p,q st p = f.($1+1) & q = $2 &
$3 = p => q;
A2: for n being Nat st 1 <= n & n < len f
for x being Element of CQC-WFF(Al) ex y
being Element of CQC-WFF(Al) st P[n,x,y]
proof
let n be Nat such that
1 <= n and
A3: n < len f;
1 <= n+1 & n+1 <= len f by A3,NAT_1:11,13;
then n+1 in dom f by FINSEQ_3:25;
then reconsider p = f.(n+1) as Element of CQC-WFF(Al) by FINSEQ_2:11;
let x be Element of CQC-WFF(Al);
take p => x,p,x;
thus thesis;
end;
consider F being FinSequence of CQC-WFF(Al) such that
A4: len F = len f & (F.1 = Begin(f) or len f = 0) &
for n being Nat st 1 <= n &
n < len f holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 4(A2);
len f in dom F by A1,A4,FINSEQ_3:25;
then reconsider p = F.(len f) as Element of CQC-WFF(Al) by FINSEQ_2:11;
take p;
thus thesis by A4;
end;
uniqueness
proof
defpred P[Nat,set,set] means ex p,q st p = f.($1+1) & q = $2 &
$3 = p => q;
let p1,p2 such that
A5: ex F being FinSequence of CQC-WFF(Al) st p1 = 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 P[n,F.n,F
.(n+1)] and
A6: ex F being FinSequence of CQC-WFF(Al) st p2 = 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 P[n,F.n,F
.(n+1)];
consider H being FinSequence of CQC-WFF(Al) such that
A7: p2 = H.(len f) and
A8: len H = len f & (H.1 = Begin(f) or len f = 0) &
for n being Nat st 1 <= n &
n < len f holds P[n,H.n,H.(n+1)] by A6;
consider G being FinSequence of CQC-WFF(Al) such that
A9: p1 = G.(len f) and
A10: len G = len f & (G.1 = Begin(f) or len f = 0) &
for n being Nat st 1 <= n &
n < len f holds P[n,G.n,G.(n+1)] by A5;
A11: for n being Nat st 1 <= n & n < len f
for x,y1,y2 being Element of CQC-WFF(Al) st P
[n,x,y1] & P[n,x,y2] holds y1 = y2;
G = H from RECDEF_1:sch 8(A11,A10,A8);
hence thesis by A9,A7;
end;
end;
:: Some details about the calculus in CALCUL_1
theorem Th21:
|- f^<*p*>^<*p*>
proof
len(f^<*p*>) in dom(f^<*p*>) by CALCUL_1:10;
then len f + len <*p*> in dom(f^<*p*>) by FINSEQ_1:22;
then
A1: len f+1 in dom(f^<*p*>) by FINSEQ_1:39;
(f^<*p*>).(len f+1) = p by FINSEQ_1:42;
then p is_tail_of f^<*p*> by A1,CALCUL_1:def 16;
then Suc(f^<*p*>^<*p*>) is_tail_of f^<*p*> by CALCUL_1:5;
then Suc(f^<*p*>^<*p*>) is_tail_of Ant(f^<*p*>^<*p*>) by CALCUL_1:5;
hence thesis by CALCUL_1:33;
end;
theorem Th22:
|- f^<*p '&' q*> implies |- f^<*p*>
proof
A1: p '&' q = Suc(f^<*p '&' q*>) by CALCUL_1:5;
assume |- f^<*p '&' q*>;
then |- Ant(f^<*p '&' q*>)^<*p*> by A1,CALCUL_1:40;
hence thesis by CALCUL_1:5;
end;
theorem Th23:
|- f^<*p '&' q*> implies |- f^<*q*>
proof
A1: p '&' q = Suc(f^<*p '&' q*>) by CALCUL_1:5;
assume |- f^<*p '&' q*>;
then |- Ant(f^<*p '&' q*>)^<*q*> by A1,CALCUL_1:41;
hence thesis by CALCUL_1:5;
end;
theorem Th24:
|- f^<*p*> & |- f^<*p*>^<*q*> implies |- f^<*q*>
proof
A1: 1 <= len (f^<*p*>) by CALCUL_1:10;
assume |- f^<*p*> & |- f^<*p*>^<*q*>;
then |- Ant(f^<*p*>)^<*q*> by A1,CALCUL_1:45;
hence thesis by CALCUL_1:5;
end;
theorem Th25:
|- f^<*p*> & |- f^<*'not' p*> implies |- f^<*q*>
proof
A1: Ant(f^<*p*>) = f & Suc(f^<*p*>) = p by CALCUL_1:5;
assume |- f^<*p*> & |- f^<*'not' p*>;
hence thesis by A1,CALCUL_1:44;
end;
theorem Th26:
|- f^<*p*>^<*q*> & |- f^<*'not' p*>^<*q*> implies |- f^<*q*>
proof
set f1 = f^<*p*>^<*q*>;
set f2 = f^<*'not' p*>^<*q*>;
assume
A1: |- f1 & |- f2;
A2: Ant(f2) = f^<*'not' p*> by CALCUL_1:5;
A3: Ant(f1) = f^<*p*> by CALCUL_1:5;
then Suc(Ant(f1)) = p by CALCUL_1:5;
then
A4: 'not' Suc(Ant(f1)) = Suc(Ant(f2)) by A2,CALCUL_1:5;
A5: 1 < len f1 & 1 < len f2 by CALCUL_1:9;
A6: Suc(f1) = q by CALCUL_1:5;
then
A7: Suc(f1) = Suc(f2) by CALCUL_1:5;
A8: Ant(Ant(f1)) = f by A3,CALCUL_1:5;
then Ant(Ant(f1)) = Ant(Ant(f2)) by A2,CALCUL_1:5;
hence thesis by A1,A8,A4,A6,A5,A7,CALCUL_1:37;
end;
theorem Th27:
|- f^<*p*>^<*q*> implies |- f^<*p => q*>
proof
assume
A1: |- f^<*p*>^<*q*>;
set g1 = f^<*p '&' 'not' q*>^<*p*>^<*q*>;
set g = f^<*p*>^<*q*>;
A2: Ant(g1) = f^<*p '&' 'not' q*>^<*p*> by CALCUL_1:5;
Suc(g) = q by CALCUL_1:5;
then
A3: Suc(g1) = Suc(g) by CALCUL_1:5;
A4: Ant(g) = f^<*p*> by CALCUL_1:5;
then
A5: 0+1 <= len Ant(g) by CALCUL_1:10;
A6: |- f^<*p '&' 'not' q*>^<*p '&' 'not' q*> by Th21;
then
A7: |- f^<*p '&' 'not' q*>^<*p*> by Th22;
Ant(Ant(g)) = f & Suc(Ant(g)) = p by A4,CALCUL_1:5;
then |- g1 by A1,A5,A3,A2,CALCUL_1:13,36;
then
A8: |- f^<*p '&' 'not' q*>^<*q*> by A7,Th24;
A9: |- f^<*'not' (p '&' 'not' q)*>^<*'not' (p '&' 'not' q)*> by Th21;
|- f^<*p '&' 'not' q*>^<*'not' q*> by A6,Th23;
then |- f^<*p '&' 'not' q*>^<*'not' (p '&' 'not' q)*> by A8,Th25;
then |- f^<*'not' (p '&' 'not' q)*> by A9,Th26;
hence thesis by QC_LANG2:def 2;
end;
theorem Th28:
1 <= len g & |- f^g implies |- f^<*Impl(Rev g)*>
proof
set h = Rev g;
assume that
A1: 1 <= len g and
A2: |- f^g;
A3: 1 <= len h by A1,FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF(Al) such that
A4: Impl(h) = F.(len h) and
A5: len F = len h and
A6: F.1 = Begin(h) or len h = 0 and
A7: for n being Nat st 1 <= n & n < len h
ex p,q st p = h.(n+1) & q = F.n &
F.(n+1) = p => q by Def4;
A8: 1 <= len h by A1,FINSEQ_5:def 3;
defpred P[Nat] means 1 <= $1 & $1 <= len F implies ex f1,f2,n st
$1+n = len (f^g) & f1 = (f^g)|Seg n & f2 = f1^<*F.$1*> & |- f2;
A9: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A10: P[k];
A11: len g <= len (f^g) by CALCUL_1:6;
assume that
A12: 1 <= k+1 and
A13: k+1 <= len F;
A14: k+1 <= len g by A5,A13,FINSEQ_5:def 3;
then consider n being Nat such that
A15: len (f^g) = (k+1)+n by A11,NAT_1:10,XXREAL_0:2;
reconsider n as Element of NAT by ORDINAL1:def 12;
A16: now
k+1 in dom F by A12,A13,FINSEQ_3:25;
then reconsider r = F.(k+1) as Element of CQC-WFF(Al) by FINSEQ_2:11;
set f1 = (f^g)|Seg n;
reconsider f1 as FinSequence of CQC-WFF(Al) by FINSEQ_1:18;
set f2 = f1^<*r*>;
len(f^g) <= len(f^g) + k by NAT_1:11;
then
A17: len(f^g) - k <= len(f^g) + k - k by XREAL_1:9;
assume k <> 0;
then
A18: 0+1 <= k by NAT_1:13;
then consider f1k being FinSequence of CQC-WFF(Al) such that
A19: ex f2,n st k+n = len (f^g) & f1k = (f^g)|Seg n & f2 = f1k^<*F.k
*> & |- f2 by A10,A13,NAT_1:13;
consider f2k being FinSequence of CQC-WFF(Al) such that
A20: ex n st k+n = len (f^g) & f1k = (f^g)|Seg n & f2k = f1k^<*F.k*>
& |- f2k by A19;
consider nk being Nat such that
A21: k+nk = len (f^g) and
A22: f1k = (f^g)|Seg nk & f2k = f1k^<*F.k*> and
A23: |- f2k by A20;
1 <= n+1 by NAT_1:11;
then
A24: nk in dom (f^g) by A15,A21,A17,FINSEQ_3:25;
then reconsider p = (f^g).nk as Element of CQC-WFF(Al) by FINSEQ_2:11;
n+1 = nk by A15,A21;
then
A25: f2k = f1^<*(f^g).nk*>^<*F.k*> by A22,A24,FINSEQ_5:10;
A26: k < len h by A5,A13,NAT_1:13;
then consider p1,q1 such that
A27: p1 = h.(k+1) and
A28: q1 = F.k & F.(k+1) = p1 => q1 by A7,A18;
k+1 in dom h by A5,A12,A13,FINSEQ_3:25;
then k+1 in dom g by FINSEQ_5:57;
then
A29: p1 = g.(len g - (k+1) +1) by A27,FINSEQ_5:58
.= g.(len g - k);
k < len g by A26,FINSEQ_5:def 3;
then
A30: k+(-k) < len g+(-k) by XREAL_1:8;
then reconsider i = len g-k as Element of NAT by INT_1:3;
len g <= k+len g by NAT_1:11;
then
A31: i <= len g by XREAL_1:20;
0+1 <= i by A30,INT_1:7;
then i in dom g by A31,FINSEQ_3:25;
then p1 = (f^g).(len f+i) by A29,FINSEQ_1:def 7
.= (f^g).(len f+len g-k)
.= (f^g).(len(f^g)-k) by FINSEQ_1:22
.= p by A21;
then |- f2 by A23,A25,A28,Th27;
hence thesis by A15;
end;
A32: k+1 <= len (f^g) by A14,A11,XXREAL_0:2;
now
F.1 = h.1 by A3,A6,Def3;
then
A33: F.1 = g.(len g) by FINSEQ_5:62;
set f1 = (f^g)|Seg n;
reconsider f1 as FinSequence of CQC-WFF(Al) by FINSEQ_1:18;
set f2 = f1^<*F.1*>;
A34: len g in dom g by A1,FINSEQ_3:25;
assume
A35: k = 0;
then
A36: (f^g).(n+1) = (f^g).(len f+len g) by A15,FINSEQ_1:22;
1 <= len(f^g) by A12,A32,XXREAL_0:2;
then len(f^g) in dom (f^g) by FINSEQ_3:25;
then (f^g)|Seg(n+1) = f1^<*(f^g).(n+1)*> by A15,A35,FINSEQ_5:10;
then f2 = (f^g)|Seg(len (f^g)) by A15,A35,A33,A34,A36,FINSEQ_1:def 7;
then
A37: f2 = (f^g)|dom(f^g) by FINSEQ_1:def 3;
then reconsider f2 as FinSequence of CQC-WFF(Al) by RELAT_1:69;
take f1,f2,n;
|- f2 by A2,A37,RELAT_1:69;
hence thesis by A15,A35;
end;
hence thesis by A16;
end;
A38: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A38,A9);
then consider f1 such that
A39: ex f2,n st len h+n = len (f^g) & f1 = (f^g)|Seg n & f2 = f1^<*F.(
len h)*> & |- f2 by A5,A8;
consider f2 such that
A40: ex n st len h+n = len (f^g) & f1 = (f^g)|Seg n & f2 = f1^<*F.(len h
)*> & |- f2 by A39;
consider n such that
A41: len h+n = len (f^g) and
A42: f1 = (f^g)|Seg n & f2 = f1^<*F.(len h)*> & |- f2 by A40;
n+len h-len h = len(f^g)-len g by A41,FINSEQ_5:def 3;
then n+len h+(-len h) = len f + len g-len g by FINSEQ_1:22;
then Seg n = dom f by FINSEQ_1:def 3;
hence thesis by A4,A42,FINSEQ_1:21;
end;
theorem Th29:
|- Per(f,P)^<*Impl(Rev (f^<*p*>))*> implies |- Per(f,P)^<*p*>
proof
set g = f^<*p*>;
set h = Rev g;
A1: 1 <= len g by CALCUL_1:10;
then
A2: 1 <= len h by FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF(Al) such that
A3: Impl(h) = F.(len h) and
A4: len F = len h and
A5: F.1 = Begin(h) or len h = 0 and
A6: for n being Nat st 1 <= n & n < len h
ex p,q st p = h.(n+1) & q = F.n &
F.(n+1) = p => q by Def4;
set H = Rev F;
A7: 1 <= len H by A2,A4,FINSEQ_5:def 3;
defpred P[Nat] means 1 <= $1 & $1 <= len H implies ex p st p = H.
$1 & |- Per(f,P)^<*p*>;
assume
A8: |- Per(f,P)^<*Impl(Rev (f^<*p*>))*>;
A9: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A10: P[k];
assume that
A11: 1 <= k+1 and
A12: k+1 <= len H;
A13: now
A14: k < len H by A12,NAT_1:13;
then 0+k < len F by FINSEQ_5:def 3;
then
A15: 0+k+(-k) < len F+(-k) by XREAL_1:8;
then reconsider i = len F-k as Element of NAT by INT_1:3;
A16: len g-i = len g - (len g-k) by A4,FINSEQ_5:def 3
.= k;
then reconsider j = len g-i as Nat;
A17: 0+1 <= i by A15,NAT_1:13;
then
A18: 1 <= i+1 by NAT_1:13;
assume
A19: k <> 0;
then
A20: 0+1 <= k by NAT_1:13;
then consider pk being Element of CQC-WFF(Al) such that
A21: pk = H.k and
A22: |- Per(f,P)^<*pk*> by A10,A12,NAT_1:13;
len F < len F+k by A19,XREAL_1:29;
then
A23: len F+(-k) < len F+k+(-k) by XREAL_1:8;
then consider p1,q1 such that
A24: p1 = h.(i+1) and
A25: q1 = F.i and
A26: F.(i+1) = p1 => q1 by A4,A6,A17;
take q1;
k+1 in dom H by A11,A12,FINSEQ_3:25;
then i = len F-(k+1)+1 & k+1 in dom F by FINSEQ_5:57;
then
A27: q1 = H.(k+1) by A25,FINSEQ_5:58;
len g < len g+i by A15,XREAL_1:29;
then len g+(-i) < len g+i+(-i) by XREAL_1:8;
then j < len f+len <*p*> by FINSEQ_1:22;
then j < len f+1 by FINSEQ_1:39;
then j <= len f by NAT_1:13;
then
A28: j in dom f by A20,A16,FINSEQ_3:25;
then
A29: g.j = (g|dom f).j by FUNCT_1:49;
j in rng P by A28,FUNCT_2:def 3;
then consider a being object such that
A30: a in dom P and
A31: P.a = j by FUNCT_1:def 3;
A32: a in dom f by A30;
then reconsider j1 = a as Element of NAT;
set g1 = Per(f,P)^<*p1*>;
i+1 <= len h by A4,A23,NAT_1:13;
then i+1 in dom h by A18,FINSEQ_3:25;
then i+1 in dom g by FINSEQ_5:57;
then p1 = g.(len g - (i+1) + 1) by A24,FINSEQ_5:58
.= g.(len g - i);
then p1 = f.(P.j1) by A29,A31,FINSEQ_1:21;
then p1 = (P*f).j1 by A30,FUNCT_1:13;
then Suc(g1) = Per(f,P).j1 by CALCUL_1:5;
then
A33: Suc(g1) = (Ant(g1)).j1 by CALCUL_1:5;
j1 in dom Per(f,P) by A32,Th19;
then j1 in dom Ant(g1) by CALCUL_1:5;
then Suc(g1) is_tail_of Ant(g1) by A33,CALCUL_1:def 16;
then
A34: |- g1 by CALCUL_1:33;
k in dom H by A20,A14,FINSEQ_3:25;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by A21,A26,FINSEQ_5:58;
then |- Per(f,P)^<*q1*> by A22,A34,CALCUL_1:56;
hence thesis by A27;
end;
now
1 <= len H by A2,A4,FINSEQ_5:def 3;
then
A35: 1 in dom H by FINSEQ_3:25;
then reconsider p = H.1 as Element of CQC-WFF(Al) by FINSEQ_2:11;
assume
A36: k = 0;
take p;
1 in dom F by A35,FINSEQ_5:57;
then p = F.(len F-1+1) by FINSEQ_5:58
.= Impl(h) by A3,A4;
hence thesis by A8,A36;
end;
hence thesis by A13;
end;
A37: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A37,A9);
then consider q such that
A38: q = H.(len H) and
A39: |- Per(f,P)^<*q*> by A7;
q = H.(len F) by A38,FINSEQ_5:def 3;
then q = Begin(h) by A1,A5,FINSEQ_5:62,def 3;
then q = h.1 by A2,Def3;
then q = g.(len g) by FINSEQ_5:62;
then q = g.(len f+len <*p*>) by FINSEQ_1:22;
then q = g.(len f+1) by FINSEQ_1:39;
hence thesis by A39,FINSEQ_1:42;
end;
theorem
|- f^<*p*> implies |- Per(f,P)^<*p*>
proof
set g = f^<*p*>;
assume |- f^<*p*>;
then |- Per(f,P)^f^<*p*> by Th20;
then
A1: |- Per(f,P)^g by FINSEQ_1:32;
1 <= len(g) by CALCUL_1:10;
then |- Per(f,P)^<*Impl(Rev g)*> by A1,Th28;
hence thesis by Th29;
end;
begin :: Multiple Occurrence in the Antecedent is Irrelevant
notation
let n be Nat;
let c be set;
synonym IdFinS(c,n) for n |-> c;
end;
theorem Th31:
for c being set st 1 <= n holds rng IdFinS(c,n) = rng <*c*>
proof
let c be set such that
A1: 1 <= n;
n in Seg n by A1,FINSEQ_1:1;
then
A2: IdFinS(c,n).n = c by FUNCOP_1:7;
thus rng IdFinS(c,n) c= rng <*c*>
proof
let a be object;
assume a in rng IdFinS(c,n);
then consider i being Nat such that
A3: i in dom IdFinS(c,n) and
A4: IdFinS(c,n).i = a by FINSEQ_2:10;
i in Seg len IdFinS(c,n) by A3,FINSEQ_1:def 3;
then i in Seg n by CARD_1:def 7;
then a = c by A4,FUNCOP_1:7;
then a in {c} by TARSKI:def 1;
hence thesis by FINSEQ_1:38;
end;
let a be object;
assume a in rng <*c*>;
then a in {c} by FINSEQ_1:38;
then
A5: a = c by TARSKI:def 1;
n = len IdFinS(c,n) by CARD_1:def 7;
then n in dom IdFinS(c,n) by A1,FINSEQ_3:25;
hence thesis by A5,A2,FUNCT_1:def 3;
end;
definition
let D be non empty set, n be Nat, p be Element of D;
redefine func IdFinS(p,n) -> FinSequence of D; :: redefines IdFinS (CALCUL_2, synonym) → |-> (FINSEQ_2, definition)
coherence
proof
now
let i be Nat;
assume i in dom IdFinS(p,n);
then i in Seg len IdFinS(p,n) by FINSEQ_1:def 3;
then i in Seg n by CARD_1:def 7;
then IdFinS(p,n).i = p by FUNCOP_1:7;
hence IdFinS(p,n).i in D;
end;
hence thesis by FINSEQ_2:12;
end;
end;
theorem
1 <= n & |- f^IdFinS(p,n)^<*q*> implies |- f^<*p*>^<*q*>
proof
assume that
A1: 1 <= n and
A2: |- f^IdFinS(p,n)^<*q*>;
set g = f^IdFinS(p,n)^<*q*>;
set h = Rev g;
A3: 1 <= len g by CALCUL_1:10;
then
A4: 1 <= len h by FINSEQ_5:def 3;
then consider F being FinSequence of CQC-WFF(Al) such that
A5: Impl(h) = F.(len h) and
A6: len F = len h and
A7: F.1 = Begin(h) or len h = 0 and
A8: for n being Nat st 1 <= n & n < len h
ex p,q st p = h.(n+1) & q = F.n &
F.(n+1) = p => q by Def4;
set H = Rev F;
A9: 1 <= len H by A4,A6,FINSEQ_5:def 3;
defpred P[Nat] means 1 <= $1 & $1 <= len H implies ex p1 st p1 =
H.$1 & |- f^<*p*>^<*p1*>;
|- f^<*p*>^(f^IdFinS(p,n))^<*q*> by A2,Th20;
then |- f^<*p*>^(f^IdFinS(p,n)^<*q*>) by FINSEQ_1:32;
then
A10: |- f^<*p*>^<*Impl(Rev g)*> by A3,Th28;
A11: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A12: P[k];
assume that
A13: 1 <= k+1 and
A14: k+1 <= len H;
A15: now
A16: k < len H by A14,NAT_1:13;
then 0+k < len F by FINSEQ_5:def 3;
then
A17: 0+k+(-k) < len F+(-k) by XREAL_1:8;
then reconsider i = len F-k as Element of NAT by INT_1:3;
A18: len g-i = len g - (len g-k) by A6,FINSEQ_5:def 3
.= k;
A19: 0+1 <= i by A17,NAT_1:13;
then
A20: 1 <= i+1 by NAT_1:13;
assume
A21: k <> 0;
then
A22: 0+1 <= k by NAT_1:13;
then consider pk being Element of CQC-WFF(Al) such that
A23: pk = H.k and
A24: |- f^<*p*>^<*pk*> by A12,A14,NAT_1:13;
len F < len F+k by A21,XREAL_1:29;
then
A25: len F+(-k) < len F+k+(-k) by XREAL_1:8;
then consider p1,q1 such that
A26: p1 = h.(i+1) and
A27: q1 = F.i and
A28: F.(i+1) = p1 => q1 by A6,A8,A19;
set g1 = f^<*p*>^<*p1*>;
A29: Suc(g1) = p1 by CALCUL_1:5;
len g < len g+i by A17,XREAL_1:29;
then len g+(-i) < len g+i+(-i) by XREAL_1:8;
then k < len(f^IdFinS(p,n)) + len <*q*> by FINSEQ_1:22,A18;
then k < len(f^IdFinS(p,n))+1 by FINSEQ_1:39;
then k <= len(f^IdFinS(p,n)) by NAT_1:13;
then
A30: k in dom (f^IdFinS(p,n)) by A22,FINSEQ_3:25;
then
A31: g.k = (g|dom(f^IdFinS(p,n))).k by FUNCT_1:49;
A32: (f^IdFinS(p,n)).k in rng (f^IdFinS(p,n)) by A30,FUNCT_1:3;
rng (f^IdFinS(p,n)) = (rng f \/ rng IdFinS(p,n)) by FINSEQ_1:31
.=(rng f \/ rng <*p*>) by A1,Th31
.= rng (f^<*p*>) by FINSEQ_1:31;
then
A33: (f^IdFinS(p,n)).k in rng Ant(g1) by A32,CALCUL_1:5;
i+1 <= len h by A6,A25,NAT_1:13;
then i+1 in dom h by A20,FINSEQ_3:25;
then i+1 in dom g by FINSEQ_5:57;
then p1 = g.(len g - (i+1) + 1) by A26,FINSEQ_5:58
.= g.(len g - i);
then p1 = (f^IdFinS(p,n)).k by A31,FINSEQ_1:21,A18;
then ex j1 being Nat st j1 in dom Ant(g1) & (Ant(g1)).j1 = p1 by A33,
FINSEQ_2:10;
then Suc(g1) is_tail_of Ant(g1) by A29,CALCUL_1:def 16;
then
A34: |- g1 by CALCUL_1:33;
take q1;
k+1 in dom H by A13,A14,FINSEQ_3:25;
then i = len F-(k+1)+1 & k+1 in dom F by FINSEQ_5:57;
then
A35: q1 = H.(k+1) by A27,FINSEQ_5:58;
k in dom H by A22,A16,FINSEQ_3:25;
then k in dom F by FINSEQ_5:57;
then pk = p1 => q1 by A23,A28,FINSEQ_5:58;
then |- f^<*p*>^<*q1*> by A24,A34,CALCUL_1:56;
hence thesis by A35;
end;
now
len H = len h by A6,FINSEQ_5:def 3;
then
A36: 1 in dom H by A4,FINSEQ_3:25;
then reconsider p1 = H.1 as Element of CQC-WFF(Al) by FINSEQ_2:11;
assume
A37: k = 0;
take p1;
1 in dom F by A36,FINSEQ_5:57;
then p1 = F.(len F-1+1) by FINSEQ_5:58
.= Impl(h) by A5,A6;
hence thesis by A10,A37;
end;
hence thesis by A15;
end;
A38: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A38,A11);
then consider p1 such that
A39: p1 = H.(len H) and
A40: |- f^<*p*>^<*p1*> by A9;
p1 = H.(len F) by A39,FINSEQ_5:def 3;
then p1 = Begin(h) by A3,A7,FINSEQ_5:62,def 3;
then p1 = h.1 by A4,Def3;
then p1 = g.(len g) by FINSEQ_5:62;
then p1 = g.(len(f^IdFinS(p,n))+len <*q*>) by FINSEQ_1:22;
then p1 = g.(len(f^IdFinS(p,n))+1) by FINSEQ_1:39;
hence thesis by A40,FINSEQ_1:42;
end;