:: A Sequent Calculus for First-Order Logic
:: 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, QC_LANG1, XBOOLE_0, VALUAT_1,
SUBSTUT1, FINSEQ_1, RELAT_1, ARYTM_3, XXREAL_0, CARD_1, NAT_1, TARSKI,
FUNCT_1, ORDINAL4, FINSEQ_2, ZFMISC_1, CQC_THE1, MCART_1, XBOOLEAN,
BVFUNC_2, ZF_MODEL, SUBSTUT2, SUBLEMMA, FUNCOP_1, FUNCT_4, FINSET_1,
ORDINAL1, CALCUL_1, NUMBER09;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FINSEQ_1, RELAT_1,
FUNCT_1, QC_LANG1, CARD_1, ORDINAL1, NUMBERS, FINSEQ_2, XXREAL_0,
XCMPLX_0, NAT_1, FUNCOP_1, CQC_LANG, FINSET_1, VALUAT_1, CQC_THE1,
RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, MCART_1, SUBSTUT1, SUBSTUT2,
SUBLEMMA;
constructors PARTFUN1, WELLORD2, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2,
CQC_THE1, SUBSTUT2, RELSET_1, XTUPLE_0, NUMBERS;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, FINSEQ_1, QC_LANG1, CQC_LANG, CARD_1, FINSEQ_2, RELAT_1,
XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, FINSEQ_2, FUNCOP_1;
expansions TARSKI;
theorems TARSKI, FUNCT_1, MCART_1, XBOOLE_0, XBOOLE_1, QC_LANG1, ZFMISC_1,
RELAT_1, QC_LANG3, QC_LANG2, SUBSTUT1, FUNCT_4, SUBLEMMA, NAT_1,
FINSEQ_1, FINSEQ_3, VALUAT_1, FINSEQ_2, SUBSTUT2, FUNCOP_1, CQC_THE1,
FINSET_1, CARD_2, CQC_SIM1, CARD_1, CARD_4, GRFUNC_1, XREAL_1, ORDINAL1,
XXREAL_0;
schemes XBOOLE_0, NAT_1, CLASSES1;
begin :: Preliminaries
reserve Al for QC-alphabet;
reserve a,b,c,d for object,
i,j,k,m,n for Nat,
p,q,r for Element of CQC-WFF(Al),
x,y,y0 for bound_QC-variable of Al,
X for Subset of CQC-WFF(Al),
A for non empty set,
J for interpretation of Al,A,
v,w for Element of Valuations_in(Al,A),
Sub for CQC_Substitution of Al,
f,f1,g,h,h1 for FinSequence of CQC-WFF(Al);
definition
let D be non empty set, f be FinSequence of D;
func Ant(f) -> FinSequence of D means
:Def1:
for i st len f = i+1 holds it = f|(Seg i) if len f > 0 otherwise it = {};
existence
proof
A1: len f > 0 implies ex g being FinSequence of D st for i st len f = i+1
holds g = f|(Seg i)
proof
assume len f > 0;
then consider j being Nat such that
A2: len f = j+1 by NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
take g = f|(Seg j);
reconsider g as FinSequence by FINSEQ_1:15;
now
A3: rng g c= rng f by RELAT_1:70;
let a be object;
assume a in rng g;
then a in rng f by A3;
hence a in D;
end;
then rng g c= D;
then reconsider g as FinSequence of D by FINSEQ_1:def 4;
for i st len f = i+1 holds g = f|(Seg i) by A2;
hence thesis;
end;
<*>D = {};
hence thesis by A1;
end;
uniqueness
proof
let g,h be FinSequence of D;
len f > 0 & (for i st len f = i+1 holds g = f|(Seg i)) & (for i st
len f = i+1 holds h = f|(Seg i)) implies g = h
proof
assume that
A4: len f > 0 and
A5: for i st len f = i+1 holds g = f|(Seg i) and
A6: for i st len f = i+1 holds h = f|(Seg i);
consider j being Nat such that
A7: len f = j+1 by A4,NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
g = f|(Seg j) by A5,A7;
hence thesis by A6,A7;
end;
hence thesis;
end;
consistency;
end;
definition
let Al;
let f be FinSequence of CQC-WFF(Al);
func Suc(f) -> Element of CQC-WFF(Al) equals
:Def2:
f.(len f) if len f > 0
otherwise VERUM(Al);
coherence
proof
per cases;
suppose len f > 0;
then 0+1 <= len f by NAT_1:13;
then len f in dom f by FINSEQ_3:25;
then f.(len f) in rng f by FUNCT_1:3;
hence thesis;
end;
suppose
A1: not len f > 0;
thus thesis by A1;
end;
end;
consistency;
end;
definition
let f be Relation, p be set;
pred p is_tail_of f means
p in rng f;
end;
Lm1: now
let f be FinSequence, p be set;
assume p is_tail_of f;
then p in rng f;
then consider i being object such that
A1: i in dom f and
A2: f.i = p by FUNCT_1:def 3;
reconsider i as Nat by A1;
take i;
thus i in dom f & f.i = p by A1,A2;
end;
Lm2:
for f be FinSequence, p be set st
ex i being Element of NAT st i in dom f & f.i = p holds
p is_tail_of f by FUNCT_1:def 3;
definition
let Al,f,g;
pred f is_Subsequence_of g means
ex N being Subset of NAT st f c= Seq (g|N);
end;
theorem Th1:
f is_Subsequence_of g implies rng f c= rng g &
ex N being Subset of NAT st rng f c= rng (g|N)
proof
assume f is_Subsequence_of g;
then consider N being Subset of NAT such that
A1: f c= Seq (g|N);
A2: rng (g|N) c= rng g by RELAT_1:70;
A3: now
rng (Seq (g|N)) = rng ((g|N) * Sgm (dom (g|N))) by FINSEQ_1:def 15;
then
A4: rng (Seq (g|N)) c= rng (g|N) by RELAT_1:26;
let a be object;
assume a in rng f;
then consider n being Nat such that
A5: n in dom f and
A6: f.n = a by FINSEQ_2:10;
[n,f.n] in f by A5,FUNCT_1:1;
then
A7: (Seq (g|N)).n = a by A1,A6,FUNCT_1:1;
dom f c= dom Seq (g|N) by A1,RELAT_1:11;
then a in rng (Seq (g|N)) by A5,A7,FUNCT_1:3;
hence a in rng (g|N) by A4;
end;
then rng f c= rng (g|N);
hence rng f c= rng g by A2;
take N;
thus thesis by A3;
end;
theorem Th2:
len f > 0 implies len Ant(f)+1 = len f & len Ant(f) < len f
proof
assume len f > 0;
then consider i being Nat such that
A1: len f = i+1 by NAT_1:6;
reconsider i as Element of NAT by ORDINAL1:def 12;
Ant(f) = f|(Seg i) by A1,Def1;
then dom Ant(f) = dom f /\ Seg i by RELAT_1:61;
then Seg (len Ant(f)) = dom f /\ Seg i by FINSEQ_1:def 3;
then
A2: Seg (len Ant(f)) = Seg (len f) /\ Seg i by FINSEQ_1:def 3;
i <= len f by A1,NAT_1:11;
then
A3: Seg i c= Seg (len f) by FINSEQ_1:5;
hence len Ant(f)+1 = len f by A1,A2,FINSEQ_1:6,XBOOLE_1:28;
len Ant(f) = i by A2,A3,FINSEQ_1:6,XBOOLE_1:28;
hence thesis by A1,NAT_1:13;
end;
theorem Th3:
len f > 0 implies f = Ant(f)^<*Suc(f)*> & rng f = rng Ant(f) \/ { Suc(f)}
proof
assume
A1: len f > 0;
then
A2: len f = len Ant(f)+1 by Th2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: now
let j be Nat such that
A5: j in dom f;
A6: 1 <= j by A3,A5,FINSEQ_1:1;
A7: now
assume j <= len Ant(f);
then
A8: j in dom Ant(f) by A6,FINSEQ_3:25;
Ant(f) = f|Seg len Ant(f) by A2,Def1;
then Ant(f) = f|dom Ant(f) by FINSEQ_1:def 3;
then f.j = (Ant(f)).j by A8,FUNCT_1:49;
hence f.j = (Ant(f)^<*Suc(f)*>).j by A8,FINSEQ_1:def 7;
end;
A9: now
1 in Seg 1 by FINSEQ_1:1;
then
A10: 1 in dom <*Suc(f)*> by FINSEQ_1:38;
assume
A11: j = len Ant(f)+1;
then j = len f by A1,Th2;
then f.j = Suc(f) by A1,Def2;
then f.j = <*Suc(f)*>.1;
hence f.j = (Ant(f)^<*Suc(f)*>).j by A11,A10,FINSEQ_1:def 7;
end;
j <= len Ant(f)+1 by A2,A3,A5,FINSEQ_1:1;
hence f.j = (Ant(f)^<*Suc(f)*>).j by A7,A9,NAT_1:8;
end;
len f = len Ant(f) + len <*Suc(f)*> by A2,FINSEQ_1:39;
then
A12: len f = len (Ant(f)^<*Suc(f)*>) by FINSEQ_1:22;
then f = (Ant(f)^<*Suc(f)*>) by A4,FINSEQ_2:9;
then rng f = rng Ant(f) \/ rng <*Suc(f)*> by FINSEQ_1:31;
hence thesis by A12,A4,FINSEQ_1:38,FINSEQ_2:9;
end;
theorem Th4:
len f > 1 implies len Ant(f) > 0
proof
assume len f > 1;
then len Ant(f)+1 > 1 by Th2;
hence thesis by NAT_1:13;
end;
theorem Th5:
Suc(f^<*p*>) = p & Ant(f^<*p*>) = f
proof
set fin = f^<*p*>;
A1: len fin = len f + 1 by FINSEQ_2:16;
then fin.(len fin) = p by FINSEQ_1:42;
hence Suc(f^<*p*>) = p by Def2;
thus Ant(f^<*p*>) = f
proof
set fin = f^<*p*>;
now
let a be object;
assume a in f;
then consider k being Nat such that
A2: k in dom f and
A3: a = [k,f.k] by FINSEQ_1:12;
k in dom fin & f.k = fin.k by A2,FINSEQ_1:def 7,FINSEQ_2:15;
hence a in fin by A3,FUNCT_1:1;
end;
then f c= fin;
then f = fin|(dom f) by GRFUNC_1:23;
then f = fin|(Seg len f) by FINSEQ_1:def 3;
hence thesis by A1,Def1;
end;
end;
reserve fin,fin1 for FinSequence;
theorem Th6:
len fin <= len (fin^fin1) & len fin1 <= len (fin^fin1) & (fin <>
{} implies 1 <= len fin & len fin1 < len (fin1^fin))
proof
len (fin^fin1) = len fin + len fin1 by FINSEQ_1:22;
hence len fin <= len (fin^fin1) & len fin1 <= len (fin^fin1) by NAT_1:12;
assume fin <> {};
then
A1: 0+1 <= len fin by NAT_1:13;
then len fin1 + 1 <= len fin + len fin1 by XREAL_1:6;
then len fin1 + 1 <= len (fin1^fin) by FINSEQ_1:22;
hence thesis by A1,NAT_1:13;
end;
theorem Th7:
Seq ((f^g)|dom f) = (f^g)|dom f
proof
(f^g)|dom f = f by FINSEQ_1:21;
hence thesis by FINSEQ_3:116;
end;
theorem Th8:
f is_Subsequence_of f^g
proof
set a = len f;
take N = Seg a;
reconsider f1 = (f^g)|N as FinSequence by FINSEQ_1:15;
A1: N = dom f by FINSEQ_1:def 3;
then f c= f1 by FINSEQ_1:21;
hence thesis by A1,Th7;
end;
theorem Th9:
1 < len (fin^<*b*>^<*c*>)
proof
len (fin^<*b*>^<*c*>) = len (fin^<*b*>) + len <*c*> by FINSEQ_1:22;
then len (fin^<*b*>^<*c*>) = len (fin^<*b*>) + 1 by FINSEQ_1:39;
then len (fin^<*b*>^<*c*>) = len fin + len <*b*> + 1 by FINSEQ_1:22;
then len (fin^<*b*>^<*c*>) = (len fin + 1) + 1 by FINSEQ_1:39;
then len (fin^<*b*>^<*c*>) = len fin + (1 + 1);
then 1 + 1 <= len (fin^<*b*>^<*c*>) by NAT_1:11;
hence thesis by NAT_1:13;
end;
theorem Th10:
1 <= len (fin^<*b*>) & len (fin^<*b*>) in dom (fin^<*b*>)
proof
len (fin^<*b*>) = len fin + 1 by FINSEQ_2:16;
then 1 <= len (fin^<*b*>) by NAT_1:11;
hence thesis by FINSEQ_3:25;
end;
theorem Th11:
0 < m implies len (Sgm (Seg n \/ {n+m})) = n+1
proof
A1: m <= n+m by NAT_1:11;
assume
A2: 0 < m;
then card (Seg n \/ {n+m}) = card (Seg n) + 1 by CARD_2:41,FINSEQ_3:10;
then
A3: card (Seg n \/ {n+m}) = n + 1 by FINSEQ_1:57;
0+1 <= m by A2,NAT_1:13;
then 1 <= m+n by A1,XXREAL_0:2;
then n+m in Seg (n+m) by FINSEQ_1:1;
then {n+m} c= Seg (n+m) by ZFMISC_1:31;
then {n+m} is included_in_Seg by FINSEQ_1:def 13;
hence thesis by A3,FINSEQ_3:39;
end;
theorem Th12:
0 < m implies dom (Sgm (Seg n \/ {n+m})) = Seg (n+1)
proof
assume 0 < m;
then len (Sgm (Seg n \/ {n+m})) = n+1 by Th11;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th13:
0 < len f implies f is_Subsequence_of Ant(f)^g^<*Suc(f)*>
proof
set n = len Ant(f);
set m = len g;
set N = Seg n \/ {n+(m+1)};
set f1 = Ant(f)^g^<*Suc(f)*>;
reconsider f2 = f1|N as FinSubsequence;
assume
A1: 0 < len f;
take N;
now
now
let b be object such that
A2: b in N;
reconsider i = b as Element of NAT by A2;
A3: now
assume i in {n+(m+1)};
then
A4: i = (n+m)+1 by TARSKI:def 1;
then
A5: 1 <= i by NAT_1:11;
len f1 = len (Ant(f)^g) + len <*Suc(f)*> by FINSEQ_1:22;
then len f1 = n + m + len <*Suc(f)*> by FINSEQ_1:22;
then i <= len f1 by A4,FINSEQ_1:39;
hence i in dom f1 by A5,FINSEQ_3:25;
end;
now
f1 = Ant(f)^(g^<*Suc(f)*>) by FINSEQ_1:32;
then
A6: n <= len f1 by Th6;
assume
A7: i in Seg n;
then
A8: 1 <= i by FINSEQ_1:1;
i <= n by A7,FINSEQ_1:1;
then i <= len f1 by A6,XXREAL_0:2;
hence i in dom f1 by A8,FINSEQ_3:25;
end;
hence b in dom f1 by A2,A3,XBOOLE_0:def 3;
end;
then
A9: N c= dom f1;
dom f2 = dom f1 /\ N by RELAT_1:61;
then
A10: dom f2 = N by A9,XBOOLE_1:28;
then
A11: dom Sgm (dom f2) = Seg (n+1) by Th12;
now
let i;
i in dom f iff 1 <= i & i <= len f by FINSEQ_3:25;
then i in dom f iff 1 <= i & i <= n+1 by A1,Th2;
hence i in dom f iff i in Seg (n+1) by FINSEQ_1:1;
end;
then for b being object holds b in dom f iff b in Seg (n+1);
then
A12: dom Sgm (dom f2) = dom f by A11,TARSKI:2;
A13: now
let i,j such that
A14: i in Seg n and
A15: j in {n+(m+1)};
A16: i <= n by A14,FINSEQ_1:1;
n+1 <= n+1+m by NAT_1:11;
then n < n+(m+1) by NAT_1:13;
then n < j by A15,TARSKI:def 1;
hence i < j by A16,XXREAL_0:2;
end;
let b be object such that
A17: b in f;
consider c,d being object such that
A18: b = [c,d] by A17,RELAT_1:def 1;
A19: c in dom f by A17,A18,FUNCT_1:1;
then reconsider i = c as Element of NAT;
Sgm (dom f2) = Sgm(Seg n)^Sgm{n+(m+1)} by A10,A13,FINSEQ_3:42;
then Sgm (dom f2) = Sgm(Seg n)^<*n+(m+1)*> by FINSEQ_3:44;
then
A20: Sgm (dom f2) = (idseq n)^<*n+(m+1)*> by FINSEQ_3:48;
A21: now
assume
A22: i in Seg n;
then
A23: i in dom Ant(f) by FINSEQ_1:def 3;
i in dom idseq n by A22;
then Sgm (dom f2).i = (idseq n).i by A20,FINSEQ_1:def 7;
then
A24: Sgm (dom f2).i = i by A22,FUNCT_1:18;
i in dom Sgm (dom f2) & Seq f2 = f2 * Sgm (dom f2) by A17,A18,A12,
FINSEQ_1:def 15,FUNCT_1:1;
then Seq f2.i = f2.i by A24,FUNCT_1:13;
then Seq f2.i = (f2|Seg n).i by A22,FUNCT_1:49;
then
A25: Seq f2.i = (f1|Seg n).i by RELAT_1:74,XBOOLE_1:7;
f1 = Ant(f)^(g^<*Suc(f)*>) & Seg len Ant f = dom Ant f by FINSEQ_1:32
,def 3;
then
A26: Seq f2.i = (Ant(f)).i by A25,FINSEQ_1:21;
f = Ant(f)^<*Suc(f)*> by A1,Th3;
hence Seq f2.i = f.i by A26,A23,FINSEQ_1:def 7;
end;
rng Sgm (dom (f1|N)) = dom (f1|N) by FINSEQ_1:50;
then dom f = dom ((f1|N) * Sgm (dom (f1|N))) by A12,RELAT_1:27;
then
A27: dom f = dom Seq f2 by FINSEQ_1:def 15;
A28: now
1 in Seg 1 by FINSEQ_1:1;
then
A29: len (Ant(f)^g) = n + m & 1 in dom <*Suc(f)*> by FINSEQ_1:22,38;
A30: i in dom Sgm (dom f2) & Seq f2 = f2 * Sgm (dom f2) by A17,A18,A12,
FINSEQ_1:def 15,FUNCT_1:1;
assume
A31: i = n+1;
len idseq n = n by CARD_1:def 7;
then Sgm (dom f2).i = n+(m+1) by A20,A31,FINSEQ_1:42;
then
A32: Seq f2.i = f2.(n+(m+1)) by A30,FUNCT_1:13;
n+(m+1) in {n+(m+1)} & {n+(m+1)} c= N by TARSKI:def 1,XBOOLE_1:7;
then Seq f2.i = f1.((n+m)+1) by A32,FUNCT_1:49;
then
A33: Seq f2.i = <*Suc(f)*>.1 by A29,FINSEQ_1:def 7;
f.i = f.(len f) by A1,A31,Th2;
then f.i = Suc(f) by A1,Def2;
hence Seq f2.i = f.i by A33;
end;
d = f.c by A17,A18,FUNCT_1:1;
hence b in Seq f2 by A18,A19,A11,A12,A21,A28,A27,FINSEQ_2:7,FUNCT_1:1;
end;
hence thesis;
end;
theorem Th14:
1 in dom <*c,d*> & 2 in dom <*c,d*> &
(f^<*c,d*>).(len f + 1) = c & (f^<*c,d*>).(len f + 2) = d
proof
A1: 2 <= len <*c,d*> by FINSEQ_1:44;
then 2 in dom <*c,d*> by FINSEQ_3:25;
then
A2: (f^<*c,d*>).(len f+2) = <*c,d*>.2 by FINSEQ_1:def 7;
1 <= 2;
then
A3: 1 <= len <*c,d*> by FINSEQ_1:44;
then 1 in dom <*c,d*> by FINSEQ_3:25;
then (f^<*c,d*>).(len f+1) = <*c,d*>.1 by FINSEQ_1:def 7;
hence thesis by A3,A1,A2,FINSEQ_3:25;
end;
begin :: A Sequent calculus
definition
let Al,f;
func still_not-bound_in f -> Subset of bound_QC-variables(Al) means
:Def5:
a in it iff ex i,p st i in dom f & p = f.i & a in still_not-bound_in p;
existence
proof
defpred P[object] means ex i,p st i in dom f & p = f.i & $1 in
still_not-bound_in p;
consider X being set such that
A1: for a being object holds a in X
iff a in bound_QC-variables(Al) & P[a] from
XBOOLE_0:sch 1;
take X;
for a being object st a in X holds a in bound_QC-variables(Al) by A1;
hence X is Subset of bound_QC-variables(Al) by TARSKI:def 3;
thus thesis by A1;
end;
uniqueness
proof
let X,Y be Subset of bound_QC-variables(Al);
assume that
A2: for a holds a in X iff ex i,p st i in dom f & p = f.i & a in
still_not-bound_in p and
A3: for a holds a in Y iff ex i,p st i in dom f & p = f.i & a in
still_not-bound_in p;
now
let a be object;
a in X iff ex i,p st i in dom f & p = f.i & a in still_not-bound_in
p by A2;
hence a in X iff a in Y by A3;
end;
hence thesis by TARSKI:2;
end;
end;
definition
let Al;
func set_of_CQC-WFF-seq(Al) -> set means
:Def6:
a in it iff a is FinSequence of CQC-WFF(Al);
existence
proof
defpred P[object] means $1 is FinSequence of CQC-WFF(Al);
consider X being set such that
A1: for a being object holds a in X iff a in bool [:NAT,CQC-WFF(Al):] & P[a]
from
XBOOLE_0:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
let X,Y be set such that
A2: a in X iff a is FinSequence of CQC-WFF(Al) and
A3: a in Y iff a is FinSequence of CQC-WFF(Al);
now
let a be object;
a in X iff a is FinSequence of CQC-WFF(Al) by A2;
hence a in X iff a in Y by A3;
end;
hence thesis by TARSKI:2;
end;
end;
reserve PR,PR1 for FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
definition
let Al,PR;
let n be Nat;
pred PR,n is_a_correct_step means
:Def7:
ex f st Suc(f) is_tail_of Ant(f) &
(PR.n)`1 = f if (PR.n)`2 = 0, ex f st (PR.n)`1 = f^<*VERUM(Al)*>
if (PR.n)`2 = 1,
ex i,f,g st 1 <= i & i < n & Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g)
& (PR.i)`1 = f & (PR.n)`1 = g if (PR.n)`2 = 2, ex i,j,f,g st 1 <= i & i < n & 1
<= j & j < i & len f > 1 & len g > 1 & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc(
Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(Ant
(f))^<*Suc(f)*> = (PR.n)`1 if (PR.n)`2 = 3, ex i,j,f,g,p st 1 <= i & i < n & 1
<= j & j < i & len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc(
f) = Suc(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(Ant(f))^<*p*> = (PR.n)`1 if (PR
.n)`2 = 4, ex i,j,f,g st 1 <= i & i < n & 1 <= j & j < i & Ant(f) = Ant(g) & f
= (PR.j)`1 & g = (PR.i)`1 & Ant(f)^<*(Suc(f)) '&' (Suc(g))*> = (PR.n)`1 if (PR.
n)`2 = 5, ex i,f,p,q st 1 <= i & i < n & p '&' q = Suc(f) & f = (PR.i)`1 & Ant(
f)^<*p*> = (PR.n)`1 if (PR.n)`2 = 6, ex i,f,p,q st 1 <= i & i < n & p '&' q =
Suc(f) & f = (PR.i)`1 & Ant(f)^<*q*>= (PR.n)`1 if (PR.n)`2 = 7, ex i,f,p,x,y st
1 <= i & i < n & Suc(f) = All(x,p) & f = (PR.i)`1 & Ant(f)^<*p.(x,y)*> = (PR.n)
`1 if (PR.n)`2 = 8, ex i,f,p,x,y st 1 <= i & i < n & Suc(f) = p.(x,y) & not y
in still_not-bound_in (Ant(f)) & not y in still_not-bound_in All(x,p) & f = (PR
.i)`1 & Ant(f)^<*All(x,p)*> = (PR.n)`1 if (PR.n)`2 = 9;
consistency;
end;
definition
let Al,PR;
attr PR is a_proof means
PR <> {} & for n being Nat st 1 <= n & n <=
len PR holds PR,n is_a_correct_step;
end;
definition
let Al,f;
pred |- f means
ex PR st PR is a_proof & f = (PR.(len PR))`1;
end;
definition
let Al,p,X;
pred p is_formal_provable_from X means
ex f st rng Ant(f) c= X & Suc (f) = p & |- f;
end;
definition
let Al,X,A,J,v;
pred J,v |= X means
p in X implies J,v |= p;
end;
definition
let Al,X,p;
pred X |= p means
J,v |= X implies J,v |= p;
end;
definition
let Al,p;
pred |= p means
{}(CQC-WFF(Al)) |= p;
end;
definition
let Al,f, A, J, v;
pred J,v |= f means
J,v |= rng(f);
end;
definition
let Al, f, p;
pred f |= p means
J,v |= f implies J,v |= p;
end;
theorem Th15:
Suc(f) is_tail_of Ant(f) implies Ant(f) |= Suc(f)
proof
assume Suc(f) is_tail_of Ant(f);
then ex i st i in dom Ant(f) & (Ant(f)).i = Suc(f) by Lm1;
then
A1: Suc(f) in rng(Ant(f)) by FUNCT_1:3;
let A,J,v;
assume J,v |= rng(Ant(f));
hence thesis by A1;
end;
theorem Th16:
Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & Ant(f) |=
Suc(f) implies Ant(g) |= Suc(g)
proof
assume that
A1: Ant(f) is_Subsequence_of Ant(g) and
A2: Suc(f) = Suc(g) & Ant(f) |= Suc(f);
let A,J,v such that
A3: J,v |= rng(Ant(g));
now
let p;
assume
A4: p in rng(Ant(f));
rng(Ant(f)) c= rng(Ant(g)) by A1,Th1;
hence J,v |= p by A3,A4;
end;
then J,v |= rng(Ant(f));
then J,v |= Ant(f);
hence thesis by A2;
end;
theorem Th17:
len f > 0 implies (J,v |= Ant(f) & J,v |= Suc(f) iff J,v |= f)
proof
assume
A1: len f > 0;
thus J,v |= Ant(f) & J,v |= Suc(f) implies J,v |= f
proof
assume that
A2: J,v |= Ant(f) and
A3: J,v |= Suc(f);
let p;
assume p in rng(f);
then p in rng(Ant(f)) \/ {Suc(f)} by A1,Th3;
then
A4: p in rng(Ant(f)) or p in {Suc(f)} by XBOOLE_0:def 3;
J,v |= rng(Ant(f)) by A2;
hence thesis by A3,A4,TARSKI:def 1;
end;
thus J,v |= f implies J,v |= Ant(f) & J,v |= Suc(f)
proof
assume
A5: J,v |= rng(f);
thus J,v |= rng(Ant(f))
proof
A6: rng(Ant(f)) c= rng(Ant(f)) \/ {Suc(f)} by XBOOLE_1:7;
let p;
assume p in rng(Ant(f));
then p in rng(Ant(f)) \/ {Suc(f)} by A6;
then p in rng(f) by A1,Th3;
hence thesis by A5;
end;
0+1 <= len f by A1,NAT_1:13;
then
A7: len f in dom f by FINSEQ_3:25;
Suc(f) = f.(len f) by A1,Def2;
then Suc(f) in rng(f) by A7,FUNCT_1:3;
hence J,v |= Suc(f) by A5;
end;
end;
theorem Th18:
len f > 1 & len g > 1 & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc(
Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g)
implies Ant(Ant(f)) |= Suc(f)
proof
assume that
A1: len f > 1 and
A2: len g > 1 and
A3: Ant(Ant(f)) = Ant(Ant(g)) and
A4: 'not' Suc(Ant(f)) = Suc(Ant(g)) and
A5: Suc(f) = Suc(g) and
A6: Ant(f) |= Suc(f) and
A7: Ant(g) |= Suc(g);
let A,J,v such that
A8: J,v |= Ant(Ant(f));
A9: len Ant(g) > 0 by A2,Th4;
A10: now
assume not J,v |= Suc(Ant(f));
then J,v |= Suc(Ant(g)) by A4,VALUAT_1:17;
then J,v |= Ant(g) by A3,A9,A8,Th17;
hence thesis by A5,A7;
end;
A11: len Ant(f) > 0 by A1,Th4;
now
assume J,v |= Suc(Ant(f));
then J,v |= Ant(f) by A11,A8,Th17;
hence thesis by A6;
end;
hence thesis by A10;
end;
theorem Th19:
len f > 1 & Ant(f) = Ant(g) & 'not' p = Suc(Ant(f)) & 'not' Suc(
f) = Suc(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g) implies Ant(Ant(f)) |= p
proof
assume that
A1: len f > 1 and
A2: Ant(f) = Ant(g) and
A3: 'not' p = Suc(Ant(f)) and
A4: 'not' Suc(f) = Suc(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g);
A5: len Ant(f) > 0 by A1,Th4;
A6: now
given A,J,v such that
A7: J,v |= Ant(f);
J,v |= Suc(f) & J,v |= 'not' Suc(f) by A2,A4,A7;
hence contradiction by VALUAT_1:17;
end;
let A,J,v such that
A8: J,v |= Ant(Ant(f));
now
assume J,v |= Suc(Ant(f));
then J,v |= Ant(f) by A5,A8,Th17;
hence contradiction by A6;
end;
hence thesis by A3,VALUAT_1:17;
end;
theorem Th20:
Ant(f) = Ant(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g) implies
Ant(f) |= (Suc(f)) '&' (Suc(g))
proof
assume
A1: Ant(f) = Ant(g) & Ant(f) |= Suc(f) & Ant(g) |= Suc(g);
let A,J,v;
assume J,v |= Ant(f);
then J,v |= Suc(f) & J,v |= Suc(g) by A1;
hence thesis by VALUAT_1:18;
end;
theorem Th21:
Ant(f) |= p '&' q implies Ant(f) |= p
proof
assume
A1: Ant(f) |= p '&' q;
let A,J,v;
assume J,v |= Ant(f);
then J,v |= p '&' q by A1;
hence thesis by VALUAT_1:18;
end;
theorem Th22:
Ant(f) |= p '&' q implies Ant(f) |= q
proof
assume
A1: Ant(f) |= p '&' q;
let A,J,v;
assume J,v |= Ant(f);
then J,v |= p '&' q by A1;
hence thesis by VALUAT_1:18;
end;
theorem Th23:
J,v |= [p,Sub] iff J,v |= p
proof
J,v |= [p,Sub] iff J,v |= [p,Sub]`1 by SUBLEMMA:def 2;
hence thesis;
end;
reserve a for Element of A;
theorem Th24:
J,v |= p.(x,y) iff ex a st v.y = a & J,v.(x|a) |= p
proof
A1: J,v |= CQC_Sub([p,Sbst(x,y)]) iff J,v.Val_S(v,[p,Sbst(x,y)]) |= [p,Sbst(
x,y)] by SUBLEMMA:89;
A2: J,v.Val_S(v,[p,Sbst(x,y)]) |= [p,Sbst(x,y)] iff J,v.Val_S(v,[p,Sbst(x,y)
]) |= p by Th23;
Val_S(v,[p,Sbst(x,y)]) = v*(@[p,Sbst(x,y)]`2) by SUBLEMMA:def 1;
then Val_S(v,[p,Sbst(x,y)]) = v*@Sbst(x,y);
then
A3: Val_S(v,[p,Sbst(x,y)]) = v*(x .--> y) by SUBSTUT1:def 2;
y in bound_QC-variables(Al);
then y in dom v by SUBLEMMA:58;
then Val_S(v,[p,Sbst(x,y)]) = x .--> v.y by A3,FUNCOP_1:17;
hence thesis by A1,A2,SUBSTUT2:def 1;
end;
theorem Th25:
Suc(f) = All(x,p) & Ant(f) |= Suc(f) implies for y holds Ant(f) |= p.(x,y)
proof
assume
A1: Suc(f) = All(x,p) & Ant(f) |= Suc(f);
let y,A,J,v;
assume J,v |= Ant(f);
then
A2: J,v |= All(x,p) by A1;
ex a st v.y = a & J,v.(x|a) |= p
proof
take v.y;
thus thesis by A2,SUBLEMMA:50;
end;
hence thesis by Th24;
end;
theorem Th26:
for X being set st X c= bound_QC-variables(Al) holds not x in X
implies v.(x|a)|X = v|X
proof
let X be set such that
A1: X c= bound_QC-variables(Al) and
A2: not x in X;
set f2 = v|X;
set f1 = v.(x|a)|X;
A3: dom f1 = dom f2 by A1,SUBLEMMA:63;
now
let b be object such that
A4: b in dom f1;
x <> b by A2,A4;
then
A5: v.(x|a).b = v.b by SUBLEMMA:48;
v.(x|a).b = f1.b by A4,FUNCT_1:47;
hence f1.b = f2.b by A3,A4,A5,FUNCT_1:47;
end;
hence thesis by A3,FUNCT_1:2;
end;
theorem Th27:
for v,w holds v|still_not-bound_in f = w|still_not-bound_in f
implies (J,v |= f implies J,w |= f)
proof
let v,w such that
A1: v|still_not-bound_in f = w|still_not-bound_in f;
assume J,v |= f;
then
A2: J,v |= rng(f);
let p such that
A3: p in rng(f);
ex i being Nat st i in dom f & p = f.i by A3,FINSEQ_2:10;
then
for b being object st b in still_not-bound_in p
holds b in still_not-bound_in f by Def5;
then still_not-bound_in p c= still_not-bound_in f;
then
A4: v|still_not-bound_in p = w|still_not-bound_in p by A1,RELAT_1:153;
J,v |= p by A2,A3;
hence thesis by A4,SUBLEMMA:68;
end;
theorem Th28:
not y in still_not-bound_in All(x,p) implies v.(y|a).(x|a)|
still_not-bound_in p = v.(x|a)|still_not-bound_in p
proof
A1: v.(y|a).(x|a) = v+*((y|a)+*(x|a)) by FUNCT_4:14;
assume
A2: not y in still_not-bound_in All(x,p);
now
assume
A3: x <> y;
dom (x|a) = {x} & dom (y|a) = {y};
then v.(y|a).(x|a) = v+*((x|a)+*(y|a)) by A1,A3,FUNCT_4:35,ZFMISC_1:11;
then
A4: v.(y|a).(x|a) = v+*(x|a)+*(y|a) by FUNCT_4:14;
not y in (still_not-bound_in p) \ {x} by A2,QC_LANG3:12;
then not y in still_not-bound_in p by A3,ZFMISC_1:56;
hence thesis by A4,Th26;
end;
hence thesis by A1;
end;
theorem Th29:
Suc(f) = p.(x,y) & Ant(f) |= Suc(f) & not y in
still_not-bound_in Ant(f) & not y in still_not-bound_in All(x,p) implies Ant(f)
|= All(x,p)
proof
assume that
A1: Suc(f) = p.(x,y) & Ant(f) |= Suc(f) and
A2: not y in still_not-bound_in (Ant(f)) and
A3: not y in still_not-bound_in All(x,p);
let A,J,v such that
A4: J,v |= Ant(f);
for a holds J,v.(x|a) |= p
proof
let a;
v.(y|a)|still_not-bound_in (Ant(f)) = v|still_not-bound_in (Ant(f)) by A2
,Th26;
then J,v.(y|a) |= Ant(f) by A4,Th27;
then J,v.(y|a) |= p.(x,y) by A1;
then
ex a1 being Element of A st v.(y|a).y = a1 & J,v.(y|a).(x |a1) |= p by Th24
;
then
A5: J,v.(y|a).(x|a) |= p by SUBLEMMA:49;
v.(y|a).(x|a)|still_not-bound_in p = v.(x|a)|still_not-bound_in p by A3
,Th28;
hence thesis by A5,SUBLEMMA:68;
end;
hence thesis by SUBLEMMA:50;
end;
theorem Th30:
Ant(f^<*VERUM(Al)*>) |= Suc(f^<*VERUM(Al)*>)
proof
let A,J,v such that
J,v |= Ant(f^<*VERUM(Al)*>);
Suc(f^<*VERUM(Al)*>) = VERUM(Al) by Th5;
hence thesis by VALUAT_1:32;
end;
theorem Th31:
for n being Nat holds 1 <= n & n <= len PR implies
(PR.n)`2 = 0 or ... or (PR.n)`2 = 9
proof
let n be Nat;
assume 1 <= n & n <= len PR;
then n in dom PR by FINSEQ_3:25;
then PR.n in rng PR by FUNCT_1:def 3;
then (PR.n)`2 in {k where k is Nat: k <= 9} by CQC_THE1:def 3,MCART_1:10;
then ex k being Nat st k = (PR.n)`2 & k <= 9;
hence thesis;
end;
Lm3: 1 <= n & n <= len PR implies (PR.n)`1 is FinSequence of CQC-WFF(Al)
proof
assume 1 <= n & n <= len PR;
then n in dom PR by FINSEQ_3:25;
then PR.n in rng PR by FUNCT_1:def 3;
then (PR.n)`1 in set_of_CQC-WFF-seq(Al) by MCART_1:10;
hence thesis by Def6;
end;
:: Theorem on the Correctness (Ebb et al, Chapter IV, Theorem 6.2)
theorem
p is_formal_provable_from X implies X |= p
proof
assume p is_formal_provable_from X;
then consider f such that
A1: rng Ant(f) c= X and
A2: Suc(f) = p and
A3: |- f;
consider PR such that
A4: PR is a_proof and
A5: f = (PR.(len PR))`1 by A3;
PR <> {} by A4;
then
A6: 1 <= len PR by FINSEQ_1:20;
defpred P[Nat] means $1 <= len PR implies for m st 1 <= m & m <=
$1 holds ex g st g = (PR.m)`1 & Ant(g) |= Suc(g);
A7: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat such that
A8: P[k];
assume
A9: k+1 <= len PR;
A10: k <= k+1 by NAT_1:11;
let m such that
A11: 1 <= m and
A12: m <= k+1;
A13: m <= len PR by A9,A12,XXREAL_0:2;
A14: now
assume
A15: m = k+1;
take g = (PR.m)`1;
thus g = (PR.m)`1;
reconsider g = (PR.m)`1 as FinSequence of CQC-WFF(Al) by A11,A13,Lm3;
A16: PR,m is_a_correct_step by A4,A11,A13;
now
(PR.m)`2 = 0 or ... or (PR.m)`2 = 9 by A11,A13,Th31;
then per cases;
suppose
(PR.m)`2 = 0;
then ex f st Suc(f) is_tail_of Ant(f) & (PR.m)`1 = f by A16,Def7;
hence Ant(g) |= Suc(g) by Th15;
end;
suppose
(PR.m)`2 = 1;
then ex f st g = f^<*VERUM(Al)*> by A16,Def7;
hence Ant(g) |= Suc(g) by Th30;
end;
suppose
(PR.m)`2 = 2;
then consider i,f,f1 such that
A17: 1 <= i and
A18: i < m and
A19: Ant(f) is_Subsequence_of Ant(f1) & Suc(f) = Suc(f1) & (PR.i
)`1 = f & (PR.m)`1 = f1 by A16,Def7;
i <= k by A15,A18,NAT_1:13;
then ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A17,
XXREAL_0:2;
hence Ant(g) |= Suc(g) by A19,Th16;
end;
suppose
(PR.m)`2 = 3;
then consider i,j,f,f1 such that
A20: 1 <= i and
A21: i < m and
A22: 1 <= j and
A23: j < i and
A24: len f > 1 & len f1 > 1 & Ant(Ant(f)) = Ant(Ant(f1)) & 'not'
Suc(Ant(f )) = Suc(Ant(f1)) & Suc(f) = Suc(f1) & f = (PR.j)`1 & f1 = (PR.i)`1
and
A25: Ant(Ant(f))^<*Suc(f)*> = (PR.m)`1 by A16,Def7;
A26: Ant(g) = Ant(Ant(f)) & Suc(g) = Suc(f) by A25,Th5;
A27: i <= k by A15,A21,NAT_1:13;
then j <= k by A23,XXREAL_0:2;
then
A28: ex h1 st h1 = (PR.j)`1 & Ant(h1) |= Suc(h1) by A8,A9,A10,A22,
XXREAL_0:2;
ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A20,A27,
XXREAL_0:2;
hence Ant(g) |= Suc(g) by A24,A28,A26,Th18;
end;
suppose
(PR.m)`2 = 4;
then consider i,j,f,f1,p such that
A29: 1 <= i and
A30: i < m and
A31: 1 <= j and
A32: j < i and
A33: len f > 1 & Ant(f) = Ant(f1) & Suc(Ant(f)) = 'not' p &
'not' Suc(f) = Suc (f1) & f = (PR.j)`1 & f1 = (PR.i)`1 and
A34: Ant(Ant(f))^<*p*> = (PR.m)`1 by A16,Def7;
A35: Ant(g) = Ant(Ant(f)) & Suc(g) = p by A34,Th5;
A36: i <= k by A15,A30,NAT_1:13;
then j <= k by A32,XXREAL_0:2;
then
A37: ex h1 st h1 = (PR.j)`1 & Ant(h1) |= Suc(h1) by A8,A9,A10,A31,
XXREAL_0:2;
ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A29,A36,
XXREAL_0:2;
hence Ant(g) |= Suc(g) by A33,A37,A35,Th19;
end;
suppose
(PR.m)`2 = 5;
then consider i,j,f,f1 such that
A38: 1 <= i and
A39: i < m and
A40: 1 <= j and
A41: j < i and
A42: Ant(f) = Ant(f1) & f = (PR.j)`1 & f1 = (PR.i)`1 and
A43: Ant(f)^<*(Suc(f)) '&' (Suc(f1))*> = (PR.m)`1 by A16,Def7;
A44: Ant(g) = Ant(f) & Suc(g) = (Suc(f)) '&' (Suc(f1)) by A43,Th5;
A45: i <= k by A15,A39,NAT_1:13;
then j <= k by A41,XXREAL_0:2;
then
A46: ex h1 st h1 = (PR.j)`1 & Ant(h1) |= Suc(h1) by A8,A9,A10,A40,
XXREAL_0:2;
ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A38,A45,
XXREAL_0:2;
hence Ant(g) |= Suc(g) by A42,A46,A44,Th20;
end;
suppose
(PR.m)`2 = 6;
then consider i,f,p,q such that
A47: 1 <= i and
A48: i < m and
A49: p '&' q = Suc(f) & f = (PR.i)`1 and
A50: Ant(f)^<*p*> = (PR.m)`1 by A16,Def7;
i <= k by A15,A48,NAT_1:13;
then
A51: ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A47,XXREAL_0:2;
Ant(g) = Ant(f) & Suc(g) = p by A50,Th5;
hence Ant(g) |= Suc(g) by A49,A51,Th21;
end;
suppose
(PR.m)`2 = 7;
then consider i,f,p,q such that
A52: 1 <= i and
A53: i < m and
A54: p '&' q = Suc(f) & f = (PR.i)`1 and
A55: Ant(f)^<*q*>= (PR.m)`1 by A16,Def7;
i <= k by A15,A53,NAT_1:13;
then
A56: ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A52,XXREAL_0:2;
Ant(g) = Ant(f) & Suc(g) = q by A55,Th5;
hence Ant(g) |= Suc(g) by A54,A56,Th22;
end;
suppose
(PR.m)`2 = 8;
then consider i,f,p,x,y such that
A57: 1 <= i and
A58: i < m and
A59: Suc(f) = All(x,p) & f = (PR.i)`1 and
A60: Ant(f)^<*p.(x,y)*> = (PR.m)`1 by A16,Def7;
i <= k by A15,A58,NAT_1:13;
then
A61: ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A57,XXREAL_0:2;
Ant(g) = Ant(f) & Suc(g) = p.(x,y) by A60,Th5;
hence Ant(g) |= Suc(g) by A59,A61,Th25;
end;
suppose
(PR.m)`2 = 9;
then consider i,f,p,x,y such that
A62: 1 <= i and
A63: i < m and
A64: Suc(f) = p.(x,y) & not y in still_not-bound_in (Ant(f)) &
( not y in still_not-bound_in All(x,p))& f = (PR.i)`1 and
A65: Ant(f)^<*All(x,p)*> = (PR.m)`1 by A16,Def7;
i <= k by A15,A63,NAT_1:13;
then
A66: ex h st h = (PR.i)`1 & Ant(h) |= Suc(h) by A8,A9,A10,A62,XXREAL_0:2;
Ant(g) = Ant(f) & Suc(g) = All(x,p) by A65,Th5;
hence Ant(g) |= Suc(g) by A64,A66,Th29;
end;
end;
hence thesis;
end;
m <= k implies ex g st g = (PR.m)`1 & Ant(g) |= Suc(g) by A8,A9,A11,A10,
XXREAL_0:2;
hence thesis by A12,A14,NAT_1:8;
end;
A67: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A67,A7);
then consider g such that
A68: g = (PR.(len PR))`1 and
A69: Ant(g) |= Suc(g) by A6;
let A,J,v;
assume J,v |= X;
then for p st p in rng(Ant(f)) holds J,v |= p by A1;
then J,v |= rng(Ant(f));
then J,v |= Ant(g) by A5,A68;
hence thesis by A2,A5,A68,A69;
end;
begin :: Derived Rules
theorem Th33:
Suc(f) is_tail_of Ant(f) implies |- f
proof
set PR = <*[f,0]*>;
A1: rng PR = {[f,0]} by FINSEQ_1:38;
now
let a be object;
assume a in rng PR;
then
A2: a = [f,0] by A1,TARSKI:def 1;
f in set_of_CQC-WFF-seq(Al) by Def6;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A2,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng PR c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider
PR as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds :] by
FINSEQ_1:def 4;
assume
A3: Suc(f) is_tail_of Ant(f);
now
let n be Nat such that
A4: 1 <= n and
A5: n <= len PR;
n <= 1 by A5,FINSEQ_1:39;
then n = 1 by A4,XXREAL_0:1;
then PR.n = [f,0];
then (PR.n)`1 = f & (PR.n)`2 = 0;
hence PR,n is_a_correct_step by A3,Def7;
end;
then
A6: PR is a_proof;
PR.1 = [f,0];
then PR.(len PR) = [f,0] by FINSEQ_1:40;
then (PR.(len PR))`1 = f;
hence thesis by A6;
end;
theorem Th34:
for n being Nat holds 1 <= n & n <= len PR implies (PR,n
is_a_correct_step iff PR^PR1,n is_a_correct_step)
proof
let n be Nat;
assume that
A1: 1 <= n and
A2: n <= len PR;
n in dom PR by A1,A2,FINSEQ_3:25;
then
A3: (PR^PR1).n = PR.n by FINSEQ_1:def 7;
len(PR^PR1) = len PR + len PR1 by FINSEQ_1:22;
then len PR <= len(PR^PR1) by NAT_1:11;
then
A4: n <= len(PR^PR1) by A2,XXREAL_0:2;
thus PR,n is_a_correct_step implies PR^PR1,n is_a_correct_step
proof
assume
A5: PR,n is_a_correct_step;
((PR^PR1).n)`2 = 0 or ... or ((PR^PR1).n)`2 = 9 by A1,A4,Th31;
then per cases;
case
((PR^PR1).n)`2 = 0;
hence thesis by A3,A5,Def7;
end;
case
((PR^PR1).n)`2 = 1;
hence thesis by A3,A5,Def7;
end;
case
((PR^PR1).n)`2 = 2;
then consider i,f,g such that
A6: 1 <= i and
A7: i < n and
A8: Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & (PR.i)`1 =
f & ( PR.n)`1 = g by A3,A5,Def7;
i <= len PR by A2,A7,XXREAL_0:2;
then i in dom PR by A6,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A6,A7,A8;
end;
case
((PR^PR1).n)`2 = 3;
then consider i,j,f,g such that
A9: 1 <= i and
A10: i < n and
A11: 1 <= j and
A12: j < i and
A13: len f > 1 & len g > 1 & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc(
Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(Ant
(f) )^<*Suc(f) *> = (PR.n)`1 by A3,A5,Def7;
A14: i <= len PR by A2,A10,XXREAL_0:2;
then i in Seg(len PR) by A9,FINSEQ_1:1;
then i in dom PR by FINSEQ_1:def 3;
then
A15: PR.i = (PR^PR1).i by FINSEQ_1:def 7;
j <= len PR by A12,A14,XXREAL_0:2;
then j in dom PR by A11,FINSEQ_3:25;
then PR.j = (PR^PR1).j by FINSEQ_1:def 7;
hence thesis by A3,A9,A10,A11,A12,A13,A15;
end;
case
((PR^PR1).n)`2 = 4;
then consider i,j,f,g,p such that
A16: 1 <= i and
A17: i < n and
A18: 1 <= j and
A19: j < i and
A20: len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc
(f) = Suc( g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(Ant(f))^<*p*> = (PR.n)`1 by
A3,A5,Def7;
A21: i <= len PR by A2,A17,XXREAL_0:2;
then i in Seg(len PR) by A16,FINSEQ_1:1;
then i in dom PR by FINSEQ_1:def 3;
then
A22: PR.i = (PR^PR1).i by FINSEQ_1:def 7;
j <= len PR by A19,A21,XXREAL_0:2;
then j in dom PR by A18,FINSEQ_3:25;
then PR.j = (PR^PR1).j by FINSEQ_1:def 7;
hence thesis by A3,A16,A17,A18,A19,A20,A22;
end;
case
((PR^PR1).n)`2 = 5;
then consider i,j,f,g such that
A23: 1 <= i and
A24: i < n and
A25: 1 <= j and
A26: j < i and
A27: Ant(f) = Ant(g) & f = (PR.j)`1 & g = (PR.i)`1 & Ant(f)^<*(Suc(f
)) '&' (Suc(g))*> = (PR.n)`1 by A3,A5,Def7;
A28: i <= len PR by A2,A24,XXREAL_0:2;
then i in Seg(len PR) by A23,FINSEQ_1:1;
then i in dom PR by FINSEQ_1:def 3;
then
A29: PR.i = (PR^PR1).i by FINSEQ_1:def 7;
j <= len PR by A26,A28,XXREAL_0:2;
then j in dom PR by A25,FINSEQ_3:25;
then PR.j = (PR^PR1).j by FINSEQ_1:def 7;
hence thesis by A3,A23,A24,A25,A26,A27,A29;
end;
case
((PR^PR1).n)`2 = 6;
then consider i,f,p,q such that
A30: 1 <= i and
A31: i < n and
A32: p '&' q = Suc(f) & f = (PR.i)`1 & Ant(f)^<*p*> = (PR.n)`1 by A3,A5,Def7;
i <= len PR by A2,A31,XXREAL_0:2;
then i in dom PR by A30,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A30,A31,A32;
end;
case
((PR^PR1).n)`2 = 7;
then consider i,f,p,q such that
A33: 1 <= i and
A34: i < n and
A35: p '&' q = Suc(f) & f = (PR.i)`1 & Ant(f)^<*q*> = (PR.n)`1 by A3,A5,Def7;
i <= len PR by A2,A34,XXREAL_0:2;
then i in dom PR by A33,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A33,A34,A35;
end;
case
((PR^PR1).n)`2 = 8;
then consider i,f,p,x,y such that
A36: 1 <= i and
A37: i < n and
A38: Suc(f) = All(x,p) & f = (PR.i)`1 & Ant(f)^<*p.(x,y)*> = (PR.n)
`1 by A3,A5,Def7;
i <= len PR by A2,A37,XXREAL_0:2;
then i in dom PR by A36,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A36,A37,A38;
end;
case
((PR^PR1).n)`2 = 9;
then consider i,f,p,x,y such that
A39: 1 <= i and
A40: i < n and
A41: Suc(f) = p.(x,y) & not y in still_not-bound_in (Ant(f)) & (
not y in still_not-bound_in All(x,p))& f = (PR.i)`1 & Ant(f)^<*All(x,p)*> = (PR
.n)`1 by A3,A5,Def7;
i <= len PR by A2,A40,XXREAL_0:2;
then i in dom PR by A39,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A39,A40,A41;
end;
end;
assume
A42: PR^PR1,n is_a_correct_step;
(PR.n)`2 = 0 or ... or (PR.n)`2 = 9 by A1,A2,Th31;
then per cases;
case
(PR.n)`2 = 0;
hence thesis by A3,A42,Def7;
end;
case
(PR.n)`2 = 1;
hence thesis by A3,A42,Def7;
end;
case
(PR.n)`2 = 2;
then consider i,f,g such that
A43: 1 <= i and
A44: i < n and
A45: Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & ((PR^PR1).i)
`1 = f & ((PR^PR1).n)`1 = g by A3,A42,Def7;
i <= len PR by A2,A44,XXREAL_0:2;
then i in dom PR by A43,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A43,A44,A45;
end;
case
(PR.n)`2 = 3;
then consider i,j,f,f1 such that
A46: 1 <= i and
A47: i < n and
A48: 1 <= j and
A49: j < i and
A50: len f > 1 & len f1 > 1 & Ant(Ant(f)) = Ant(Ant(f1)) & 'not' Suc(
Ant(f )) = Suc(Ant(f1)) & Suc(f) = Suc(f1) & f = ((PR^PR1).j)`1 & f1 = ((PR^PR1
). i)`1 & Ant(Ant (f))^<*Suc(f)*> = ((PR^PR1).n)`1 by A3,A42,Def7;
A51: i <= len PR by A2,A47,XXREAL_0:2;
then i in Seg(len PR) by A46,FINSEQ_1:1;
then i in dom PR by FINSEQ_1:def 3;
then
A52: PR.i = (PR^PR1).i by FINSEQ_1:def 7;
j <= len PR by A49,A51,XXREAL_0:2;
then j in dom PR by A48,FINSEQ_3:25;
then PR.j = (PR^PR1).j by FINSEQ_1:def 7;
hence thesis by A3,A46,A47,A48,A49,A50,A52;
end;
case
(PR.n)`2 = 4;
then consider i,j,f,g,p such that
A53: 1 <= i and
A54: i < n and
A55: 1 <= j and
A56: j < i and
A57: len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc(
f) = Suc( g) & f = ((PR^PR1).j)`1 & g = ((PR^PR1).i)`1 & Ant(Ant(f))^<*p*> = ((
PR^ PR1). n)`1 by A3,A42,Def7;
A58: i <= len PR by A2,A54,XXREAL_0:2;
then i in Seg(len PR) by A53,FINSEQ_1:1;
then i in dom PR by FINSEQ_1:def 3;
then
A59: PR.i = (PR^PR1).i by FINSEQ_1:def 7;
j <= len PR by A56,A58,XXREAL_0:2;
then j in dom PR by A55,FINSEQ_3:25;
then PR.j = (PR^PR1).j by FINSEQ_1:def 7;
hence thesis by A3,A53,A54,A55,A56,A57,A59;
end;
case
(PR.n)`2 = 5;
then consider i,j,f,g such that
A60: 1 <= i and
A61: i < n and
A62: 1 <= j and
A63: j < i and
A64: Ant(f) = Ant(g) & f = ((PR^PR1).j)`1 & g = ((PR^PR1).i)`1 & Ant(
f)^<* (Suc(f)) '&' (Suc(g))*> = ((PR^PR1).n)`1 by A3,A42,Def7;
A65: i <= len PR by A2,A61,XXREAL_0:2;
then i in Seg(len PR) by A60,FINSEQ_1:1;
then i in dom PR by FINSEQ_1:def 3;
then
A66: PR.i = (PR^PR1).i by FINSEQ_1:def 7;
j <= len PR by A63,A65,XXREAL_0:2;
then j in dom PR by A62,FINSEQ_3:25;
then PR.j = (PR^PR1).j by FINSEQ_1:def 7;
hence thesis by A3,A60,A61,A62,A63,A64,A66;
end;
case
(PR.n)`2 = 6;
then consider i,f,p,q such that
A67: 1 <= i and
A68: i < n and
A69: p '&' q = Suc(f) & f = ((PR^PR1).i)`1 & Ant(f)^<*p*> = ((PR^PR1)
.n)`1 by A3,A42,Def7;
i <= len PR by A2,A68,XXREAL_0:2;
then i in dom PR by A67,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A67,A68,A69;
end;
case
(PR.n)`2 = 7;
then consider i,f,p,q such that
A70: 1 <= i and
A71: i < n and
A72: p '&' q = Suc(f) & f = ((PR^PR1).i)`1 & Ant(f)^<*q*>= ((PR^PR1).
n)`1 by A3,A42,Def7;
i <= len PR by A2,A71,XXREAL_0:2;
then i in dom PR by A70,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A70,A71,A72;
end;
case
(PR.n)`2 = 8;
then consider i,f,p,x,y such that
A73: 1 <= i and
A74: i < n and
A75: Suc(f) = All(x,p) & f = ((PR^PR1).i)`1 & Ant(f)^<*p.(x,y)*> = ((
PR^PR1). n)`1 by A3,A42,Def7;
i <= len PR by A2,A74,XXREAL_0:2;
then i in dom PR by A73,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A73,A74,A75;
end;
case
(PR.n)`2 = 9;
then consider i,f,p,x,y such that
A76: 1 <= i and
A77: i < n and
A78: Suc(f) = p.(x,y) & not y in still_not-bound_in (Ant(f)) & ( not
y in still_not-bound_in All(x,p))& f = ((PR^PR1).i)`1 & Ant(f)^<*All(x,p)*> = (
( PR^PR1).n)`1 by A3,A42,Def7;
i <= len PR by A2,A77,XXREAL_0:2;
then i in dom PR by A76,FINSEQ_3:25;
then PR.i = (PR^PR1).i by FINSEQ_1:def 7;
hence thesis by A3,A76,A77,A78;
end;
end;
theorem Th35:
1 <= n & n <= len PR1 & PR1,n is_a_correct_step implies (PR^PR1)
,(n+len PR) is_a_correct_step
proof
assume that
A1: 1 <= n and
A2: n <= len PR1 and
A3: PR1,n is_a_correct_step;
n in dom PR1 by A1,A2,FINSEQ_3:25;
then
A4: PR1.n = (PR^PR1).(n+len PR) by FINSEQ_1:def 7;
n + len PR <= len PR + len PR1 by A2,XREAL_1:6;
then
A5: n+len PR <= len(PR^PR1) by FINSEQ_1:22;
((PR^PR1).(n+len PR))`2 = 0 or ... or ((PR^PR1).(n+len PR))`2 = 9
by A1,A5,Th31,NAT_1:12;
then per cases;
case
((PR^PR1).(n+len PR))`2 = 0;
hence thesis by A3,A4,Def7;
end;
case
((PR^PR1).(n+len PR))`2 = 1;
hence thesis by A3,A4,Def7;
end;
case
((PR^PR1).(n+len PR))`2 = 2;
then consider i,f,g such that
A6: 1 <= i and
A7: i < n and
A8: Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & (PR1.i)`1 = f
& ( PR1.n)`1 = g by A3,A4,Def7;
i <= len PR1 by A2,A7,XXREAL_0:2;
then i in dom PR1 by A6,FINSEQ_3:25;
then
A9: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A6,A7,NAT_1:12,XREAL_1:6;
hence thesis by A4,A8,A9;
end;
case
((PR^PR1).(n+len PR))`2 = 3;
then consider i,j,f,f1 such that
A10: 1 <= i and
A11: i < n and
A12: 1 <= j and
A13: j < i and
A14: len f > 1 & len f1 > 1 & Ant(Ant(f)) = Ant(Ant(f1)) & 'not' Suc(
Ant(f )) = Suc(Ant(f1)) & Suc(f) = Suc(f1) & f = (PR1.j)`1 & f1 = (PR1.i)`1 &
Ant (Ant(f))^<*Suc (f)*> = (PR1.n)`1 by A3,A4,Def7;
A15: 1 <= len PR+j & len PR+j < i+len PR by A12,A13,NAT_1:12,XREAL_1:6;
A16: i <= len PR1 by A2,A11,XXREAL_0:2;
then i in dom PR1 by A10,FINSEQ_3:25;
then
A17: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
j <= len PR1 by A13,A16,XXREAL_0:2;
then j in dom PR1 by A12,FINSEQ_3:25;
then
A18: PR1.j = (PR^PR1).(len PR+j) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A10,A11,NAT_1:12,XREAL_1:6;
hence thesis by A4,A14,A15,A17,A18;
end;
case
((PR^PR1).(n+len PR))`2 = 4;
then consider i,j,f,g,p such that
A19: 1 <= i and
A20: i < n and
A21: 1 <= j and
A22: j < i and
A23: len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc(f
) = Suc( g) & f = (PR1.j)`1 & g = (PR1.i)`1 & Ant(Ant(f))^<*p*> = (PR1.n)`1 by
A3,A4,Def7;
A24: 1 <= len PR+j & len PR+j < i+len PR by A21,A22,NAT_1:12,XREAL_1:6;
A25: i <= len PR1 by A2,A20,XXREAL_0:2;
then i in dom PR1 by A19,FINSEQ_3:25;
then
A26: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
j <= len PR1 by A22,A25,XXREAL_0:2;
then j in dom PR1 by A21,FINSEQ_3:25;
then
A27: PR1.j = (PR^PR1).(len PR+j) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A19,A20,NAT_1:12,XREAL_1:6;
hence thesis by A4,A23,A24,A26,A27;
end;
case
((PR^PR1).(n+len PR))`2 = 5;
then consider i,j,f,g such that
A28: 1 <= i and
A29: i < n and
A30: 1 <= j and
A31: j < i and
A32: Ant(f) = Ant(g) & f = (PR1.j)`1 & g = (PR1.i)`1 & Ant(f)^<*(Suc(f
)) '&' (Suc(g))*> = (PR1.n)`1 by A3,A4,Def7;
A33: 1 <= len PR+j & len PR+j < i+len PR by A30,A31,NAT_1:12,XREAL_1:6;
A34: i <= len PR1 by A2,A29,XXREAL_0:2;
then i in dom PR1 by A28,FINSEQ_3:25;
then
A35: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
j <= len PR1 by A31,A34,XXREAL_0:2;
then j in dom PR1 by A30,FINSEQ_3:25;
then
A36: PR1.j = (PR^PR1).(len PR+j) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A28,A29,NAT_1:12,XREAL_1:6;
hence thesis by A4,A32,A33,A35,A36;
end;
case
((PR^PR1).(n+len PR))`2 = 6;
then consider i,f,p,q such that
A37: 1 <= i and
A38: i < n and
A39: p '&' q = Suc(f) & f = (PR1.i)`1 & Ant(f)^<*p*> = (PR1.n)`1 by A3,A4,Def7;
i <= len PR1 by A2,A38,XXREAL_0:2;
then i in dom PR1 by A37,FINSEQ_3:25;
then
A40: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A37,A38,NAT_1:12,XREAL_1:6;
hence thesis by A4,A39,A40;
end;
case
((PR^PR1).(n+len PR))`2 = 7;
then consider i,f,p,q such that
A41: 1 <= i and
A42: i < n and
A43: p '&' q = Suc(f) & f = (PR1.i)`1 & Ant(f)^<*q*>= (PR1.n)`1 by A3,A4,Def7;
i <= len PR1 by A2,A42,XXREAL_0:2;
then i in dom PR1 by A41,FINSEQ_3:25;
then
A44: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A41,A42,NAT_1:12,XREAL_1:6;
hence thesis by A4,A43,A44;
end;
case
((PR^PR1).(n+len PR))`2 = 8;
then consider i,f,p,x,y such that
A45: 1 <= i and
A46: i < n and
A47: Suc(f) = All(x,p) & f = (PR1.i)`1 & Ant(f)^<*p.(x,y)*> = (PR1.n)
`1 by A3,A4,Def7;
i <= len PR1 by A2,A46,XXREAL_0:2;
then i in dom PR1 by A45,FINSEQ_3:25;
then
A48: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A45,A46,NAT_1:12,XREAL_1:6;
hence thesis by A4,A47,A48;
end;
case
((PR^PR1).(n+len PR))`2 = 9;
then consider i,f,p,x,y such that
A49: 1 <= i and
A50: i < n and
A51: Suc(f) = p.(x,y) & not y in still_not-bound_in (Ant(f)) & ( not
y in still_not-bound_in All(x,p))& f = (PR1.i)`1 & Ant(f)^<*All(x,p)*> = (PR1.n
) `1 by A3,A4,Def7;
i <= len PR1 by A2,A50,XXREAL_0:2;
then i in dom PR1 by A49,FINSEQ_3:25;
then
A52: PR1.i = (PR^PR1).(len PR+i) by FINSEQ_1:def 7;
1 <= len PR+i & len PR+i < n+len PR by A49,A50,NAT_1:12,XREAL_1:6;
hence thesis by A4,A51,A52;
end;
end;
theorem Th36:
Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) & |- f implies |- g
proof
assume that
A1: Ant(f) is_Subsequence_of Ant(g) & Suc(f) = Suc(g) and
A2: |- f;
consider PR such that
A3: PR is a_proof and
A4: (PR.(len PR))`1 = f by A2;
A5: g in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[g,2]*>;
then a in {[g,2]} by FINSEQ_1:38;
then a = [g,2] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A5,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[g,2]*> c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider PR1 = <*[g,2]*> as FinSequence of [:set_of_CQC-WFF-seq(Al),
Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A6: 1 in dom PR1 by FINSEQ_1:38;
set PR2 = PR^PR1;
reconsider PR2 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A7: PR <> {} by A3;
now
let n be Nat;
assume 1 <= n & n <= len PR2;
then
A8: n in dom PR2 by FINSEQ_3:25;
A9: now
A10: 1 <= len PR by A7,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A11: f = (PR2.(len PR))`1 by A4,FINSEQ_1:def 7;
given k being Nat such that
A12: k in dom PR1 and
A13: n = len PR + k;
k in Seg 1 by A12,FINSEQ_1:38;
then
A14: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A15: PR1.k = [g,2];
then (PR1.k)`1 = g;
then
A16: (PR2.n)`1 = g by A12,A13,FINSEQ_1:def 7;
(PR1.k)`2 = 2 by A15;
then
A17: (PR2.n)`2 = 2 by A12,A13,FINSEQ_1:def 7;
len PR < n by A13,A14,NAT_1:13;
hence PR2,n is_a_correct_step by A1,A16,A17,A10,A11,Def7;
end;
now
assume n in dom PR;
then
A18: 1 <= n & n <= len PR by FINSEQ_3:25;
then PR,n is_a_correct_step by A3;
hence PR2,n is_a_correct_step by A18,Th34;
end;
hence PR2,n is_a_correct_step by A8,A9,FINSEQ_1:25;
end;
then
A19: PR2 is a_proof;
PR2.(len PR2) = PR2.(len PR + len PR1) by FINSEQ_1:22;
then PR2.(len PR2) = PR2.(len PR + 1) by FINSEQ_1:39;
then PR2.(len PR2) = PR1.1 by A6,FINSEQ_1:def 7;
then PR2.(len PR2) = [g,2];
then (PR2.(len PR2))`1 = g;
hence thesis by A19;
end;
theorem Th37:
1 < len f & 1 < len g & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc(
Ant(f)) = Suc(Ant(g)) & Suc(f) = Suc(g) & |- f & |- g implies |- Ant(Ant(f))^<*
Suc(f)*>
proof
assume that
A1: 1 < len f & 1 < len g & Ant(Ant(f)) = Ant(Ant(g)) & 'not' Suc(Ant(f)
) = Suc(Ant(g)) & Suc(f) = Suc(g) and
A2: |- f and
A3: |- g;
consider PR1 such that
A4: PR1 is a_proof and
A5: g = (PR1.(len PR1))`1 by A3;
consider PR such that
A6: PR is a_proof and
A7: f = (PR.(len PR))`1 by A2;
A8: Ant(Ant(f))^<*Suc(f)*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(Ant(f))^<*Suc(f)*>,3]*>;
then a in {[Ant(Ant(f))^<*Suc(f)*>,3]} by FINSEQ_1:38;
then a = [Ant(Ant(f))^<*Suc(f)*>,3] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A8,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[Ant(Ant(f))^<*Suc(f)*>,3]*> c= [:set_of_CQC-WFF-seq(Al),
Proof_Step_Kinds:];
then reconsider PR2 = <*[Ant(Ant(f))^<*Suc(f)*>,3]*> as FinSequence of [:
set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A9: 1 in dom PR2 by FINSEQ_1:38;
set PR3 = PR^PR1^PR2;
reconsider PR3 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A10: PR <> {} by A6;
now
let n be Nat;
assume 1 <= n & n <= len PR3;
then
A11: n in dom PR3 by FINSEQ_3:25;
A12: now
given k being Nat such that
A13: k in dom PR2 and
A14: n = len (PR^PR1) + k;
k in Seg 1 by A13,FINSEQ_1:38;
then
A15: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A16: PR2.k = [Ant(Ant(f))^<*Suc(f)*>,3];
then (PR2.k)`1 = Ant(Ant(f))^<*Suc(f)*>;
then
A17: (PR3.n)`1 = Ant(Ant(f))^<*Suc(f)*> by A13,A14,FINSEQ_1:def 7;
(PR2.k)`2 = 3 by A16;
then
A18: (PR3.n)`2 = 3 by A13,A14,FINSEQ_1:def 7;
A19: len (PR^PR1) < n by A14,A15,NAT_1:13;
A20: 1 <= len PR by A10,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A21: f = ((PR^PR1).(len PR))`1 by A7,FINSEQ_1:def 7;
A22: PR1 <> {} by A4;
then
A23: len PR < len (PR^PR1) by Th6;
then len PR in dom (PR^PR1) by A20,FINSEQ_3:25;
then
A24: f = (PR3.(len PR))`1 by A21,FINSEQ_1:def 7;
1 <= len PR1 by A22,Th6;
then len PR1 in dom PR1 by FINSEQ_3:25;
then g = ((PR^PR1).(len PR + len PR1))`1 by A5,FINSEQ_1:def 7;
then
A25: g = ((PR^PR1).(len (PR^PR1)))`1 by FINSEQ_1:22;
1 <= len (PR^PR1) by A10,Th6;
then len (PR^PR1) in dom (PR^PR1) by FINSEQ_3:25;
then
A26: g = (PR3.(len (PR^PR1)))`1 by A25,FINSEQ_1:def 7;
1 <= len (PR^PR1) by A10,Th6;
hence PR3,n is_a_correct_step by A1,A17,A18,A20,A23,A24,A19,A26,Def7;
end;
now
A27: now
given k being Nat such that
A28: k in dom PR1 and
A29: n = len PR + k;
A30: 1 <= k by A28,FINSEQ_3:25;
A31: k <= len PR1 by A28,FINSEQ_3:25;
then n <= len PR1 + len PR by A29,XREAL_1:6;
then
A32: n <= len (PR^PR1) by FINSEQ_1:22;
k <= n by A29,NAT_1:11;
then
A33: 1 <= n by A30,XXREAL_0:2;
PR1,k is_a_correct_step by A4,A30,A31;
then (PR^PR1),n is_a_correct_step by A29,A30,A31,Th35;
hence PR3,n is_a_correct_step by A33,A32,Th34;
end;
A34: now
assume
A35: n in dom PR;
then
A36: 1 <= n by FINSEQ_3:25;
A37: n <= len PR by A35,FINSEQ_3:25;
len PR <= len (PR^PR1) by Th6;
then
A38: n <= len (PR^PR1) by A37,XXREAL_0:2;
PR,n is_a_correct_step by A6,A36,A37;
then PR^PR1,n is_a_correct_step by A36,A37,Th34;
hence PR3,n is_a_correct_step by A36,A38,Th34;
end;
assume n in dom (PR^PR1);
hence PR3,n is_a_correct_step by A34,A27,FINSEQ_1:25;
end;
hence PR3,n is_a_correct_step by A11,A12,FINSEQ_1:25;
end;
then
A39: PR3 is a_proof;
PR3.(len PR3) = PR3.(len (PR^PR1) + len PR2) by FINSEQ_1:22;
then PR3.(len PR3) = PR3.(len (PR^PR1) + 1) by FINSEQ_1:39;
then PR3.(len PR3) = PR2.1 by A9,FINSEQ_1:def 7;
then PR3.(len PR3) = [Ant(Ant(f))^<*Suc(f)*>,3];
then (PR3.(len PR3))`1 = Ant(Ant(f))^<*Suc(f)*>;
hence thesis by A39;
end;
theorem Th38:
len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc(
f) = Suc(g) & |- f & |- g implies |- Ant(Ant(f))^<*p*>
proof
assume that
A1: len f > 1 & Ant(f) = Ant(g) & Suc(Ant(f)) = 'not' p & 'not' Suc(f) =
Suc(g) and
A2: |- f and
A3: |- g;
consider PR1 such that
A4: PR1 is a_proof and
A5: g = (PR1.(len PR1))`1 by A3;
consider PR such that
A6: PR is a_proof and
A7: f = (PR.(len PR))`1 by A2;
A8: Ant(Ant(f))^<*p*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(Ant(f))^<*p*>,4]*>;
then a in {[Ant(Ant(f))^<*p*>,4]} by FINSEQ_1:38;
then a = [Ant(Ant(f))^<*p*>,4] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A8,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[Ant(Ant(f))^<*p*>,4]*> c=
[:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider PR2 = <*[Ant(Ant(f))^<*p*>,4]*> as FinSequence of [:
set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A9: 1 in dom PR2 by FINSEQ_1:38;
set PR3 = PR^PR1^PR2;
reconsider PR3 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A10: PR <> {} by A6;
now
let n be Nat;
assume 1 <= n & n <= len PR3;
then
A11: n in dom PR3 by FINSEQ_3:25;
A12: now
given k being Nat such that
A13: k in dom PR2 and
A14: n = len (PR^PR1) + k;
k in Seg 1 by A13,FINSEQ_1:38;
then
A15: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A16: PR2.k = [Ant(Ant(f))^<*p*>,4];
then (PR2.k)`1 = Ant(Ant(f))^<*p*>;
then
A17: (PR3.n)`1 = Ant(Ant(f))^<*p*> by A13,A14,FINSEQ_1:def 7;
(PR2.k)`2 = 4 by A16;
then
A18: (PR3.n)`2 = 4 by A13,A14,FINSEQ_1:def 7;
A19: len (PR^PR1) < n by A14,A15,NAT_1:13;
A20: 1 <= len PR by A10,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A21: f = ((PR^PR1).(len PR))`1 by A7,FINSEQ_1:def 7;
A22: PR1 <> {} by A4;
then
A23: len PR < len (PR^PR1) by Th6;
then len PR in dom (PR^PR1) by A20,FINSEQ_3:25;
then
A24: f = (PR3.(len PR))`1 by A21,FINSEQ_1:def 7;
1 <= len PR1 by A22,Th6;
then len PR1 in dom PR1 by FINSEQ_3:25;
then g = ((PR^PR1).(len PR + len PR1))`1 by A5,FINSEQ_1:def 7;
then
A25: g = ((PR^PR1).(len (PR^PR1)))`1 by FINSEQ_1:22;
1 <= len (PR^PR1) by A10,Th6;
then len (PR^PR1) in dom (PR^PR1) by FINSEQ_3:25;
then
A26: g = (PR3.(len (PR^PR1)))`1 by A25,FINSEQ_1:def 7;
1 <= len (PR^PR1) by A10,Th6;
hence PR3,n is_a_correct_step by A1,A17,A18,A20,A23,A24,A19,A26,Def7;
end;
now
A27: now
given k being Nat such that
A28: k in dom PR1 and
A29: n = len PR + k;
A30: 1 <= k by A28,FINSEQ_3:25;
A31: k <= len PR1 by A28,FINSEQ_3:25;
then n <= len PR1 + len PR by A29,XREAL_1:6;
then
A32: n <= len (PR^PR1) by FINSEQ_1:22;
k <= n by A29,NAT_1:11;
then
A33: 1 <= n by A30,XXREAL_0:2;
PR1,k is_a_correct_step by A4,A30,A31;
then (PR^PR1),n is_a_correct_step by A29,A30,A31,Th35;
hence PR3,n is_a_correct_step by A33,A32,Th34;
end;
A34: now
assume
A35: n in dom PR;
then
A36: 1 <= n by FINSEQ_3:25;
A37: n <= len PR by A35,FINSEQ_3:25;
len PR <= len (PR^PR1) by Th6;
then
A38: n <= len (PR^PR1) by A37,XXREAL_0:2;
PR,n is_a_correct_step by A6,A36,A37;
then PR^PR1,n is_a_correct_step by A36,A37,Th34;
hence PR3,n is_a_correct_step by A36,A38,Th34;
end;
assume n in dom (PR^PR1);
hence PR3,n is_a_correct_step by A34,A27,FINSEQ_1:25;
end;
hence PR3,n is_a_correct_step by A11,A12,FINSEQ_1:25;
end;
then
A39: PR3 is a_proof;
PR3.(len PR3) = PR3.(len (PR^PR1) + len PR2) by FINSEQ_1:22;
then PR3.(len PR3) = PR3.(len (PR^PR1) + 1) by FINSEQ_1:39;
then PR3.(len PR3) = PR2.1 by A9,FINSEQ_1:def 7;
then PR3.(len PR3) = [Ant(Ant(f))^<*p*>,4];
then (PR3.(len PR3))`1 = Ant(Ant(f))^<*p*>;
hence thesis by A39;
end;
theorem Th39:
Ant(f) = Ant(g) & |- f & |- g implies |- Ant(f)^<*(Suc(f)) '&' ( Suc(g))*>
proof
assume that
A1: Ant(f) = Ant(g) and
A2: |- f and
A3: |- g;
consider PR1 such that
A4: PR1 is a_proof and
A5: g = (PR1.(len PR1))`1 by A3;
consider PR such that
A6: PR is a_proof and
A7: f = (PR.(len PR))`1 by A2;
A8: Ant(f)^<*(Suc(f)) '&' (Suc(g))*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5]*>;
then a in {[Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5]} by FINSEQ_1:38;
then a = [Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A8,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5]*> c=
[:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider
PR2 = <*[Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5]*> as FinSequence of
[:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A9: 1 in dom PR2 by FINSEQ_1:38;
set PR3 = PR^PR1^PR2;
reconsider PR3 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A10: PR <> {} by A6;
now
let n be Nat;
assume 1 <= n & n <= len PR3;
then
A11: n in dom PR3 by FINSEQ_3:25;
A12: now
given k being Nat such that
A13: k in dom PR2 and
A14: n = len (PR^PR1) + k;
k in Seg 1 by A13,FINSEQ_1:38;
then
A15: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A16: PR2.k = [Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5];
then (PR2.k)`1 = Ant(f)^<*(Suc(f)) '&' (Suc(g))*>;
then
A17: (PR3.n)`1 = Ant(f)^<*(Suc(f)) '&' (Suc(g))*> by A13,A14,FINSEQ_1:def 7;
(PR2.k)`2 = 5 by A16;
then
A18: (PR3.n)`2 = 5 by A13,A14,FINSEQ_1:def 7;
A19: len (PR^PR1) < n by A14,A15,NAT_1:13;
A20: 1 <= len PR by A10,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A21: f = ((PR^PR1).(len PR))`1 by A7,FINSEQ_1:def 7;
A22: PR1 <> {} by A4;
then
A23: len PR < len (PR^PR1) by Th6;
then len PR in dom (PR^PR1) by A20,FINSEQ_3:25;
then
A24: f = (PR3.(len PR))`1 by A21,FINSEQ_1:def 7;
1 <= len PR1 by A22,Th6;
then len PR1 in dom PR1 by FINSEQ_3:25;
then g = ((PR^PR1).(len PR + len PR1))`1 by A5,FINSEQ_1:def 7;
then
A25: g = ((PR^PR1).(len (PR^PR1)))`1 by FINSEQ_1:22;
1 <= len (PR^PR1) by A10,Th6;
then len (PR^PR1) in dom (PR^PR1) by FINSEQ_3:25;
then
A26: g = (PR3.(len (PR^PR1)))`1 by A25,FINSEQ_1:def 7;
1 <= len (PR^PR1) by A10,Th6;
hence PR3,n is_a_correct_step by A1,A17,A18,A20,A23,A24,A19,A26,Def7;
end;
now
A27: now
given k being Nat such that
A28: k in dom PR1 and
A29: n = len PR + k;
A30: 1 <= k by A28,FINSEQ_3:25;
A31: k <= len PR1 by A28,FINSEQ_3:25;
then n <= len PR1 + len PR by A29,XREAL_1:6;
then
A32: n <= len (PR^PR1) by FINSEQ_1:22;
k <= n by A29,NAT_1:11;
then
A33: 1 <= n by A30,XXREAL_0:2;
PR1,k is_a_correct_step by A4,A30,A31;
then (PR^PR1),n is_a_correct_step by A29,A30,A31,Th35;
hence PR3,n is_a_correct_step by A33,A32,Th34;
end;
A34: now
assume
A35: n in dom PR;
then
A36: 1 <= n by FINSEQ_3:25;
A37: n <= len PR by A35,FINSEQ_3:25;
len PR <= len (PR^PR1) by Th6;
then
A38: n <= len (PR^PR1) by A37,XXREAL_0:2;
PR,n is_a_correct_step by A6,A36,A37;
then PR^PR1,n is_a_correct_step by A36,A37,Th34;
hence PR3,n is_a_correct_step by A36,A38,Th34;
end;
assume n in dom (PR^PR1);
hence PR3,n is_a_correct_step by A34,A27,FINSEQ_1:25;
end;
hence PR3,n is_a_correct_step by A11,A12,FINSEQ_1:25;
end;
then
A39: PR3 is a_proof;
PR3.(len PR3) = PR3.(len (PR^PR1) + len PR2) by FINSEQ_1:22;
then PR3.(len PR3) = PR3.(len (PR^PR1) + 1) by FINSEQ_1:39;
then PR3.(len PR3) = PR2.1 by A9,FINSEQ_1:def 7;
then PR3.(len PR3) = [Ant(f)^<*(Suc(f)) '&' (Suc(g))*>,5];
then (PR3.(len PR3))`1 = Ant(f)^<*(Suc(f)) '&' (Suc(g))*>;
hence thesis by A39;
end;
theorem Th40:
p '&' q = Suc(f) & |- f implies |- Ant(f)^<*p*>
proof
assume that
A1: p '&' q = Suc(f) and
A2: |- f;
consider PR such that
A3: PR is a_proof and
A4: (PR.(len PR))`1 = f by A2;
A5: Ant(f)^<*p*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(f)^<*p*>,6]*>;
then a in {[Ant(f)^<*p*>,6]} by FINSEQ_1:38;
then a = [Ant(f)^<*p*>,6] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A5,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[Ant(f)^<*p*>,6]*> c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider
PR1 = <*[Ant(f)^<*p*>,6]*> as FinSequence of [:set_of_CQC-WFF-seq(Al)
,Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A6: 1 in dom PR1 by FINSEQ_1:38;
set PR2 = PR^PR1;
reconsider PR2 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A7: PR <> {} by A3;
now
let n be Nat;
assume 1 <= n & n <= len PR2;
then
A8: n in dom PR2 by FINSEQ_3:25;
A9: now
A10: 1 <= len PR by A7,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A11: f = (PR2.(len PR))`1 by A4,FINSEQ_1:def 7;
given k being Nat such that
A12: k in dom PR1 and
A13: n = len PR + k;
k in Seg 1 by A12,FINSEQ_1:38;
then
A14: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A15: PR1.k = [Ant(f)^<*p*>,6];
then (PR1.k)`1 = Ant(f)^<*p*>;
then
A16: (PR2.n)`1 = Ant(f)^<*p*> by A12,A13,FINSEQ_1:def 7;
(PR1.k)`2 = 6 by A15;
then
A17: (PR2.n)`2 = 6 by A12,A13,FINSEQ_1:def 7;
len PR < n by A13,A14,NAT_1:13;
hence PR2,n is_a_correct_step by A1,A16,A17,A10,A11,Def7;
end;
now
assume n in dom PR;
then
A18: 1 <= n & n <= len PR by FINSEQ_3:25;
then PR,n is_a_correct_step by A3;
hence PR2,n is_a_correct_step by A18,Th34;
end;
hence PR2,n is_a_correct_step by A8,A9,FINSEQ_1:25;
end;
then
A19: PR2 is a_proof;
PR2.(len PR2) = PR2.(len PR + len PR1) by FINSEQ_1:22;
then PR2.(len PR2) = PR2.(len PR + 1) by FINSEQ_1:39;
then PR2.(len PR2) = PR1.1 by A6,FINSEQ_1:def 7;
then PR2.(len PR2) = [Ant(f)^<*p*>,6];
then (PR2.(len PR2))`1 = Ant(f)^<*p*>;
hence thesis by A19;
end;
theorem Th41:
p '&' q = Suc(f) & |- f implies |- Ant(f)^<*q*>
proof
assume that
A1: p '&' q = Suc(f) and
A2: |- f;
consider PR such that
A3: PR is a_proof and
A4: (PR.(len PR))`1 = f by A2;
A5: Ant(f)^<*q*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(f)^<*q*>,7]*>;
then a in {[Ant(f)^<*q*>,7]} by FINSEQ_1:38;
then a = [Ant(f)^<*q*>,7] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A5,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[Ant(f)^<*q*>,7]*> c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
then reconsider
PR1 = <*[Ant(f)^<*q*>,7]*> as FinSequence of [:set_of_CQC-WFF-seq(Al)
,Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A6: 1 in dom PR1 by FINSEQ_1:38;
set PR2 = PR^PR1;
reconsider PR2 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A7: PR <> {} by A3;
now
let n be Nat;
assume 1 <= n & n <= len PR2;
then
A8: n in dom PR2 by FINSEQ_3:25;
A9: now
A10: 1 <= len PR by A7,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A11: f = (PR2.(len PR))`1 by A4,FINSEQ_1:def 7;
given k being Nat such that
A12: k in dom PR1 and
A13: n = len PR + k;
k in Seg 1 by A12,FINSEQ_1:38;
then
A14: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A15: PR1.k = [Ant(f)^<*q*>,7];
then (PR1.k)`1 = Ant(f)^<*q*>;
then
A16: (PR2.n)`1 = Ant(f)^<*q*> by A12,A13,FINSEQ_1:def 7;
(PR1.k)`2 = 7 by A15;
then
A17: (PR2.n)`2 = 7 by A12,A13,FINSEQ_1:def 7;
len PR < n by A13,A14,NAT_1:13;
hence PR2,n is_a_correct_step by A1,A16,A17,A10,A11,Def7;
end;
now
assume n in dom PR;
then
A18: 1 <= n & n <= len PR by FINSEQ_3:25;
then PR,n is_a_correct_step by A3;
hence PR2,n is_a_correct_step by A18,Th34;
end;
hence PR2,n is_a_correct_step by A8,A9,FINSEQ_1:25;
end;
then
A19: PR2 is a_proof;
PR2.(len PR2) = PR2.(len PR + len PR1) by FINSEQ_1:22;
then PR2.(len PR2) = PR2.(len PR + 1) by FINSEQ_1:39;
then PR2.(len PR2) = PR1.1 by A6,FINSEQ_1:def 7;
then PR2.(len PR2) = [Ant(f)^<*q*>,7];
then (PR2.(len PR2))`1 = Ant(f)^<*q*>;
hence thesis by A19;
end;
theorem Th42:
Suc(f) = All(x,p) & |- f implies |- Ant(f)^<*p.(x,y)*>
proof
assume that
A1: Suc(f) = All(x,p) and
A2: |- f;
consider PR such that
A3: PR is a_proof and
A4: (PR.(len PR))`1 = f by A2;
A5: Ant(f)^<*p.(x,y)*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(f)^<*p.(x,y)*>,8]*>;
then a in {[Ant(f)^<*p.(x,y)*>,8]} by FINSEQ_1:38;
then a = [Ant(f)^<*p.(x,y)*>,8] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A5,CQC_THE1:21
,ZFMISC_1:87;
end;
then
rng <*[Ant(f)^<*p.(x,y)*>,8]*> c= [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds
:];
then reconsider PR1 = <*[Ant(f)^<*p.(x,y)*>,8]*> as FinSequence of [:
set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A6: 1 in dom PR1 by FINSEQ_1:38;
set PR2 = PR^PR1;
reconsider PR2 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A7: PR <> {} by A3;
now
let n be Nat;
assume 1 <= n & n <= len PR2;
then
A8: n in dom PR2 by FINSEQ_3:25;
A9: now
A10: 1 <= len PR by A7,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A11: f = (PR2.(len PR))`1 by A4,FINSEQ_1:def 7;
given k being Nat such that
A12: k in dom PR1 and
A13: n = len PR + k;
k in Seg 1 by A12,FINSEQ_1:38;
then
A14: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A15: PR1.k = [Ant(f)^<*p.(x,y)*>,8];
then (PR1.k)`1 = Ant(f)^<*p.(x,y)*>;
then
A16: (PR2.n)`1 = Ant(f)^<*p.(x,y)*> by A12,A13,FINSEQ_1:def 7;
(PR1.k)`2 = 8 by A15;
then
A17: (PR2.n)`2 = 8 by A12,A13,FINSEQ_1:def 7;
len PR < n by A13,A14,NAT_1:13;
hence PR2,n is_a_correct_step by A1,A16,A17,A10,A11,Def7;
end;
now
assume n in dom PR;
then
A18: 1 <= n & n <= len PR by FINSEQ_3:25;
then PR,n is_a_correct_step by A3;
hence PR2,n is_a_correct_step by A18,Th34;
end;
hence PR2,n is_a_correct_step by A8,A9,FINSEQ_1:25;
end;
then
A19: PR2 is a_proof;
PR2.(len PR2) = PR2.(len PR + len PR1) by FINSEQ_1:22;
then PR2.(len PR2) = PR2.(len PR + 1) by FINSEQ_1:39;
then PR2.(len PR2) = PR1.1 by A6,FINSEQ_1:def 7;
then PR2.(len PR2) = [Ant(f)^<*p.(x,y)*>,8];
then (PR2.(len PR2))`1 = Ant(f)^<*p.(x,y)*>;
hence thesis by A19;
end;
theorem Th43:
Suc(f) = p.(x,y) & not y in still_not-bound_in Ant(f) & not y in
still_not-bound_in All(x,p) & |- f implies |- Ant(f)^<*All(x,p)*>
proof
assume that
A1: Suc(f) = p.(x,y) & not y in still_not-bound_in (Ant(f)) & not y in
still_not-bound_in All(x,p) and
A2: |- f;
consider PR such that
A3: PR is a_proof and
A4: (PR.(len PR))`1 = f by A2;
A5: Ant(f)^<*All(x,p)*> in set_of_CQC-WFF-seq(Al) by Def6;
now
let a be object;
assume a in rng <*[Ant(f)^<*All(x,p)*>,9]*>;
then a in {[Ant(f)^<*All(x,p)*>,9]} by FINSEQ_1:38;
then a = [Ant(f)^<*All(x,p)*>,9] by TARSKI:def 1;
hence a in [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by A5,CQC_THE1:21
,ZFMISC_1:87;
end;
then rng <*[Ant(f)^<*All(x,p)*>,9]*> c= [:set_of_CQC-WFF-seq(Al),
Proof_Step_Kinds:];
then reconsider PR1 = <*[Ant(f)^<*All(x,p)*>,9]*> as FinSequence of [:
set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:] by FINSEQ_1:def 4;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A6: 1 in dom PR1 by FINSEQ_1:38;
set PR2 = PR^PR1;
reconsider PR2 as FinSequence of [:set_of_CQC-WFF-seq(Al),Proof_Step_Kinds:];
A7: PR <> {} by A3;
now
let n be Nat;
assume 1 <= n & n <= len PR2;
then
A8: n in dom PR2 by FINSEQ_3:25;
A9: now
A10: 1 <= len PR by A7,Th6;
then len PR in dom PR by FINSEQ_3:25;
then
A11: f = (PR2.(len PR))`1 by A4,FINSEQ_1:def 7;
given k being Nat such that
A12: k in dom PR1 and
A13: n = len PR + k;
k in Seg 1 by A12,FINSEQ_1:38;
then
A14: k = 1 by FINSEQ_1:2,TARSKI:def 1;
then
A15: PR1.k = [Ant(f)^<*All(x,p)*>,9];
then (PR1.k)`1 = Ant(f)^<*All(x,p)*>;
then
A16: (PR2.n)`1 = Ant(f)^<*All(x,p)*> by A12,A13,FINSEQ_1:def 7;
(PR1.k)`2 = 9 by A15;
then
A17: (PR2.n)`2 = 9 by A12,A13,FINSEQ_1:def 7;
len PR < n by A13,A14,NAT_1:13;
hence PR2,n is_a_correct_step by A1,A16,A17,A10,A11,Def7;
end;
now
assume n in dom PR;
then
A18: 1 <= n & n <= len PR by FINSEQ_3:25;
then PR,n is_a_correct_step by A3;
hence PR2,n is_a_correct_step by A18,Th34;
end;
hence PR2,n is_a_correct_step by A8,A9,FINSEQ_1:25;
end;
then
A19: PR2 is a_proof;
PR2.(len PR2) = PR2.(len PR + len PR1) by FINSEQ_1:22;
then PR2.(len PR2) = PR2.(len PR + 1) by FINSEQ_1:39;
then PR2.(len PR2) = PR1.1 by A6,FINSEQ_1:def 7;
then PR2.(len PR2) = [Ant(f)^<*All(x,p)*>,9];
then (PR2.(len PR2))`1 = Ant(f)^<*All(x,p)*>;
hence thesis by A19;
end;
theorem Th44:
|- f & |- Ant(f)^<*'not' Suc(f)*> implies |- Ant(f)^<*p*>
proof
assume that
A1: |- f and
A2: |- Ant(f)^<*'not' Suc(f)*>;
set f1 = Ant(f)^<*'not' p*>^<*Suc(f)*>;
Ant(f1) = Ant(f)^<*'not' p*> & Suc(f) = Suc(f1) by Th5;
then
A3: |- f1 by A1,Th8,Th36;
set f3 = Ant(f)^<*'not' p*>^<*'not' Suc(f)*>;
set f2 = Ant(f)^<*'not' Suc(f)*>;
Suc(f2) = 'not' Suc(f) by Th5;
then
A4: Suc(f2) = Suc(f3) by Th5;
Ant(f3) = Ant(f)^<*'not' p*> & Ant(f2) = Ant(f) by Th5;
then
A5: |- f3 by A2,A4,Th8,Th36;
Suc(f1) = Suc(f) by Th5;
then
A6: 'not' Suc(f1) = Suc(f3) by Th5;
A7: 1< len f1 by Th9;
A8: Ant(f1) = Ant(f)^<*'not' p*> by Th5;
then Ant(f1) = Ant(f3) & Suc(Ant(f1)) = 'not' p by Th5;
then |- Ant(Ant(f1))^<*p*> by A3,A5,A6,A7,Th38;
hence thesis by A8,Th5;
end;
theorem Th45:
1 <= len f & |- f & |- f^<*p*> implies |- Ant(f)^<*p*>
proof
assume that
A1: 1 <= len f and
A2: |- f and
A3: |- f^<*p*>;
set f2 = Ant(f)^<*'not' Suc(f)*>^<*'not' Suc(f)*>;
set f1 = Ant(f)^<*'not' Suc(f)*>^<*Suc(f)*>;
A4: Ant(f2) = Ant(f)^<*'not' Suc(f)*> by Th5;
then
A5: len Ant(f2) in dom Ant(f2) by Th10;
(Ant(f)^<*'not' Suc(f)*>).(len Ant(f) + 1) = 'not' Suc(f) by FINSEQ_1:42;
then (Ant(f2)).(len Ant(f) + 1) = 'not' Suc(f) by Th5;
then (Ant(f2)).(len Ant(f) + 1) = Suc(f2) by Th5;
then (Ant(f2)).(len Ant(f2)) = Suc(f2) by A4,FINSEQ_2:16;
then
A6: |- f2 by A5,Lm2,Th33;
set f4 = Ant(f1)^<*p*>;
f2 = Ant(f1)^<*'not' Suc(f)*> by Th5;
then
A7: f2 = Ant(f1)^<*'not' Suc(f1)*> by Th5;
Ant(f1) = Ant(f)^<*'not' Suc(f)*> & Suc(f1) = Suc(f) by Th5;
then |- f1 by A2,Th8,Th36;
then
A8: |- Ant(f1)^<*p*> by A6,A7,Th44;
set f3 = f^<*p*>;
1+1 <= len f + 1 by A1,XREAL_1:6;
then 1+1 <= len f + len <*p*> by FINSEQ_1:39;
then 1+1 <= len f3 by FINSEQ_1:22;
then
A9: 1 < len f3 by NAT_1:13;
A10: Ant(f1) = Ant(f)^<*'not' Suc(f)*> by Th5;
then Suc(Ant(f1)) = 'not' Suc(f) by Th5;
then Suc(Ant(f1)) = 'not' Suc(Ant(f3)) by Th5;
then
A11: Suc(Ant(f4)) = 'not' Suc(Ant(f3)) by Th5;
1 <= len Ant(f1) by A10,Th10;
then 1+1 <= len Ant(f1) + 1 by XREAL_1:6;
then 1+1 <= len Ant(f1) + len <*p*> by FINSEQ_1:39;
then 1+1 <= len f4 by FINSEQ_1:22;
then
A12: 1 < len f4 by NAT_1:13;
Ant(f4) = Ant(f1) by Th5;
then Ant(Ant(f4)) = Ant(f) by A10,Th5;
then
A13: Ant(Ant(f4)) = Ant(Ant(f3)) by Th5;
Suc(f4) = p by Th5;
then |- Ant(Ant(f3))^<*Suc(f3)*> by A3,A8,A9,A12,A13,A11,Th5,Th37;
then |- Ant(f)^<*Suc(f3)*> by Th5;
hence thesis by Th5;
end;
theorem Th46:
|- f^<*p*>^<*q*> implies |- f^<*'not' q*>^<*'not' p*>
proof
set f1 = f^<*p*>^<*q*>;
set f2 = Ant(Ant(f1))^<*'not' q*>^<*p*>^<*q*>;
assume
A1: |- f1;
A2: Ant(f1) = f^<*p*> by Th5;
then
A3: Ant(Ant(f1)) = f by Th5;
set f4 = Ant(Ant(f1))^<*'not' q*>^<*'not' p*>^<*'not' p*>;
set f3 = Ant(Ant(f1))^<*'not' q*>^<*p*>^<*'not' q*>;
A4: 1 < len f4 by Th9;
A5: Suc(Ant(f2)^<* 'not' p*>) = 'not' p by Th5;
then
A6: Suc(Ant(f2)^<* 'not' p*>) = Suc(f4) by Th5;
Ant(f3) = Ant(Ant(f1))^<*'not' q*>^<*p*> by Th5;
then Ant(f3) = Ant(Ant(f1))^(<*'not' q*>^<*p*>) by FINSEQ_1:32;
then
A7: Ant(f3) = Ant(Ant(f1))^<*'not' q,p*> by FINSEQ_1:def 9;
then (Ant(f3)).(len f+1) = 'not' q by A3,Th14;
then
A8: (Ant(f3)).(len f+1) = Suc(f3) by Th5;
Suc(f1) = q by Th5;
then
A9: Suc(f1) = Suc(f2) by Th5;
A10: Ant(f2) = Ant(Ant(f1))^<*'not' q*>^<*p*> by Th5;
then
A11: 1 < len (Ant(f2)^<* 'not' p*>) by Th9;
Suc(Ant(f1)) = p & 0+1 <= len Ant(f1) by A2,Th5,Th10;
then
A12: |- f2 by A1,A10,A9,Th13,Th36;
1 in dom <*'not' q,p*> by Th14;
then
A13: len f+1 in dom (Ant(f3)) by A3,A7,FINSEQ_1:28;
Suc(f2) = q & Ant(f2) = Ant(Ant(f1))^<*'not' q*>^<*p*> by Th5;
then |- Ant(f2)^<*'not' Suc(f2)*> by A8,A13,Lm2,Th33;
then
A14: |- Ant(f2)^<* 'not' p*> by A12,Th44;
A15: Ant(f4) = Ant(Ant(f1))^<*'not' q*>^<*'not' p*> by Th5;
then Ant(f4) = Ant(Ant(f1))^(<*'not' q*>^<*'not' p*>) by FINSEQ_1:32;
then
A16: Ant(f4) = Ant(Ant(f1))^<*'not' q,'not' p*> by FINSEQ_1:def 9;
then (Ant(f4)).(len f+2) = 'not' p by A3,Th14;
then
A17: (Ant(f4)).(len f+2) = Suc(f4) by Th5;
2 in dom <*'not' q,'not' p*> by Th14;
then len f+2 in dom (Ant(f4)) by A3,A16,FINSEQ_1:28;
then
A18: |- f4 by A17,Lm2,Th33;
A19: Ant(Ant(f2)^<* 'not' p*>) = Ant(Ant(f1))^<*'not' q*>^<*p*> by A10,Th5;
then Suc(Ant(Ant(f2)^<* 'not' p*>)) = p by Th5;
then
A20: 'not' Suc(Ant(Ant(f2)^<* 'not' p*>)) = Suc(Ant(f4)) by A15,Th5;
A21: Ant(Ant(Ant(f2)^<* 'not' p*>)) = Ant(Ant(f1))^<*'not' q*> by A19,Th5;
then Ant(Ant(f4)) = Ant(Ant(Ant(f2)^<* 'not' p*>)) by A15,Th5;
hence thesis by A3,A14,A18,A11,A4,A21,A20,A5,A6,Th37;
end;
theorem
|- f^<*'not' p*>^<*'not' q*> implies |- f^<*q*>^<*p*>
proof
set f1 = f^<*'not' p*>^<*'not' q*>;
set f2 = Ant(Ant(f1))^<*q*>^<*'not' p*>^<*'not' q*>;
assume
A1: |- f1;
A2: Ant(f2) = Ant(Ant(f1))^<*q*>^<*'not' p*> by Th5;
Suc(f1) = 'not' q by Th5;
then
A3: Suc(f1) = Suc(f2) by Th5;
A4: Ant(f1) = f^<*'not' p*> by Th5;
then
A5: Ant(Ant(f1)) = f by Th5;
Suc(Ant(f1)) = 'not' p & 0+1 <= len Ant(f1) by A4,Th5,Th10;
then
A6: |- f2 by A1,A2,A3,Th13,Th36;
set f4 = Ant(Ant(f1))^<*q*>^<*p*>^<*p*>;
set f3 = Ant(Ant(f1))^<*q*>^<*'not' p*>^<*q*>;
A7: 1 < len f4 by Th9;
A8: Ant(f3) = Ant(Ant(f1))^<*q*>^<*'not' p*> by Th5;
then
A9: 1 < len (Ant(f3)^<*p*>) by Th9;
Ant(f3) = Ant(Ant(f1))^(<*q*>^<*'not' p*>) by A8,FINSEQ_1:32;
then
A10: Ant(f3) = Ant(Ant(f1))^<*q,'not' p*> by FINSEQ_1:def 9;
then (Ant(f3)).(len f+1) = q by A5,Th14;
then
A11: (Ant(f3)).(len f+1) = Suc(f3) by Th5;
1 in dom <*q,'not' p*> by Th14;
then len f+1 in dom (Ant(f3)) by A5,A10,FINSEQ_1:28;
then
A12: |- f3 by A11,Lm2,Th33;
A13: Suc(Ant(f3)^<*p*>) = p by Th5;
then
A14: Suc(Ant(f3)^<*p*>) = Suc(f4) by Th5;
Ant(f2) = Ant(Ant(f1))^<*q*>^<*'not' p*> by Th5;
then
A15: Ant(f2) = Ant(f3) by Th5;
Suc(f2) = 'not' q by Th5;
then
A16: Suc(f2) = 'not' Suc(f3) by Th5;
A17: Ant(f4) = Ant(Ant(f1))^<*q*>^<*p*> by Th5;
then Ant(f4) = Ant(Ant(f1))^(<*q*>^<*p*>) by FINSEQ_1:32;
then
A18: Ant(f4) = Ant(Ant(f1))^<*q,p*> by FINSEQ_1:def 9;
then (Ant(f4)).(len f+2) = p by A5,Th14;
then
A19: (Ant(f4)).(len f+2) = Suc(f4) by Th5;
2 in dom <*q,p*> by Th14;
then len f+2 in dom (Ant(f4)) by A5,A18,FINSEQ_1:28;
then
A20: |- f4 by A19,Lm2,Th33;
A21: Ant(Ant(f3)^<*p*>) = Ant(Ant(f1))^<*q*>^<*'not' p*> by A8,Th5;
then Suc(Ant(Ant(f3)^<*p*>)) = 'not' p by Th5;
then
A22: Suc(Ant(Ant(f3)^<*p*>)) = 'not' Suc(Ant(f4)) by A17,Th5;
0+1 <= len f2 by Th10;
then |- Ant(f3)^<*'not' Suc(f3)*> by A6,A16,A15,Th3;
then
A23: |- Ant(f3)^<*p*> by A12,Th44;
A24: Ant(Ant(Ant(f3)^<*p*>)) = Ant(Ant(f1))^<*q*> by A21,Th5;
then Ant(Ant(f4)) = Ant(Ant(Ant(f3)^<*p*>)) by A17,Th5;
hence thesis by A5,A23,A20,A9,A7,A24,A22,A13,A14,Th37;
end;
theorem Th48:
|- f^<*'not' p*>^<*q*> implies |- f^<*'not' q*>^<*p*>
proof
set f1 = f^<*'not' p*>^<*q*>;
set f2 = Ant(Ant(f1))^<*'not' q*>^<*'not' p*>^<*q*>;
assume
A1: |- f1;
A2: Ant(f1) = f^<*'not' p*> by Th5;
then
A3: Ant(Ant(f1)) = f by Th5;
set f4 = Ant(Ant(f1))^<*'not' q*>^<*p*>^<*p*>;
set f3 = Ant(Ant(f1))^<*'not' q*>^<*'not' p*>^<*'not' q*>;
A4: 1 < len f4 by Th9;
Ant(f3) = Ant(Ant(f1))^<*'not' q*>^<*'not' p*> by Th5;
then Ant(f3) = Ant(Ant(f1))^(<*'not' q*>^<*'not' p*>) by FINSEQ_1:32;
then
A5: Ant(f3) = Ant(Ant(f1))^<*'not' q,'not' p*> by FINSEQ_1:def 9;
then (Ant(f3)).(len f+1) = 'not' q by A3,Th14;
then
A6: (Ant(f3)).(len f+1) = Suc(f3) by Th5;
1 in dom <*'not' q,'not' p*> by Th14;
then
A7: len f+1 in dom (Ant(f3)) by A3,A5,FINSEQ_1:28;
Suc(f1) = q by Th5;
then
A8: Suc(f1) = Suc(f2) by Th5;
A9: Ant(f2) = Ant(Ant(f1))^<*'not' q*>^<*'not' p*> by Th5;
then
A10: 1 < len (Ant(f2)^<* p*>) by Th9;
Suc(Ant(f1)) = 'not' p & 0+1 <= len Ant(f1) by A2,Th5,Th10;
then
A11: |- f2 by A1,A9,A8,Th13,Th36;
Suc(f2) = q & Ant(f2) = Ant(Ant(f1))^<*'not' q*>^<*'not' p*> by Th5;
then |- Ant(f2)^<*'not' Suc(f2)*> by A6,A7,Lm2,Th33;
then
A12: |- Ant(f2)^<*p*> by A11,Th44;
A13: Ant(f4) = Ant(Ant(f1))^<*'not' q*>^<*p*> by Th5;
then Ant(f4) = Ant(Ant(f1))^(<*'not' q*>^<*p*>) by FINSEQ_1:32;
then
A14: Ant(f4) = Ant(Ant(f1))^<*'not' q,p*> by FINSEQ_1:def 9;
then (Ant(f4)).(len f+2) = p by A3,Th14;
then
A15: (Ant(f4)).(len f+2) = Suc(f4) by Th5;
2 in dom <*'not' q,p*> by Th14;
then len f+2 in dom (Ant(f4)) by A3,A14,FINSEQ_1:28;
then
A16: |- f4 by A15,Lm2,Th33;
A17: Ant(Ant(f2)^<*p*>) = Ant(Ant(f1))^<*'not' q*>^<*'not' p*> by A9,Th5;
then Ant(Ant(Ant(f2)^<*p*>)) = Ant(Ant(f1))^<*'not' q*> by Th5;
then
A18: Ant(Ant(f4)) = Ant(Ant(Ant(f2)^<*p*>)) by A13,Th5;
Suc(Ant(Ant(f2)^<* p*>)) = 'not' p by A17,Th5;
then
A19: Suc(Ant(Ant(f2)^<*p*>)) = 'not' Suc(Ant(f4)) by A13,Th5;
A20: Suc(f4) = p by Th5;
then Suc(Ant(f2)^<*p*>) = Suc(f4) by Th5;
then |- Ant(Ant(f4))^<*p*> by A12,A16,A10,A4,A18,A19,A20,Th37;
hence thesis by A3,A13,Th5;
end;
theorem Th49:
|- f^<*p*>^<*'not' q*> implies |- f^<*q*>^<*'not' p*>
proof
set f1 = f^<*p*>^<*'not' q*>;
set f2 = Ant(Ant(f1))^<*q*>^<*p*>^<*'not' q*>;
assume
A1: |- f1;
A2: Ant(f2) = Ant(Ant(f1))^<*q*>^<*p*> by Th5;
Suc(f1) = 'not' q by Th5;
then
A3: Suc(f1) = Suc(f2) by Th5;
A4: Ant(f1) = f^<*p*> by Th5;
then
A5: Ant(Ant(f1)) = f by Th5;
Suc(Ant(f1)) = p & 0+1 <= len Ant(f1) by A4,Th5,Th10;
then
A6: |- f2 by A1,A2,A3,Th13,Th36;
set f4 = Ant(Ant(f1))^<*q*>^<*'not' p*>^<*'not' p*>;
set f3 = Ant(Ant(f1))^<*q*>^<*p*>^<*q*>;
A7: 1 < len f4 by Th9;
A8: Ant(f3) = Ant(Ant(f1))^<*q*>^<*p*> by Th5;
then
A9: 1 < len (Ant(f3)^<*'not' p*>) by Th9;
Ant(f3) = Ant(Ant(f1))^(<*q*>^<*p*>) by A8,FINSEQ_1:32;
then
A10: Ant(f3) = Ant(Ant(f1))^<*q,p*> by FINSEQ_1:def 9;
then (Ant(f3)).(len f+1) = q by A5,Th14;
then
A11: (Ant(f3)).(len f+1) = Suc(f3) by Th5;
1 in dom <*q,p*> by Th14;
then len f+1 in dom (Ant(f3)) by A5,A10,FINSEQ_1:28;
then
A12: |- f3 by A11,Lm2,Th33;
A13: Suc(Ant(f3)^<*'not' p*>) = 'not' p by Th5;
then
A14: Suc(Ant(f3)^<*'not' p*>) = Suc(f4) by Th5;
Ant(f2) = Ant(Ant(f1))^<*q*>^<*p*> by Th5;
then
A15: Ant(f2) = Ant(f3) by Th5;
Suc(f2) = 'not' q by Th5;
then
A16: Suc(f2) = 'not' Suc(f3) by Th5;
A17: Ant(f4) = Ant(Ant(f1))^<*q*>^<*'not' p*> by Th5;
then Ant(f4) = Ant(Ant(f1))^(<*q*>^<*'not' p*>) by FINSEQ_1:32;
then
A18: Ant(f4) = Ant(Ant(f1))^<*q,'not' p*> by FINSEQ_1:def 9;
then (Ant(f4)).(len f+2) = 'not' p by A5,Th14;
then
A19: (Ant(f4)).(len f+2) = Suc(f4) by Th5;
2 in dom <*q,'not' p*> by Th14;
then len f+2 in dom (Ant(f4)) by A5,A18,FINSEQ_1:28;
then
A20: |- f4 by A19,Lm2,Th33;
A21: Ant(Ant(f3)^<*'not' p*>) = Ant(Ant(f1))^<*q*>^<*p*> by A8,Th5;
then Suc(Ant(Ant(f3)^<*'not' p*>)) = p by Th5;
then
A22: 'not' Suc(Ant(Ant(f3)^<*'not' p*>)) = Suc(Ant(f4)) by A17,Th5;
0+1 <= len f2 by Th10;
then |- Ant(f3)^<*'not' Suc(f3)*> by A6,A16,A15,Th3;
then
A23: |- Ant(f3)^<*'not' p*> by A12,Th44;
A24: Ant(Ant(Ant(f3)^<*'not' p*>)) = Ant(Ant(f1))^<*q*> by A21,Th5;
then Ant(Ant(f4)) = Ant(Ant(Ant(f3)^<*'not' p*>)) by A17,Th5;
hence thesis by A5,A23,A20,A9,A7,A24,A22,A13,A14,Th37;
end;
::$CT
theorem
|- f^<*p*> implies |- f^<*p 'or' q*>
proof
set f1 = f^<*'not' p '&' 'not' q*>^<*'not' p '&' 'not' q*>;
assume
A1: |- f^<*p*>;
A2: Ant(f1) = f^<*'not' p '&' 'not' q*> by Th5;
len f+1 = len f + len <*'not' p '&' 'not' q*> by FINSEQ_1:39;
then len f+1 = len Ant(f1) by A2,FINSEQ_1:22;
then
A3: len f+1 in dom Ant(f1) by A2,Th10;
A4: Suc(f1) = 'not' p '&' 'not' q by Th5;
(Ant(f1)).(len f+1) = 'not' p '&' 'not' q by A2,FINSEQ_1:42;
then Suc(f1) is_tail_of Ant(f1) by A4,A3,Lm2;
then |- f^<*'not' p '&' 'not' q*>^<*'not' p*> by A2,A4,Th33,Th40;
then |- f^<*p*>^<*'not' ('not' p '&' 'not' q)*> by Th49;
then
A5: |- f^<*p*>^<*p 'or' q*> by QC_LANG2:def 3;
1 <= len (f^<*p*>) by Th10;
then |- Ant(f^<*p*>)^<*p 'or' q*> by A1,A5,Th45;
hence thesis by Th5;
end;
theorem
|- f^<*q*> implies |- f^<*p 'or' q*>
proof
set f1 = f^<*'not' p '&' 'not' q*>^<*'not' p '&' 'not' q*>;
assume
A1: |- f^<*q*>;
A2: Ant(f1) = f^<*'not' p '&' 'not' q*> by Th5;
len f+1 = len f + len <*'not' p '&' 'not' q*> by FINSEQ_1:39;
then len f+1 = len Ant(f1) by A2,FINSEQ_1:22;
then
A3: len f+1 in dom Ant(f1) by A2,Th10;
A4: Suc(f1) = 'not' p '&' 'not' q by Th5;
(Ant(f1)).(len f+1) = 'not' p '&' 'not' q by A2,FINSEQ_1:42;
then Suc(f1) is_tail_of Ant(f1) by A4,A3,Lm2;
then |- f^<*'not' p '&' 'not' q*>^<*'not' q*> by A2,A4,Th33,Th41;
then |- f^<*q*>^<*'not' ('not' p '&' 'not' q)*> by Th49;
then
A5: |- f^<*q*>^<*p 'or' q*> by QC_LANG2:def 3;
1 <= len (f^<*q*>) by Th10;
then |- Ant(f^<*q*>)^<*p 'or' q*> by A1,A5,Th45;
hence thesis by Th5;
end;
theorem Th52:
|- f^<*p*>^<*r*> & |- f^<*q*>^<*r*> implies |- f^<*p 'or' q*>^<* r*>
proof
set f1 = f^<*'not' r*>^<*'not' p*>;
set f2 = f^<*'not' r*>^<*'not' q*>;
A1: Ant(f1) = f^<*'not' r*> by Th5;
A2: Suc(f2) = 'not' q by Th5;
assume |- f^<*p*>^<*r*> & |- f^<*q*>^<*r*>;
then
A3: |- f^<*'not' r*>^<*'not' p*> & |- f^<*'not' r*>^<*'not' q*> by Th46;
Suc(f1) = 'not' p & Ant(f2) = f^<*'not' r*> by Th5;
then |- Ant(f1)^<*'not' p '&' 'not' q*> by A3,A2,Th5,Th39;
then |- f^<*'not' ('not' p '&' 'not' q)*>^<*r*> by A1,Th48;
hence thesis by QC_LANG2:def 3;
end;
theorem Th53:
|- f^<*p*> implies |- f^<*'not' 'not' p*>
proof
assume
A1: |- f^<*p*>;
set f5 = f^<*p*>;
set f4 = f^<*p*>^<*'not' 'not' p*>^<*'not' 'not' p*>;
set f2 = f^<*p*>^<*'not' p*>^<*'not' p*>;
set f1 = f^<*p*>^<*'not' p*>^<*p*>;
set f3 = Ant(f1)^<*'not' 'not' p*>;
A2: Suc(f1) = p by Th5;
A3: Ant(f1) = f^<*p*>^<*'not' p*> by Th5;
then
A4: 1 < len f3 by Th9;
A5: Ant(f4) = f^<*p*>^<*'not' 'not' p*> by Th5;
then Ant(f4) = f^(<*p*>^<*'not' 'not' p*>) by FINSEQ_1:32;
then
A6: Ant(f4) = f^<*p,'not' 'not' p *> by FINSEQ_1:def 9;
A7: Ant(f3) = Ant(f1) by Th5;
then Suc(Ant(f3)) = 'not' p by A3,Th5;
then
A8: 'not' Suc(Ant(f3)) = Suc(Ant(f4)) by A5,Th5;
Ant(f1) = f^(<*p*>^<*'not' p*>) by A3,FINSEQ_1:32;
then
A9: Ant(f1) = f^<*p,'not' p *> by FINSEQ_1:def 9;
len f+2 = len f + len <*p,'not' p *> by FINSEQ_1:44;
then len f+2 = len Ant(f1) by A9,FINSEQ_1:22;
then 1 <= len f+1 & len f+1 <= len Ant(f1) by NAT_1:11,XREAL_1:6;
then
A10: len f+1 in dom Ant(f1) by FINSEQ_3:25;
(Ant(f1)).(len f+1) = p by A9,Th14;
then
A11: |- f1 by A2,A10,Lm2,Th33;
A12: 1 < len f4 by Th9;
0+1 <= len f2 by Th10;
then
A13: f2 = Ant(f2)^<*Suc(f2)*> by Th3;
A14: 1 <= len f5 by Th10;
len f+2 = len f + len <*p,'not' 'not' p *> by FINSEQ_1:44;
then len f+2 = len Ant(f4) by A6,FINSEQ_1:22;
then
A15: len f+2 in dom Ant(f4) by A5,Th10;
A16: Ant(f2) = f^<*p*>^<*'not' p*> by Th5;
then Ant(f2) = f^(<*p*>^<*'not' p*>) by FINSEQ_1:32;
then
A17: Ant(f2) = f^<*p,'not' p *> by FINSEQ_1:def 9;
len f+2 = len f + len <*p,'not' p *> by FINSEQ_1:44;
then len f+2 = len Ant(f2) by A17,FINSEQ_1:22;
then
A18: len f+2 in dom Ant(f2) by A16,Th10;
A19: Suc(f2) = 'not' p by Th5;
then
A20: 'not' Suc(f1) = Suc(f2) by Th5;
(Ant(f2)).(len f+2) = 'not' p by A17,Th14;
then
A21: |- f2 by A18,A19,Lm2,Th33;
A22: Suc(f4) = 'not' 'not' p by Th5;
then
A23: Suc(f3) = Suc(f4) by Th5;
(Ant(f4)).(len f+2) = 'not' 'not' p by A6,Th14;
then
A24: |- f4 by A15,A22,Lm2,Th33;
Ant(f1) = Ant(f2) by A16,Th5;
then
A25: |- Ant(f1)^<*'not' 'not' p*> by A11,A21,A13,A20,Th44;
A26: Ant(Ant(f3)) = f^<*p*> by A3,A7,Th5;
then Ant(Ant(f3)) = Ant(Ant(f4)) by A5,Th5;
then |- f^<*p*>^<*'not' 'not' p*> by A25,A22,A24,A23,A26,A8,A4,A12,Th37;
then |- Ant(f5)^<*'not' 'not' p*> by A1,A14,Th45;
hence thesis by Th5;
end;
theorem Th54:
|- f^<*'not' 'not' p*> implies |- f^<*p*>
proof
assume
A1: |- f^<*'not' 'not' p*>;
set f5 = f^<*'not' 'not' p*>;
set f4 = f^<*'not' 'not' p*>^<*p*>^<*p*>;
set f2 = f^<*'not' 'not' p*>^<*'not' p*>^<*'not' 'not' p*>;
set f1 = f^<*'not' 'not' p*>^<*'not' p*>^<*'not' p*>;
set f3 = Ant(f1)^<*p*>;
A2: Suc(f1) = 'not' p by Th5;
A3: Ant(f1) = f^<*'not' 'not' p*>^<*'not' p*> by Th5;
then
A4: 1 < len f3 by Th9;
Ant(f1) = f^(<*'not' 'not' p*>^<*'not' p*>) by A3,FINSEQ_1:32;
then
A5: Ant(f1) = f^<*'not' 'not' p,'not' p *> by FINSEQ_1:def 9;
len f+2 = len f + len <*'not' 'not' p,'not' p *> by FINSEQ_1:44;
then len f+2 = len Ant(f1) by A5,FINSEQ_1:22;
then
A6: len f+2 in dom Ant(f1) by A3,Th10;
(Ant(f1)).(len f+2) = 'not' p by A5,Th14;
then
A7: |- f1 by A2,A6,Lm2,Th33;
A8: 1 < len f4 by Th9;
A9: Ant(f2) = f^<*'not' 'not' p*>^<*'not' p*> by Th5;
then Ant(f2) = f^(<*'not' 'not' p*>^<*'not' p*>) by FINSEQ_1:32;
then
A10: Ant(f2) = f^<*'not' 'not' p,'not' p *> by FINSEQ_1:def 9;
len f+2 = len f + len <*'not' 'not' p,'not' p *> by FINSEQ_1:44;
then len f+2 = len Ant(f2) by A10,FINSEQ_1:22;
then 1 <= len f+1 & len f+1 <= len Ant(f2) by NAT_1:11,XREAL_1:6;
then
A11: len f+1 in dom Ant(f2) by FINSEQ_3:25;
0+1 <= len f2 by Th10;
then
A12: f2 = Ant(f2)^<*Suc(f2)*> by Th3;
A13: 1 <= len f5 by Th10;
A14: Ant(f4) = f^<*'not' 'not' p*>^<*p*> by Th5;
then Ant(f4) = f^(<*'not' 'not' p*>^<*p*>) by FINSEQ_1:32;
then
A15: Ant(f4) = f^<*'not' 'not' p,p *> by FINSEQ_1:def 9;
A16: Ant(f3) = Ant(f1) by Th5;
then Suc(Ant(f3)) = 'not' p by A3,Th5;
then
A17: Suc(Ant(f3)) = 'not' Suc(Ant(f4)) by A14,Th5;
len f+2 = len f + len <*'not' 'not' p,p *> by FINSEQ_1:44;
then len f+2 = len Ant(f4) by A15,FINSEQ_1:22;
then
A18: len f+2 in dom Ant(f4) by A14,Th10;
A19: Suc(f2) = 'not' 'not' p by Th5;
then
A20: 'not' Suc(f1) = Suc(f2) by Th5;
(Ant(f2)).(len f+1) = 'not' 'not' p by A10,Th14;
then
A21: |- f2 by A11,A19,Lm2,Th33;
A22: Suc(f4) = p by Th5;
then
A23: Suc(f3) = Suc(f4) by Th5;
(Ant(f4)).(len f+2) = p by A15,Th14;
then
A24: |- f4 by A18,A22,Lm2,Th33;
Ant(f1) = Ant(f2) by A9,Th5;
then
A25: |- Ant(f1)^<*p*> by A7,A21,A12,A20,Th44;
A26: Ant(Ant(f3)) = f^<*'not' 'not' p*> by A3,A16,Th5;
then Ant(Ant(f3)) = Ant(Ant(f4)) by A14,Th5;
then |- f^<*'not' 'not' p*>^<*p*> by A25,A22,A24,A23,A26,A17,A4,A8,Th37;
then |- Ant(f5)^<*p*> by A1,A13,Th45;
hence thesis by Th5;
end;
theorem
|- f^<*p => q*> & |- f^<*p*> implies |- f^<*q*>
proof
assume that
A1: |- f^<*p => q*> and
A2: |- f^<*p*>;
set f3 = f^<*q*>^<*q*>;
set f2 = f^<*'not' p*>^<*'not' p*>;
set f1 = f^<*'not' p*>^<*p*>;
A3: Ant(f1) = f^<*'not' p*> by Th5;
Suc(f^<*p*>) = p by Th5;
then
A4: Suc(f^<*p*>) = Suc(f1) by Th5;
A5: 0+1 <= len f2 by Th10;
A6: Ant(f3) = f^<*q*> by Th5;
then
A7: (Ant(f3)).(len f+1) = q by FINSEQ_1:42;
len f+1 = len f + len <*q*> by FINSEQ_1:39;
then len f+1 = len Ant(f3) by A6,FINSEQ_1:22;
then
A8: len f+1 in dom Ant(f3) by A6,Th10;
Suc(f3) = q by Th5;
then
A9: |- f3 by A7,A8,Lm2,Th33;
A10: Ant(f2) = f^<*'not' p*> by Th5;
len f+1 = len f + len <*'not' p *> by FINSEQ_1:39;
then len f+1 = len Ant(f2) by A10,FINSEQ_1:22;
then
A11: len f+1 in dom Ant(f2) by A10,Th10;
A12: Suc(f2) = 'not' p by Th5;
then
A13: 'not' Suc(f1) = Suc(f2) by Th5;
(Ant(f2)).(len f+1) = 'not' p by A10,FINSEQ_1:42;
then
A14: |- f2 by A11,A12,Lm2,Th33;
Ant(f1) = Ant(f2) by A10,Th5;
then
A15: |- Ant(f1)^<*'not' Suc(f1)*> by A14,A5,A13,Th3;
Ant(f^<*p*>) = f by Th5;
then |- f1 by A2,A3,A4,Th8,Th36;
then |- Ant(f1)^<*q*> by A15,Th44;
then |- f^<*'not' p 'or' q*>^<*q*> by A3,A9,Th52;
then
A16: |- f^<*'not' ('not' 'not' p '&' 'not' q)*>^<*q*> by QC_LANG2:def 3;
set f4 = f^<*'not' q*>^<*'not' 'not' p '&' 'not' q*>;
set f5 = Ant(f4)^<*p*>;
set f6 = Ant(f4)^<*'not' q*>;
A17: Ant(f5) = Ant(f4) & Suc(f5) = p by Th5;
A18: Ant(f6) = Ant(f4) & Suc(f6) = 'not' q by Th5;
A19: Suc(f4) = 'not' 'not' p '&' 'not' q by Th5;
then |- Ant(f4)^<*'not' 'not' p*> by A16,Th40,Th48;
then
A20: |- Ant(f4)^<*p*> by Th54;
|- Ant(f4)^<*'not' q*> by A16,A19,Th41,Th48;
then |- Ant(f4)^<*p '&' 'not' q*> by A20,A17,A18,Th39;
then |- f^<*'not' q*>^<*p '&' 'not' q*> by Th5;
then |- f^<*'not' (p '&' 'not' q)*>^<*q*> by Th48;
then
A21: |- f^<*p => q*>^<*q*> by QC_LANG2:def 2;
1 <= len (f^<*p => q*>) by Th10;
then |- Ant(f^<*p => q*>)^<*q*> by A1,A21,Th45;
hence thesis by Th5;
end;
theorem Th56:
('not' p).(x,y) = 'not' (p.(x,y))
proof
set S = [p,Sbst(x,y)];
S`1 = p & S`2 = Sbst(x,y);
then ('not' p).(x,y) = CQC_Sub(['not' p,Sbst(x,y)]) & Sub_not S = ['not' p,
Sbst(x,y)] by SUBSTUT1:def 20,SUBSTUT2:def 1;
then ('not' p).(x,y) = 'not' CQC_Sub(S) by SUBSTUT1:29;
hence thesis by SUBSTUT2:def 1;
end;
theorem
(ex y st |- f^<*p.(x,y)*>) implies |- f^<*Ex(x,p)*>
proof
given y such that
A1: |- f^<*p.(x,y)*>;
set f1 = f^<*All(x,'not' p)*>^<*All(x,'not' p)*>;
A2: Ant(f1) = f^<*All(x,'not' p)*> by Th5;
len f+1 = len f + len <*All(x,'not' p)*> by FINSEQ_1:39;
then len f+1 = len Ant(f1) by A2,FINSEQ_1:22;
then
A3: len f+1 in dom Ant(f1) by A2,Th10;
A4: Suc(f1) = All(x,'not' p) by Th5;
(Ant(f1)).(len f+1) = All(x,'not' p) by A2,FINSEQ_1:42;
then Suc(f1) is_tail_of Ant(f1) by A4,A3,Lm2;
then |- f^<*All(x,'not' p)*>^<*('not' p).(x,y)*> by A2,A4,Th33,Th42;
then |- f^<*All(x,'not' p)*>^<*'not' (p.(x,y))*> by Th56;
then |- f^<*p.(x,y)*>^<*'not' All(x,'not' p)*> by Th49;
then
A5: |- f^<*p.(x,y)*>^<*Ex(x,p)*> by QC_LANG2:def 5;
1 <= len (f^<*p.(x,y)*>) by Th10;
then |- Ant(f^<*p.(x,y)*>)^<*Ex(x,p)*> by A1,A5,Th45;
hence thesis by Th5;
end;
theorem Th58:
still_not-bound_in (f^g) = still_not-bound_in f \/ still_not-bound_in g
proof
thus still_not-bound_in (f^g) c= still_not-bound_in f \/ still_not-bound_in g
proof
let b be object;
assume b in still_not-bound_in (f^g);
then consider i,p such that
A1: i in dom (f^g) and
A2: p = (f^g).i & b in still_not-bound_in p by Def5;
A3: now
given n being Nat such that
A4: n in dom g and
A5: i = len f + n;
(f^g).i = g.n by A4,A5,FINSEQ_1:def 7;
then
A6: b in still_not-bound_in g by A2,A4,Def5;
still_not-bound_in g c= still_not-bound_in f \/ still_not-bound_in
g by XBOOLE_1:7;
hence thesis by A6;
end;
now
assume
A7: i in dom f;
then (f^g).i = f.i by FINSEQ_1:def 7;
then
A8: b in still_not-bound_in f by A2,A7,Def5;
still_not-bound_in f c= still_not-bound_in f \/ still_not-bound_in g
by XBOOLE_1:7;
hence thesis by A8;
end;
hence thesis by A1,A3,FINSEQ_1:25;
end;
thus still_not-bound_in f \/ still_not-bound_in g c= still_not-bound_in (f^g
)
proof
let b be object such that
A9: b in still_not-bound_in f \/ still_not-bound_in g;
A10: now
assume b in still_not-bound_in g;
then consider i,p such that
A11: i in dom g & p = g.i and
A12: b in still_not-bound_in p by Def5;
len f + i in dom (f^g) & p = (f^g).(len f + i) by A11,FINSEQ_1:28,def 7;
hence thesis by A12,Def5;
end;
now
assume b in still_not-bound_in f;
then consider i,p such that
A13: i in dom f and
A14: p = f.i and
A15: b in still_not-bound_in p by Def5;
dom f c= dom (f^g) & p = (f^g).i by A13,A14,FINSEQ_1:26,def 7;
hence thesis by A13,A15,Def5;
end;
hence thesis by A9,A10,XBOOLE_0:def 3;
end;
end;
theorem Th59:
still_not-bound_in <*p*> = still_not-bound_in p
proof
A1: now
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A2: 1 in dom <*p*> by FINSEQ_1:38;
A3: p = <*p*>.1;
let b be object;
assume b in still_not-bound_in p;
hence b in still_not-bound_in <*p*> by A2,A3,Def5;
end;
now
let b be object;
assume b in still_not-bound_in <*p*>;
then consider i,q such that
A4: i in dom <*p*> and
A5: q = <*p*>.i & b in still_not-bound_in q by Def5;
i in Seg 1 by A4,FINSEQ_1:38;
then i = 1 by FINSEQ_1:2,TARSKI:def 1;
hence b in still_not-bound_in p by A5;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
|- f^<*p.(x,y)*>^<*q*> & not y in still_not-bound_in (f^<*Ex(x,p)*>^<*
q*>) implies |- f^<*Ex(x,p)*>^<*q*>
proof
assume that
A1: |- f^<*p.(x,y)*>^<*q*> and
A2: not y in still_not-bound_in (f^<*Ex(x,p)*>^<*q*>);
set f1 = f^<*'not' q*>^<*('not' p).(x,y)*>;
|- f^<*'not' q*>^<*'not' (p.(x,y))*> by A1,Th46;
then
A3: |- f^<*'not' q*>^<*('not' p).(x,y)*> by Th56;
A4: not y in still_not-bound_in (f^<*Ex(x,p)*>) \/ still_not-bound_in <*q*>
by A2,Th58;
then not y in still_not-bound_in (f^<*Ex(x,p)*>) by XBOOLE_0:def 3;
then
A5: not y in still_not-bound_in f \/ still_not-bound_in <*Ex(x,p)*> by Th58;
then not y in still_not-bound_in <*Ex(x,p)*> by XBOOLE_0:def 3;
then not y in still_not-bound_in Ex(x,p) by Th59;
then not y in still_not-bound_in p \ {x} by QC_LANG3:19;
then not y in still_not-bound_in 'not' p \ {x} by QC_LANG3:7;
then
A6: not y in still_not-bound_in All(x,'not' p) by QC_LANG3:12;
not y in still_not-bound_in <*q*> by A4,XBOOLE_0:def 3;
then not y in still_not-bound_in q by Th59;
then not y in still_not-bound_in 'not' q by QC_LANG3:7;
then
A7: not y in still_not-bound_in <*'not' q*> by Th59;
not y in still_not-bound_in f by A5,XBOOLE_0:def 3;
then not y in still_not-bound_in f \/ still_not-bound_in <*'not' q*> by A7,
XBOOLE_0:def 3;
then not y in still_not-bound_in (f^<*'not' q*>) by Th58;
then
A8: not y in still_not-bound_in Ant(f1) by Th5;
Suc(f1) = ('not' p).(x,y) by Th5;
then |- Ant(f1)^<*All(x,'not' p)*> by A3,A8,A6,Th43;
then |- f^<*'not' q*>^<*All(x,'not' p)*> by Th5;
then |- f^<*'not' All(x,'not' p)*>^<*q*> by Th48;
hence thesis by QC_LANG2:def 5;
end;
theorem Th61:
still_not-bound_in f = union {still_not-bound_in p : ex i st i
in dom f & p = f.i}
proof
defpred P[set] means ex p st $1 = still_not-bound_in p & ex i st i in dom f
& p = f.i;
set X = {still_not-bound_in p : ex i st i in dom f & p = f.i};
A1: now
let b be object;
assume b in union X;
then consider Y being set such that
A2: b in Y and
A3: Y in X by TARSKI:def 4;
P[Y] by A3;
hence b in still_not-bound_in f by A2,Def5;
end;
now
let b be object;
assume b in still_not-bound_in f;
then consider i,p such that
A4: i in dom f & p = f.i and
A5: b in still_not-bound_in p by Def5;
still_not-bound_in p in X by A4;
hence b in union X by A5,TARSKI:def 4;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th62:
still_not-bound_in f is finite
proof
defpred P[object,object] means
ex p st $2 = still_not-bound_in p & p = f.$1;
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
set X = {still_not-bound_in p : ex i st i in dom f & p = f.i};
consider F1 being Function such that
A2: rng F1 = Seg n and
A3: dom F1 in omega by FINSET_1:def 1;
A4: now
let b be set;
assume b in X;
then ex p st b = still_not-bound_in p & ex i st i in dom f & p = f.i;
hence b is finite by CQC_SIM1:19;
end;
A5: for a being object st a in dom f ex b being object st P[a,b]
proof
let a be object;
assume a in dom f;
then f.a in rng f by FUNCT_1:3;
then reconsider p = f.a as Element of CQC-WFF(Al);
take still_not-bound_in p;
thus thesis;
end;
consider F2 being Function such that
A6: dom F2 = dom f &
for b being object st b in dom f holds P[b,F2.b] from CLASSES1:
sch 1(A5);
set F = F2*F1;
A7: now
let b be object;
assume b in X;
then consider p such that
A8: b = still_not-bound_in p and
A9: ex i st i in dom f & p = f.i;
consider i such that
A10: i in dom f and
A11: p = f.i by A9;
P[i,F2.i] by A6,A10;
then b in rng F2 by A6,A8,A10,A11,FUNCT_1:3;
hence b in rng F by A6,A1,A2,RELAT_1:28;
end;
now
let b be object;
assume b in rng F;
then b in rng F2 by A6,A1,A2,RELAT_1:28;
then consider a being object such that
A12: a in dom F2 and
A13: b = F2.a by FUNCT_1:def 3;
reconsider a as Element of NAT by A6,A12;
P[a,F2.a] by A6,A12;
hence b in X by A6,A12,A13;
end;
then
A14: rng F = X by A7,TARSKI:2;
dom F in omega by A6,A1,A2,A3,RELAT_1:27;
then X is finite by A14,FINSET_1:def 1;
then union X is finite by A4,FINSET_1:7;
hence thesis by Th61;
end;
theorem Th63:
card bound_QC-variables(Al) = card QC-symbols(Al) &
not bound_QC-variables(Al) is finite
proof
NAT c= QC-symbols(Al) by QC_LANG1:3;
then
A1: not QC-symbols(Al) is finite;
bound_QC-variables(Al) = [: {4}, QC-symbols(Al) :] by QC_LANG1:def 4;
then card bound_QC-variables(Al) = card [:QC-symbols(Al),{4}:] by CARD_2:4;
hence thesis by A1,CARD_4:19;
end;
theorem Th64:
ex x st not x in still_not-bound_in f
proof
still_not-bound_in f is finite by Th62;
then still_not-bound_in f <> bound_QC-variables(Al) by Th63;
then
not ( for b being object holds b in still_not-bound_in f iff
b in bound_QC-variables(Al)) by TARSKI:2;
then consider b such that
A1: not b in still_not-bound_in f and
A2: b in bound_QC-variables(Al);
reconsider x = b as bound_QC-variable of Al by A2;
take x;
thus thesis by A1;
end;
theorem Th65:
|- f^<*All(x,p)*> implies |- f^<*All(x,'not' 'not' p)*>
proof
assume
A1: |- f^<*All(x,p)*>;
consider y0 such that
A2: not y0 in still_not-bound_in (f^<*All(x,p)*>) by Th64;
Ant(f^<*All(x,p)*>) = f & Suc(f^<*All(x,p)*>) = All(x,p) by Th5;
then |- f^<*p.(x,y0)*> by A1,Th42;
then |- f^<*'not' 'not' (p.(x,y0))*> by Th53;
then |- f^<*'not' (('not' p).(x,y0))*> by Th56;
then
A3: |- f^<*('not' 'not' p).(x,y0)*> by Th56;
set f1 = f^<*('not' 'not' p).(x,y0)*>;
A4: not y0 in still_not-bound_in f \/ still_not-bound_in <*All(x,p)*> by A2
,Th58;
then not y0 in still_not-bound_in f by XBOOLE_0:def 3;
then
A5: not y0 in still_not-bound_in Ant(f1) by Th5;
not y0 in still_not-bound_in <*All(x,p)*> by A4,XBOOLE_0:def 3;
then not y0 in still_not-bound_in All(x,p) by Th59;
then not y0 in still_not-bound_in p \ {x} by QC_LANG3:12;
then not y0 in still_not-bound_in 'not' p \ {x} by QC_LANG3:7;
then not y0 in still_not-bound_in 'not' 'not' p \ {x} by QC_LANG3:7;
then
A6: not y0 in still_not-bound_in All(x,'not' 'not' p) by QC_LANG3:12;
Suc(f1) = ('not' 'not' p).(x, y0) by Th5;
then |- Ant(f1)^<* All(x,'not' 'not' p)*> by A3,A5,A6,Th43;
hence thesis by Th5;
end;
theorem Th66:
|- f^<*All(x,'not' 'not' p)*> implies |- f^<*All(x,p)*>
proof
assume
A1: |- f^<*All(x,'not' 'not' p)*>;
consider y0 such that
A2: not y0 in still_not-bound_in (f^<*All(x,p)*>) by Th64;
Ant(f^<*All(x,'not' 'not' p)*>) = f & Suc(f^<*All(x,'not' 'not' p)*>) =
All( x,'not' 'not' p) by Th5;
then |- f^<*('not' 'not' p).(x,y0)*> by A1,Th42;
then |- f^<*'not' (('not' p).(x,y0))*> by Th56;
then
A3: |- f^<*'not' 'not' (p.(x,y0))*> by Th56;
set f1 = f^<*p.(x,y0)*>;
A4: not y0 in still_not-bound_in f \/ still_not-bound_in <*All(x,p)*> by A2
,Th58;
then not y0 in still_not-bound_in f by XBOOLE_0:def 3;
then
A5: not y0 in still_not-bound_in Ant(f1) by Th5;
not y0 in still_not-bound_in <*All(x,p)*> by A4,XBOOLE_0:def 3;
then
A6: not y0 in still_not-bound_in All(x,p) by Th59;
Suc(f1) = p.(x,y0) by Th5;
then |- Ant(f1)^<* All(x,p)*> by A3,A5,A6,Th43,Th54;
hence thesis by Th5;
end;
theorem
|- f^<*All(x,p)*> iff |- f^<*'not' Ex(x,'not' p)*>
proof
thus |- f^<*All(x,p)*> implies |- f^<*'not' Ex(x,'not' p)*>
proof
assume |- f^<*All(x,p)*>;
then |- f^<*All(x,'not' 'not' p)*> by Th65;
then |- f^<*'not' 'not' All(x,'not' 'not' p)*> by Th53;
hence thesis by QC_LANG2:def 5;
end;
assume |- f^<*'not' Ex(x,'not' p)*>;
then |- f^<*'not' 'not' All(x,'not' 'not' p)*> by QC_LANG2:def 5;
then |- f^<*All(x,'not' 'not' p)*> by Th54;
hence thesis by Th66;
end;
definition
let f be FinSequence, p be set;
redefine pred p is_tail_of f means :: redefines is_tail_of (CALCUL_1, definition)
ex i being Nat st i in dom f & f.i = p;
compatibility by Lm1,Lm2;
end;