:: Representation Theorem for Stacks
:: by Grzegorz Bancerek
::
:: Received February 22, 2011
:: Copyright (c) 2011 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 STACKS_1, XBOOLE_0, STRUCT_0, ZFMISC_1, SUBSET_1, FUNCT_1,
NUMBERS, NAT_1, TARSKI, ARYTM_3, RELAT_1, FINSEQ_1, FINSEQ_3, ORDINAL4,
FUNCOP_1, PARTFUN1, CARD_1, XXREAL_0, COMPLEX1, GLIB_000, RELAT_2,
EQREL_1, FILTER_1, BINOP_1, MCART_1, ORDERS_1, WELLORD1, ARYTM_1,
SETFAM_1, FUNCT_2, AOFA_000, PBOOLE, FUNCT_4, MATRIX_7, REWRITE1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELAT_2, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCT_3,
FUNCOP_1, ORDERS_1, FUNCT_4, NUMBERS, XXREAL_0, NAT_1, NAT_D, FINSEQ_1,
FINSEQ_2, EQREL_1, FINSEQ_3, PBOOLE, FUNCT_7, STRUCT_0, FILTER_1,
REWRITE1, ABCMIZ_1, AOFA_000;
constructors BINOP_1, DOMAIN_1, XXREAL_0, RELSET_1, FILTER_1, FUNCT_7,
REWRITE1, ABCMIZ_1, POLYNOM3, NAT_D;
registrations XBOOLE_0, RELSET_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1,
PARTFUN1, FUNCT_2, NAT_1, ORDINAL1, XXREAL_0, XREAL_0, CARD_1, EQREL_1,
SUBSET_1, REWRITE1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, RELAT_2, PARTFUN1, FUNCT_2,
FINSEQ_1, BINOP_1, FILTER_1, REWRITE1;
theorems TARSKI, XBOOLE_1, FINSEQ_1, FINSEQ_3, FINSEQ_5, NAT_1, NAT_D,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3, FUNCOP_1, WSIERP_1, BINOP_1,
POLYALG1, EQREL_1, WELLORD2, RELSET_1, ORDINAL1, XREAL_1, NAT_2,
ZFMISC_1, SETFAM_1, RELAT_1, XBOOLE_0, ORDERS_1, MATRIX_7, FUNCT_7,
FILTER_1, FUNCT_4, REWRITE1, XXREAL_0, MSUALG_8, HILBERT2, RLVECT_3,
FINSEQOP, FINSEQ_2;
schemes XBOOLE_0, RELSET_1, NAT_1, FUNCT_2, BINOP_1, RECDEF_1, ALTCAT_1,
WELLORD2, FINSEQ_1, FINSEQ_2;
begin :: Preliminaries
reserve i,j for Nat;
reserve x,y for set;
definition
let A be set;
let s1,s2 be FinSequence of A;
redefine func s1^s2 -> Element of A*;
coherence
proof
s1^s2 is FinSequence of A;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
let A be set;
let i be Nat;
let s be FinSequence of A;
redefine func Del(s,i) -> Element of A*;
coherence
proof
rng Del(s,i) c= rng s & rng s c= A by FINSEQ_3:115; then
rng Del(s,i) c= A by XBOOLE_1:1; then
Del(s,i) is FinSequence of A by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
end;
theorem Lem1:
Del({},i) = {}
proof
dom Del({},i) c= dom {} by WSIERP_1:47;
hence thesis;
end;
theorem FINSEQp2150:
for D being non empty set
for s being FinSequence of D st s <> {}
ex w being FinSequence of D, n being Element of D st s = <*n*>^w
proof
let D be non empty set;
let s be FinSequence of D;
defpred P[FinSequence] means $1 <> {} implies
ex w being FinSequence of D, n being Element of D st $1 = <*n*>^w;
A1: for s being FinSequence of D
for m being Element of D st P[s] holds P[s^<*m*>]
proof
let s be FinSequence of D;
let m be Element of D such that
A2: s <> {} implies
ex w being FinSequence of D, n being Element of D st s = <*n*>^w;
assume s^<*m*> <> {};
per cases;
suppose
A3: s = {};
reconsider w = <*> D as FinSequence of D;
take w, n = m;
thus s^<*m*> = <*m*> by A3,FINSEQ_1:47
.= <*n*>^w by FINSEQ_1:47;
end;
suppose
s <> {};
then consider w being FinSequence of D, n being Element of D such that
A4: s = <*n*>^w by A2;
take w^<*m*>,n;
thus thesis by A4,FINSEQ_1:45;
end;
end;
A5: P[<*> D];
for p being FinSequence of D holds P[p] from FINSEQ_2:sch 2(A5,A1);
hence thesis;
end;
scheme IndSeqD{D()->non empty set, P[set]}:
for p being FinSequence of D() holds P[p]
provided
A1: P[<*> D()] and
A2: for p being FinSequence of D() for x being Element of D() st P[p]
holds P[<*x*>^p]
proof
defpred R[set] means
for p being FinSequence of D() st len p = $1 holds P[p];
A3: for i st R[i] holds R[i+1]
proof
let i such that
A4: for p being FinSequence of D() st len p = i holds P[p];
let p be FinSequence of D();
assume
A5: len p = i + 1;
then p <> {}; then
consider q being FinSequence of D(), x being Element of D() such that
A6: p = <*x*>^q by FINSEQp2150;
len p = len q + 1 by A6,FINSEQ_5:8;
hence thesis by A2,A4,A5,A6;
end;
let p be FinSequence of D();
A7: len p = len p;
A8: R[0]
proof let p be FinSequence of D();
assume len p = 0;
then p = <*>D();
hence thesis by A1;
end;
for i holds R[i] from NAT_1:sch 2(A8,A3);
hence thesis by A7;
end;
definition
let C,D be non empty set;
let R be Relation;
mode BinOp of C,D,R -> Function of [:C,D:],D means:
Def2:
for x being Element of C,y1,y2 being Element of D
st [y1,y2] in R holds [it.(x,y1),it.(x,y2)] in R;
existence
proof
take f = pr2(C,D);
let x be Element of C,y1,y2 be Element of D;
f.(x,y1) = y1 by FUNCT_3:def 6;
hence thesis by FUNCT_3:def 6;
end;
end;
scheme LambdaD2{ A,B,C() -> non empty set, F(set,set) -> Element of C() }:
ex M being Function of [:A(),B():],C() st
for i being Element of A(), j being Element of B() holds M.(i,j) = F(i,j)
proof
consider M being ManySortedSet of [:A(),B():] such that
A1: for i being Element of A(), j being Element of B() holds M.(i,j) = F(i,j)
from ALTCAT_1:sch 2;
A2: dom M = [:A(),B():] by PARTFUN1:def 4;
rng M c= C()
proof let y; assume y in rng M; then
consider x such that
A3: x in dom M & y = M.x by FUNCT_1:def 5;
consider x1,x2 being set such that
A4: x1 in A() & x2 in B() & x = [x1,x2] by A2,A3,ZFMISC_1:def 2;
y = M.(x1,x2) by A3,A4 .= F(x1,x2) by A1,A4;
hence thesis;
end; then
reconsider M as Function of [:A(),B():],C() by A2,FUNCT_2:4;
take M; thus thesis by A1;
end;
definition
let C,D be non empty set;
let R be Equivalence_Relation of D;
let b be Function of [:C,D:],D;
assume
A1: b is BinOp of C,D,R;
func b /\/ R -> Function of [:C, Class R:], Class R means
:Def4:
for x,y,y1 be set st x in C & y in Class R & y1 in y
holds it.(x,y) = Class(R,b.(x,y1));
existence
proof
now
let X be set;
assume X in Class R;
then ex x being set st x in D & X = Class(R,x) by EQREL_1:def 5;
hence X <> {} by EQREL_1:28;
end;
then consider g being Function such that
A2: dom g = Class R and
A3: for X being set st X in Class R holds g.X in X by WELLORD2:28;
A4: rng g c= D
proof
let x be set;
assume x in rng g;
then consider y being set such that
A5: y in dom g and
A6: x = g.y by FUNCT_1:def 5;
x in y by A2,A3,A5,A6;
hence thesis by A2,A5;
end;
deffunc F(Element of D) = EqClass(R,$1);
consider f being Function of D, Class R such that
A7: for x being Element of D holds f.x = F(x) from FUNCT_2:sch 4;
reconsider g as Function of Class R, D by A2,A4,FUNCT_2:def 1,RELSET_1:11;
deffunc F(Element of C,Element of Class R) = f.(b.($1,g.$2));
consider bR being Function of [:C, Class R:], Class R such that
A8: for x being Element of C,y being Element of Class R holds bR.(x,y) = F(x,y)
from LambdaD2;
take bR;
let x,y,y1 be set;
assume that
A9: x in C and
A10: y in Class R and
A12: y1 in y;
reconsider x9 = x as Element of C by A9;
reconsider y9 = y as Element of Class R by A10;
reconsider y19 = y1 as Element of D by A10,A12;
A13: ex y2 being set st y2 in D & y9 = Class(R,y2) by EQREL_1:def 5;
g.y9 in y by A3;
then [g.y9,y19] in R by A12,A13,EQREL_1:30;
then [b.(x9,g.y9),b.(x9,y19)] in R by A1,Def2;
then
A16: b.(x9,g.y9) in EqClass(R,b.(x9,y19)) by EQREL_1:27;
A17: f.(b.(x9,g.y9)) = EqClass(R,b.(x9,g.y9)) by A7;
bR.(x9,y9) = f.(b.(x9,g.y9)) by A8;
hence thesis by A16,A17,EQREL_1:31;
end;
uniqueness
proof
let b1,b2 be Function of [:C, Class R:], Class R such that
A18: for x,y,y1 being set st x in C & y in Class R & y1 in y
holds b1.(x,y) = Class(R,b.(x,y1)) and
A19: for x,y,y1 being set st x in C & y in Class R & y1 in y
holds b2.(x,y) = Class(R,b.(x,y1));
now
let x be Element of C,y be Element of Class R;
consider y1 being set such that
A22: y1 in D and
A23: y = Class(R,y1) by EQREL_1:def 5;
b1.(x,y) = Class(R,b.(x,y1)) by A18,A22,A23,EQREL_1:28;
hence b1.(x,y) = b2.(x,y) by A19,A22,A23,EQREL_1:28;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let A,B be non empty set;
let C be Subset of A;
let D be Subset of B;
let f be Function of A,B;
let g be Function of C,D;
redefine func f+*g -> Function of A,B;
coherence
proof per cases;
suppose D = {}; then
g = {};
hence thesis by FUNCT_4:22;
end;
suppose
A0: D <> {};
A1: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
.= A \/ dom g by FUNCT_2:def 1
.= A \/ C by A0,FUNCT_2:def 1 .= A by XBOOLE_1:12;
A2: rng(f+*g) c= rng f \/ rng g by FUNCT_4:18;
rng f \/ rng g c= B \/ D & B \/ D = B by XBOOLE_1:12,13;
hence thesis by A1,A2,XBOOLE_1:1,FUNCT_2:4;
end;
end;
end;
begin :: Stack Algebra
definition
struct(2-sorted) StackSystem(#
carrier -> set, :: elements
carrier' -> set, :: stacks
s_empty -> Subset of the carrier',
s_push -> Function of [:the carrier, the carrier':], the carrier',
s_pop -> Function of the carrier', the carrier',
s_top -> Function of the carrier', the carrier
#);
end;
registration
let a1 be non empty set, a2 be set, a3 be Subset of a2,
a4 be Function of [:a1, a2:], a2,
a5 be Function of a2, a2,
a6 be Function of a2, a1;
cluster StackSystem(#a1,a2,a3,a4,a5,a6#) -> non empty;
coherence;
end;
registration
let a1 be set, a2 be non empty set, a3 be Subset of a2,
a4 be Function of [:a1, a2:], a2,
a5 be Function of a2, a2,
a6 be Function of a2, a1;
cluster StackSystem(#a1,a2,a3,a4,a5,a6#) -> non void;
coherence;
end;
registration
cluster non empty non void strict StackSystem;
existence
proof
set a1 = the non empty set, a2 = a1;
set a3 = the Subset of a2,
a4 = the Function of [:a1, a2:], a2,
a5 = the Function of a2, a2,
a6 = the Function of a2, a1;
take StackSystem(#a1,a2,a3,a4,a5,a6#);
thus thesis;
end;
end;
definition
let X be StackSystem;
mode stack of X is Element of the carrier' of X;
end;
definition
let X be non empty non void StackSystem;
let s be stack of X;
pred emp s means:
EMP: s in the s_empty of X;
func pop s -> stack of X equals (the s_pop of X).s;
coherence;
func top s -> Element of X equals (the s_top of X).s;
coherence;
let e be Element of X;
func push(e,s) -> stack of X equals (the s_push of X).(e,s);
coherence;
end;
definition
let A be non empty set;
func StandardStackSystem A -> non empty non void strict StackSystem means:
EXAM:
the carrier of it = A &
the carrier' of it = A* &
for s being stack of it holds
(emp s iff s is empty) &
for g being FinSequence st g = s holds
(not emp s implies top s = g.1 & pop s = Del(g,1)) &
(emp s implies top s = the Element of it & pop s = {}) &
for e being Element of it holds
push(e,s) = <*e*>^g;
existence
proof
reconsider s0 = <*>A as Element of A* by FINSEQ_1:def 11;
set E = {s0};
deffunc F(Element of A, Element of A*) = <*$1*>^$2;
deffunc G(Element of A*) = Del($1,1);
deffunc H(Element of A*) = IFEQ($1,{}, the Element of A, $1/.1);
consider psh being Function of [:A,A*:], A* such that
F1: for a being Element of A for s being Element of A* holds psh.(a,s) = F(a,s)
from BINOP_1:sch 4;
consider pp being Function of A*, A* such that
F2: for s being Element of A* holds pp.s = G(s) from FUNCT_2:sch 4;
consider tp being Function of A*, A such that
F3: for s being Element of A* holds tp.s = H(s) from FUNCT_2:sch 4;
take X = StackSystem(#A, A*, E, psh, pp, tp#);
thus the carrier of X = A & the carrier' of X = A*;
let s be stack of X;
emp s iff s in E by EMP;
hence
A0: emp s iff s is empty by TARSKI:def 1;
let g be FinSequence; assume
A1: g = s; then
reconsider h = g as Element of A*;
hereby assume
A5: not emp s; then
A3: 1 in dom h by A0,A1,FINSEQ_5:6;
thus top s = IFEQ(s,{}, the Element of A, h/.1) by F3,A1
.= h/.1 by A0,A5,FUNCOP_1:def 8 .= g.1 by A3,PARTFUN1:def 8;
thus pop s = Del(g,1) by A1,F2;
end;
hereby assume
A4: emp s;
thus top s = IFEQ(s,{}, the Element of A, h/.1) by F3,A1
.= the Element of X by A0,A4,FUNCOP_1:def 8;
thus pop s = Del(g,1) by A1,F2 .= {} by A0,A1,A4,Lem1;
end;
let e be Element of X;
thus push(e,s) = <*e*>^g by F1,A1;
end;
uniqueness
proof let X1,X2 be non empty non void strict StackSystem such that
A1: the carrier of X1 = A and
B1: the carrier' of X1 = A* and
C1: for s being stack of X1 holds
(emp s iff s is empty) &
for g being FinSequence st g = s holds
(not emp s implies top s = g.1 & pop s = Del(g,1)) &
(emp s implies top s = the Element of X1 & pop s = {}) &
for e being Element of X1 holds push(e,s) = <*e*>^g and
A2: the carrier of X2 = A and
B2: the carrier' of X2 = A* and
C2: for s being stack of X2 holds
(emp s iff s is empty) &
for g being FinSequence st g = s holds
(not emp s implies top s = g.1 & pop s = Del(g,1)) &
(emp s implies top s = the Element of X2 & pop s = {}) &
for e being Element of X2 holds push(e,s) = <*e*>^g;
now
let x be Element of A;
reconsider e1 = x as Element of X1 by A1;
reconsider e2 = x as Element of X2 by A2;
let y be Element of A*;
reconsider s1 = y as stack of X1 by B1;
reconsider s2 = y as stack of X2 by B2;
thus (the s_push of X1).(x,y) = push(e1,s1)
.= <*x*>^y by C1
.= push(e2,s2) by C2
.= (the s_push of X2).(x,y);
end; then
A3: the s_push of X1 = the s_push of X2 by A1,B1,A2,B2,BINOP_1:2;
now
let x be Element of A*;
reconsider s1 = x as stack of X1 by B1;
reconsider s2 = x as stack of X2 by B2;
per cases;
suppose
D1: not emp s1; then s1 is non empty by C1; then
D2: not emp s2 by C2;
thus (the s_pop of X1).x = pop s1
.= Del(x,1) by D1,C1
.= pop s2 by D2,C2
.= (the s_pop of X2).x;
end;
suppose
D1: emp s1; then s1 is empty by C1; then
D2: emp s2 by C2;
thus (the s_pop of X1).x = pop s1
.= {} by D1,C1
.= pop s2 by D2,C2
.= (the s_pop of X2).x;
end;
end; then
A4: the s_pop of X1 = the s_pop of X2 by B1,B2,FUNCT_2:113;
K1: now
let x be Element of A*;
reconsider s1 = x as stack of X1 by B1;
reconsider s2 = x as stack of X2 by B2;
per cases;
suppose
D1: not emp s1; then s1 is non empty by C1; then
D2: not emp s2 by C2;
thus (the s_top of X1).x = top s1
.= x.1 by D1,C1
.= top s2 by D2,C2
.= (the s_top of X2).x;
end;
suppose
D1: emp s1; then s1 is empty by C1; then
D2: emp s2 by C2;
thus (the s_top of X1).x = top s1
.= the Element of A by A1,D1,C1
.= top s2 by A2,D2,C2
.= (the s_top of X2).x;
end;
end;
the s_empty of X1 = the s_empty of X2
proof
thus the s_empty of X1 c= the s_empty of X2
proof
let x be set; assume
A6: x in the s_empty of X1; then
reconsider s1 = x as stack of X1;
reconsider s2 = s1 as stack of X2 by B1,B2;
emp s1 by A6,EMP; then
s1 is empty by C1; then
emp s2 by C2;
hence thesis by EMP;
end;
let x be set; assume
A6: x in the s_empty of X2; then
reconsider s2 = x as stack of X2;
reconsider s1 = s2 as stack of X1 by B1,B2;
emp s2 by A6,EMP; then
s2 is empty by C2; then
emp s1 by C1;
hence thesis by EMP;
end;
hence thesis by A1,B1,A2,B2,A3,A4,K1,FUNCT_2:113;
end;
end;
reserve A for non empty set;
reserve c for Element of StandardStackSystem A;
reserve m for stack of StandardStackSystem A;
registration
let A;
cluster -> Relation-like Function-like stack of StandardStackSystem A;
coherence
proof
the carrier' of StandardStackSystem A = A* by EXAM;
hence thesis;
end;
end;
registration
let A;
cluster -> FinSequence-like stack of StandardStackSystem A;
coherence
proof
the carrier' of StandardStackSystem A = A* by EXAM;
hence thesis;
end;
end;
::$H+
emp m iff m = {} by EXAM;
push(c,m) = <*c*>^m by EXAM;
not emp m implies pop m = Del(m,1) by EXAM;
::$H-
reserve X for non empty non void StackSystem;
reserve s,s1,s2 for stack of X;
reserve e,e1,e2 for Element of X;
definition
let X;
attr X is pop-finite means:
POPFIN:
for f being Function of NAT, the carrier' of X
ex i being Nat, s st f.i = s &
(not emp s implies f.(i+1) <> pop s);
attr X is push-pop means:
PUSHPOP:
not emp s implies s = push(top s, pop s);
attr X is top-push means:
TOPPUSH:
e = top push(e,s);
attr X is pop-push means:
POPPUSH:
s = pop push(e,s);
attr X is push-non-empty means:
PUSHNE:
not emp push(e,s);
end;
registration
let A be non empty set;
cluster StandardStackSystem A -> pop-finite;
coherence
proof set X = StandardStackSystem A;
let f be Function of NAT, the carrier' of X such that
E1: for i being Nat, s being stack of X st f.i = s holds
not emp s & f.(i+1) = pop s;
reconsider g = f.1 as Element of A* by EXAM;
defpred P[Nat] means
ex i st ex g being Element of A* st g = f.i & $1 = len g;
E2: ex k being Nat st P[k]
proof take k = len g, i = 1, g;
thus thesis;
end;
E3: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof let k be Nat;assume
E4: k <> 0; then
consider n0 being Nat such that
E7: k = n0+1 by NAT_1:6;
given i being Nat, g being Element of A* such that
E5: g = f.i & k = len g;
reconsider s = g as stack of X by E5;
reconsider h = pop s as Element of A* by EXAM;
take n = len h;
E8: s is non empty by E4,E5; then
not emp s by EXAM; then
E6: f.(i+1) = pop s & h = Del(g,1) by E1,E5,EXAM;
1 in dom g by E8,FINSEQ_5:6; then
n0 = n by E7,E5,E6,FINSEQ_3:118;
hence thesis by E7,E6,NAT_1:13;
end;
P[0] from NAT_1:sch 7(E2,E3); then
consider i being Nat, g being Element of A* such that
E9: g = f.i & 0 = len g;
reconsider s = g as stack of X by E9;
g is empty & not emp s by E1,E9;
hence thesis by EXAM;
end;
cluster StandardStackSystem A -> push-pop;
coherence
proof set X = StandardStackSystem A;
let s be stack of X;
reconsider g = s as Element of A* by EXAM;
assume
A0: not emp s; then
A2: s is non empty by EXAM; then
A1: g = <*g.1*>^Del(g,1) by POLYALG1:4;
reconsider h = Del(g,1) as stack of X by EXAM;
1 in dom g by A2,FINSEQ_5:6; then
g.1 in A by FUNCT_1:172; then
reconsider x = g.1 as Element of X by EXAM;
thus s = push(x, h) by A1,EXAM .= push(top s, h) by A0,EXAM
.= push(top s, pop s) by A0,EXAM;
end;
cluster StandardStackSystem A -> top-push;
coherence
proof set X = StandardStackSystem A;
let s be stack of X;
let e be Element of X;
reconsider g = s as Element of A* by EXAM;
reconsider h = push(e,s) as Element of A* by EXAM;
A1: h = <*e*>^g by EXAM; then
A2: not emp push(e,s) by EXAM;
thus e = h.1 by A1,FINSEQ_1:58 .= top push(e,s) by A2,EXAM;
end;
cluster StandardStackSystem A -> pop-push;
coherence
proof set X = StandardStackSystem A;
let s be stack of X;
let e be Element of X;
reconsider g = s as Element of A* by EXAM;
reconsider h = push(e,s) as Element of A* by EXAM;
A1: h = <*e*>^g by EXAM; then
A2: not emp push(e,s) by EXAM;
thus s = Del(<*e*>^g,1) by WSIERP_1:48 .= pop push(e,s) by A1,A2,EXAM;
end;
cluster StandardStackSystem A -> push-non-empty;
coherence
proof set X = StandardStackSystem A;
let s be stack of X;
let e be Element of X;
reconsider g = s as Element of A* by EXAM;
push(e,s) = <*e*>^g by EXAM;
hence not emp push(e,s) by EXAM;
end;
end;
registration
cluster pop-finite push-pop top-push pop-push push-non-empty
strict (non empty non void StackSystem);
existence
proof
set A = the non empty set;
take StandardStackSystem A; thus thesis;
end;
end;
definition
mode StackAlgebra is pop-finite push-pop top-push pop-push push-non-empty
(non empty non void StackSystem);
end;
theorem Th1:
for X being non empty non void StackSystem st X is pop-finite
ex s being stack of X st emp s
proof
let X be non empty non void StackSystem such that
A0: X is pop-finite;
set s1 = the stack of X;
defpred P[set, stack of X, stack of X] means $3 = pop $2;
A1: for n being Element of NAT for x being stack of X
ex y being stack of X st P[n,x,y];
consider f being Function of NAT, the carrier' of X such that
A2: f.0 = s1 & for n being Element of NAT holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A1);
consider i being Nat, s being stack of X such that
A3: f.i = s & (not emp s implies f.(i+1) <> pop s) by A0,POPFIN;
take s;
i is Element of NAT by ORDINAL1:def 13;
hence thesis by A2,A3;
end;
registration
let X be pop-finite (non empty non void StackSystem);
cluster the s_empty of X -> non empty;
coherence
proof
ex s being stack of X st emp s by Th1;
hence thesis by EMP;
end;
end;
theorem Th2:
X is top-push pop-push & push(e1,s1) = push(e2,s2) implies e1 = e2 & s1 = s2
proof assume X is top-push; then
A1: e1 = top push(e1,s1) & e2 = top push(e2,s2) by TOPPUSH;
assume X is pop-push; then
s1 = pop push(e1,s1) & s2 = pop push(e2,s2) by POPPUSH;
hence thesis by A1;
end;
theorem
X is push-pop & not emp s1 & not emp s2 &
pop s1 = pop s2 & top s1 = top s2 implies s1 = s2
proof
assume Z0: X is push-pop;
assume not emp s1; then
s1 = push(top s1, pop s1) by Z0,PUSHPOP;
hence thesis by Z0,PUSHPOP;
end;
begin :: Schemes of Induction
scheme
INDsch{X() -> StackAlgebra, s() -> stack of X(), P[set]}:
P[s()]
provided
P1: for s being stack of X() st emp s holds P[s] and
P2: for s being stack of X(), e being Element of X() st P[s]
holds P[push(e,s)]
proof
defpred Q[set, stack of X(), stack of X()] means $3 = pop $2;
A1: for n being Element of NAT for x being stack of X()
ex y being stack of X() st Q[n,x,y];
consider f being Function of NAT, the carrier' of X() such that
A2: f.0 = s() & for n being Element of NAT holds Q[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A1);
consider i being Nat, s being stack of X() such that
A3: f.i = s & (not emp s implies f.(i+1) <> pop s) by POPFIN;
defpred R[Nat] means P[f.(i-'$1)];
i-'0 = i by NAT_D:40; then
A5: R[0] by A3,A2,P1;
A6: now let j be Nat; assume
B1: R[j];
B2: i-'(j+1) = i-'j-'1 by NAT_2:32;
per cases;
suppose i-'j >= 1; then
i-'(j+1)+1 = i-'j by B2,XREAL_1:237; then
f.(i-'j) = pop (f.(i-'(j+1))) by A2; then
not emp f.(i-'(j+1)) implies
f.(i-'(j+1)) = push(top(f.(i-'(j+1))),f.(i-'j)) by PUSHPOP;
hence R[j+1] by P1,P2,B1;
end;
suppose
B7: i-'j < 0+1; then
B6: i-'j <= 0 by NAT_1:13;
B4: i-'j = 0 by B7,NAT_1:13;
i-'(j+1) = 0-'1 by B4,NAT_2:32 .= 0 by NAT_2:10;
hence R[j+1] by B1,B6;
end;
end;
for j being Nat holds R[j] from NAT_1:sch 2(A5,A6); then
R[i];
hence thesis by A2,XREAL_1:234;
end;
scheme
EXsch{X() -> StackAlgebra,
s() -> stack of X(),
A() -> non empty set,
e() -> Element of A(),
d(set,set) -> Element of A()}:
ex a being Element of A() st
ex F being Function of the carrier' of X(), A() st
a = F.s() & (for s1 being stack of X() st emp s1 holds F.s1 = e()) &
for s1 being stack of X(), e being Element of X()
holds F.push(e,s1) = d(e,F.s1)
proof
defpred G[set] means
(for s being stack of X() st emp s holds [s,e()] in $1) &
(for s being stack of X(), a being Element of X(), v being Element of A()
st [s,v] in $1 holds [push(a,s),d(a,v)] in $1);
consider M being set such that
A1: x in M iff x in bool [:the carrier' of X(),A():] & G[x]
from XBOOLE_0:sch 1;
B1: G[[:the carrier' of X(),A():]] & [:the carrier' of X(),A():] in
bool [:the carrier' of X(),A():] by ZFMISC_1:def 1; then
A2: [:the carrier' of X(),A():] in M by A1;
reconsider M as non empty set by A1,B1;
set F = meet M;
reconsider F as Subset of [:the carrier' of X(),A():] by A2,SETFAM_1:4;
defpred P[stack of X()] means
for y1,y2 being set st [$1,y1] in F & [$1,y2] in F holds y1 = y2;
A8: G[F]
proof
hereby let s be stack of X(); assume emp s; then
for Y being set st Y in M holds [s,e()] in Y by A1;
hence [s,e()] in F by SETFAM_1:def 1;
end;
let s be stack of X(), a be Element of X(), v be Element of A(); assume
S1: [s,v] in F;
now let Y be set; assume Y in M; then
G[Y] & [s,v] in Y by S1,A1,SETFAM_1:def 1;
hence [push(a,s),d(a,v)] in Y;
end;
hence [push(a,s),d(a,v)] in F by SETFAM_1:def 1;
end;
defpred Q[stack of X()] means
ex y being set st [$1,y] in F;
A6: for s being stack of X() st emp s holds Q[s]
proof
let s be stack of X(); assume
Z0: emp s;
take y = e();
for Y being set st Y in M holds [s,e()] in Y by Z0,A1;
hence thesis by SETFAM_1:def 1;
end;
A7: for s being stack of X(), e being Element of X() st Q[s] holds Q[push(e,s)]
proof
let s be stack of X(), e be Element of X();
given y being set such that
M1: [s,y] in F;
reconsider y as Element of A() by M1,ZFMISC_1:106;
take z = d(e,y);
now let Y be set; assume
M2: Y in M; then
[s,y] in Y by M1,SETFAM_1:def 1;
hence [push(e,s),z] in Y by M2,A1;
end;
hence thesis by SETFAM_1:def 1;
end;
A3: for s being stack of X() st emp s holds P[s]
proof let s be stack of X(); assume
B1: emp s;
let y1,y2 be set; assume
B2: [s,y1] in F & [s,y2] in F;
set Y1 = F \ {[s,y1]}, Y2 = F \ {[s,y2]};
B8: now assume
B4: y1 <> e();
G[Y1]
proof
hereby let s1 be stack of X(); assume emp s1; then
B5: [s1,e()] in F by A8;
[s,y1] <> [s1,e()] by B4,ZFMISC_1:33; then
[s1,e()] nin {[s,y1]} by TARSKI:def 1;
hence [s1,e()] in Y1 by B5,XBOOLE_0:def 5;
end;
let s1 be stack of X(), a be Element of X(), v be Element of A();
assume [s1,v] in Y1; then
[s1,v] in F by XBOOLE_0:def 5; then
B6: [push(a,s1),d(a,v)] in F by A8;
push(a,s1) <> s by B1,PUSHNE; then
[s,y1] <> [push(a,s1),d(a,v)] by ZFMISC_1:33; then
[push(a,s1),d(a,v)] nin {[s,y1]} by TARSKI:def 1;
hence [push(a,s1),d(a,v)] in Y1 by B6,XBOOLE_0:def 5;
end; then
Y1 in M by A1; then
F c= Y1 by SETFAM_1:4; then
[s,y1] in Y1 & [s,y1] in {[s,y1]} by B2,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
now assume
B4: y2 <> e();
G[Y2]
proof
hereby let s1 be stack of X(); assume emp s1; then
B5: [s1,e()] in F by A8;
[s,y2] <> [s1,e()] by B4,ZFMISC_1:33; then
[s1,e()] nin {[s,y2]} by TARSKI:def 1;
hence [s1,e()] in Y2 by B5,XBOOLE_0:def 5;
end;
let s1 be stack of X(), a be Element of X(), v be Element of A();
assume [s1,v] in Y2; then
[s1,v] in F by XBOOLE_0:def 5; then
B6: [push(a,s1),d(a,v)] in F by A8;
push(a,s1) <> s by B1,PUSHNE; then
[s,y2] <> [push(a,s1),d(a,v)] by ZFMISC_1:33; then
[push(a,s1),d(a,v)] nin {[s,y2]} by TARSKI:def 1;
hence [push(a,s1),d(a,v)] in Y2 by B6,XBOOLE_0:def 5;
end; then
Y2 in M by A1; then
F c= Y2 by SETFAM_1:4; then
[s,y2] in Y2 & [s,y2] in {[s,y2]} by B2,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
hence y1 = y2 by B8;
end;
A4: for s being stack of X(), e being Element of X() st P[s] holds P[push(e,s)]
proof let s be stack of X(), e be Element of X(); assume
C1: P[s];
let y1,y2 be set;assume
C2: [push(e,s),y1] in F & [push(e,s),y2] in F;
Q[s] from INDsch(A6,A7); then
consider y being set such that
C9: [s,y] in F;
reconsider y as Element of A() by C9,ZFMISC_1:106;
set Y1 = F \ {[push(e,s),y1]}, Y2 = F \ {[push(e,s),y2]};
C8: now assume
C4: y1 <> d(e,y);
G[Y1]
proof
hereby let s1 be stack of X(); assume
C11: emp s1; then
C5: [s1,e()] in F by A8;
not emp push(e,s) by PUSHNE; then
[push(e,s),y1] <> [s1,e()] by C11,ZFMISC_1:33; then
[s1,e()] nin {[push(e,s),y1]} by TARSKI:def 1;
hence [s1,e()] in Y1 by C5,XBOOLE_0:def 5;
end;
let s1 be stack of X(), a be Element of X(), v be Element of A();
assume [s1,v] in Y1; then
C10: [s1,v] in F by XBOOLE_0:def 5; then
C6: [push(a,s1),d(a,v)] in F by A8;
now assume [push(e,s),y1] = [push(a,s1),d(a,v)]; then
C12: push(e,s) = push(a,s1) & y1 = d(a,v) by ZFMISC_1:33; then
e = a & s = s1 by Th2;
hence contradiction by C1,C9,C10,C4,C12;
end; then
[push(a,s1),d(a,v)] nin {[push(e,s),y1]} by TARSKI:def 1;
hence [push(a,s1),d(a,v)] in Y1 by C6,XBOOLE_0:def 5;
end; then
Y1 in M by A1; then
F c= Y1 by SETFAM_1:4; then
[push(e,s),y1] in Y1 & [push(e,s),y1] in {[push(e,s),y1]}
by C2,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
now assume
C4: y2 <> d(e,y);
G[Y2]
proof
hereby let s1 be stack of X(); assume
C11: emp s1; then
C5: [s1,e()] in F by A8;
not emp push(e,s) by PUSHNE; then
[push(e,s),y2] <> [s1,e()] by C11,ZFMISC_1:33; then
[s1,e()] nin {[push(e,s),y2]} by TARSKI:def 1;
hence [s1,e()] in Y2 by C5,XBOOLE_0:def 5;
end;
let s1 be stack of X(), a be Element of X(), v be Element of A();
assume [s1,v] in Y2; then
C10: [s1,v] in F by XBOOLE_0:def 5; then
C6: [push(a,s1),d(a,v)] in F by A8;
now assume [push(e,s),y2] = [push(a,s1),d(a,v)]; then
C12: push(e,s) = push(a,s1) & y2 = d(a,v) by ZFMISC_1:33; then
e = a & s = s1 by Th2;
hence contradiction by C1,C9,C10,C4,C12;
end; then
[push(a,s1),d(a,v)] nin {[push(e,s),y2]} by TARSKI:def 1;
hence [push(a,s1),d(a,v)] in Y2 by C6,XBOOLE_0:def 5;
end; then
Y2 in M by A1; then
F c= Y2 by SETFAM_1:4; then
[push(e,s),y2] in Y2 & [push(e,s),y2] in {[push(e,s),y2]}
by C2,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
hence y1 = y2 by C8;
end;
A5: F is Function-like
proof
let x,y1,y2 be set; assume
B1: [x,y1] in F & [x,y2] in F; then
reconsider x as stack of X() by ZFMISC_1:106;
P[x] from INDsch(A3,A4);
hence thesis by B1;
end;
F is quasi_total
proof
per cases;
case A() = {} implies the carrier' of X() = {};
thus the carrier' of X() c= dom F
proof
let x; assume x in the carrier' of X();
then reconsider x as stack of X();
Q[x] from INDsch(A6,A7);
hence thesis by RELAT_1:def 4;
end;
thus thesis;
end;
case A() = {} & the carrier' of X() <> {};
hence thesis;
end;
end; then
reconsider F as Function of the carrier' of X(),A() by A5;
take a = F.s(), F;
thus a = F.s();
hereby let s1 be stack of X(); assume emp s1; then
[s1,e()] in F by A8;
hence F.s1 = e() by FUNCT_1:8;
end;
let s1 be stack of X(), e be Element of X();
dom F = the carrier' of X() by FUNCT_2:def 1; then
[s1,F.s1] in F by FUNCT_1:def 4; then
[push(e,s1),d(e,F.s1)] in F by A8;
hence F.push(e,s1) = d(e,F.s1) by FUNCT_1:8;
end;
scheme
UNIQsch{X() -> StackAlgebra,
s() -> stack of X(),
A() -> non empty set,
e() -> Element of A(),
d(set,set) -> Element of A()}:
for a1,a2 being Element of A() st
(ex F being Function of the carrier' of X(), A() st
a1 = F.s() & (for s1 being stack of X() st emp s1 holds F.s1 = e()) &
for s1 being stack of X(), e being Element of X()
holds F.push(e,s1) = d(e,F.s1)) &
(ex F being Function of the carrier' of X(), A() st
a2 = F.s() & (for s1 being stack of X() st emp s1 holds F.s1 = e()) &
for s1 being stack of X(), e being Element of X()
holds F.push(e,s1) = d(e,F.s1))
holds a1 = a2
proof
let a1,a2 be Element of A();
given F1 be Function of the carrier' of X(), A() such that
A1: a1 = F1.s() & (for s1 being stack of X() st emp s1 holds F1.s1 = e()) &
for s1 being stack of X(), e being Element of X()
holds F1.push(e,s1) = d(e,F1.s1);
given F2 be Function of the carrier' of X(), A() such that
A2: a2 = F2.s() & (for s1 being stack of X() st emp s1 holds F2.s1 = e()) &
for s1 being stack of X(), e being Element of X()
holds F2.push(e,s1) = d(e,F2.s1);
defpred P[stack of X()] means F1.$1 = F2.$1;
A3: now let s be stack of X();
assume emp s; then
F1.s = e() & F2.s = e() by A1,A2;
hence P[s];
end;
A4: now let s be stack of X(), e be Element of X();
assume
P[s]; then
F1.push(e,s) = d(e,F2.s) by A1;
hence P[push(e,s)] by A2;
end;
P[s()] from INDsch(A3,A4);
hence a1 = a2 by A1,A2;
end;
begin :: Stack Congruence
reserve X for StackAlgebra;
reserve s,s1,s2,s3 for stack of X;
reserve e,e1,e2,e3 for Element of X;
definition
let X,s;
func |.s.| -> Element of (the carrier of X)* means:
MOD:
ex F being Function of the carrier' of X, (the carrier of X)* st
it = F.s & (for s1 st emp s1 holds F.s1 = {}) &
for s1, e holds F.push(e,s1) = <*e*>^(F.s1);
existence
proof
deffunc d(Element of X, Element of (the carrier of X)*) = <*$1*>^$2;
reconsider w = <*>the carrier of X as Element of (the carrier of X)*
by FINSEQ_1:def 11;
ex a being Element of (the carrier of X)* st
ex F being Function of the carrier' of X, (the carrier of X)* st
a = F.s & (for s1 st emp s1 holds F.s1 = w) &
for s1, e holds F.push(e,s1) = d(e,F.s1 qua Element of (the carrier of X)*)
from EXsch;
hence thesis;
end;
uniqueness
proof
deffunc d(Element of X, Element of (the carrier of X)*) = <*$1*>^$2;
reconsider w = <*>the carrier of X as Element of (the carrier of X)*
by FINSEQ_1:def 11;
for a1,a2 being Element of (the carrier of X)* st
(ex F being Function of the carrier' of X, (the carrier of X)* st
a1 = F.s & (for s1 st emp s1 holds F.s1 = w) &
for s1,e holds F.push(e,s1) = d(e,F.s1 qua Element of (the carrier of X)*))
&
(ex F being Function of the carrier' of X, (the carrier of X)* st
a2 = F.s & (for s1 st emp s1 holds F.s1 = w) &
for s1,e holds F.push(e,s1) = d(e,F.s1 qua Element of (the carrier of X)*))
holds a1 = a2 from UNIQsch;
hence thesis;
end;
end;
theorem Th31:
emp s implies |.s.| = {}
proof
ex F being Function of the carrier' of X, (the carrier of X)* st
|.s.| = F.s & (for s1 st emp s1 holds F.s1 = {}) &
for s1, e holds F.push(e,s1) = <*e*>^(F.s1) by MOD;
hence thesis;
end;
theorem Th32:
not emp s implies |.s.| = <*top s*>^|.pop s.|
proof
consider F being Function of the carrier' of X, (the carrier of X)* such
that
A1: |.s.| = F.s & (for s1 st emp s1 holds F.s1 = {}) &
for s1, e holds F.push(e,s1) = <*e*>^(F.s1) by MOD;
A2: |.pop s.| = F.pop s by A1,MOD;
assume not emp s; then
s = push(top s, pop s) by PUSHPOP;
hence thesis by A1,A2;
end;
theorem Th33:
not emp s implies |.pop s.| = Del(|.s.|,1)
proof
assume not emp s; then
|.s.| = <*top s*>^|.pop s.| by Th32;
hence thesis by WSIERP_1:48;
end;
theorem Th34:
|.push(e,s).| = <*e*>^|.s.|
proof
not emp push(e,s) by PUSHNE;
hence |.push(e,s).| = <*top push(e,s)*>^|.pop push(e,s).| by Th32
.= <*e*>^|.pop push(e,s).| by TOPPUSH
.= <*e*>^|.s.| by POPPUSH;
end;
theorem Th35:
not emp s implies top s = |.s.|.1
proof
assume not emp s; then
|.s.| = <*top s*>^|.pop s.| by Th32;
hence top s = |.s.|.1 by FINSEQ_1:58;
end;
theorem Th351:
|.s.| = {} implies emp s
proof assume |.s.| = {} & not emp s; then
{} = <*top s*>^|.pop s.| by Th32;
hence thesis;
end;
theorem ThZ:
for s being stack of StandardStackSystem A holds |.s.| = s
proof
defpred P[stack of StandardStackSystem A] means |.$1.| = $1;
A1: now let s be stack of StandardStackSystem A;
assume emp s; then
s = {} & |.s.| = {} by EXAM,Th31;
hence P[s];
end;
A2: now let s be stack of StandardStackSystem A;
let e be Element of StandardStackSystem A;
assume P[s]; then
|.push(e,s).| = <*e*>^s by Th34;
hence P[push(e,s)] by EXAM;
end;
let s be stack of StandardStackSystem A;
thus P[s] from INDsch(A1,A2);
end;
theorem Th36:
for x being Element of (the carrier of X)*
ex s st |.s.| = x
proof
set D = the carrier of X;
defpred P[FinSequence of D] means ex s st |.s.| = $1;
A1: P[<*> D]
proof
consider s such that
B1: emp s by Th1;
take s; thus thesis by B1,Th31;
end;
A2: for p being FinSequence of D for x being Element of D st P[p]
holds P[<*x*>^p]
proof
let p be FinSequence of D, x be Element of D;
given s such that
A3: |.s.| = p;
take s2 = push(x,s);
thus thesis by A3,Th34;
end;
for p being FinSequence of D holds P[p] from IndSeqD(A1,A2);
hence thesis;
end;
definition
let X,s1,s2;
pred s1 == s2 means:
CONG: |.s1.| = |.s2.|;
reflexivity;
symmetry;
end;
theorem Th41:
s1 == s2 & s2 == s3 implies s1 == s3
proof
assume |.s1.| = |.s2.| & |.s2.| = |.s3.|;
hence |.s1.| = |.s3.|;
end;
theorem Th42:
s1 == s2 & emp s1 implies emp s2
proof
assume
A1: |.s1.| = |.s2.| & emp s1;
assume not emp s2; then
|.s2.| = <*top s2*>^|.pop s2.| by Th32;
hence thesis by A1,Th31;
end;
theorem Th43:
emp s1 & emp s2 implies s1 == s2
proof
assume emp s1 & emp s2; then
|.s1.| = {} & |.s2.| = {} by Th31;
hence |.s1.| = |.s2.|;
end;
theorem Th44:
s1 == s2 implies push(e,s1) == push(e,s2)
proof
assume |.s1.| = |.s2.|;
hence |.push(e,s1).| = <*e*>^|.s2.| by Th34 .= |.push(e,s2).| by Th34;
end;
theorem Th45:
s1 == s2 & not emp s1 implies pop s1 == pop s2
proof
assume
A0: s1 == s2 & not emp s1; then
A1: |.s1.| = |.s2.| & not emp s2 by CONG,Th42;
thus |.pop s1.| = Del(|.s1.|,1) by A0,Th33 .= |.pop s2.| by A1,Th33;
end;
theorem Th46:
s1 == s2 & not emp s1 implies top s1 = top s2
proof
assume
A0: s1 == s2 & not emp s1; then
A1: |.s1.| = |.s2.| & not emp s2 by CONG,Th42;
thus top s1 = |.s1.|.1 by A0,Th35 .= top s2 by A1,Th35;
end;
definition
let X;
attr X is proper-for-identity means:
PROP:
for s1,s2 st s1 == s2 holds s1 = s2;
end;
registration
let A;
cluster StandardStackSystem A -> proper-for-identity;
coherence
proof set X = StandardStackSystem A;
let s1,s2 be stack of X;
assume |.s1.| = |.s2.|;
hence s1 = |.s2.| by ThZ .= s2 by ThZ;
end;
end;
definition
let X;
func ==_X -> Relation of the carrier' of X means:
REL:
[s1,s2] in it iff s1 == s2;
existence
proof
defpred P[stack of X, stack of X] means $1 == $2;
thus ex R being Relation of the carrier' of X st
for s1,s2 holds [s1,s2] in R iff P[s1,s2] from RELSET_1:sch 2;
end;
uniqueness
proof
defpred P[stack of X, stack of X] means $1 == $2;
let R1,R2 be Relation of the carrier' of X such that
A1: [s1,s2] in R1 iff P[s1,s2] and
A2: [s1,s2] in R2 iff P[s1,s2];
thus thesis from RELSET_1:sch 4(A1,A2);
end;
end;
registration
let X;
cluster ==_X -> total symmetric transitive;
coherence
proof set R = ==_X;
thus
A1: dom (==_X) = the carrier' of X
proof
thus dom R c= the carrier' of X;
let x; assume x in the carrier' of X; then
reconsider s = x as stack of X;
[s,s] in R by REL;
hence thesis by RELAT_1:def 4;
end;
A4: field R = dom R \/ rng R
.= the carrier' of X by A1,XBOOLE_1:12;
thus ==_X is symmetric
proof
let x,y be set; assume
x in field R & y in field R; then
reconsider s1 = x, s2 = y as stack of X by A4;
assume [x,y] in R; then
s1 == s2 by REL;
hence thesis by REL;
end;
let x,y,z be set; assume
x in field R & y in field R & z in field R; then
reconsider s1 = x, s2 = y, s3 = z as stack of X by A4;
assume [x,y] in R & [y,z] in R; then
s1 == s2 & s2 == s3 by REL; then
s1 == s3 by Th41;
hence thesis by REL;
end;
end;
theorem Th50:
emp s implies Class(==_X, s) = the s_empty of X
proof
assume
Z0: emp s;
thus Class(==_X, s) c= the s_empty of X
proof
let x; assume
Z1: x in Class(==_X, s); then
reconsider s1 = x as stack of X;
[s,s1] in ==_X by Z1,EQREL_1:26; then
s == s1 by REL; then
emp s1 by Z0,Th42;
hence thesis by EMP;
end;
let x; assume
Z2: x in the s_empty of X; then
reconsider s1 = x as stack of X;
emp s1 by Z2,EMP; then
s == s1 by Z0,Th43; then
[s,s1] in ==_X by REL;
hence thesis by EQREL_1:26;
end;
definition
let X,s;
func coset s -> Subset of the carrier' of X means:
COSET:
s in it &
(for e,s1 st s1 in it holds
push(e,s1) in it & (not emp s1 implies pop s1 in it)) &
for A being Subset of the carrier' of X st
s in A &
(for e,s1 st s1 in A holds
push(e,s1) in A & (not emp s1 implies pop s1 in A))
holds it c= A;
existence
proof
defpred P[set] means
s in $1 &
(for e,s1 st s1 in $1 holds
push(e,s1) in $1 & (not emp s1 implies pop s1 in $1));
consider Y being set such that
A1: x in Y iff x in bool the carrier' of X & P[x] from XBOOLE_0:sch 1;
set S = the carrier' of X;
B1: P[the carrier' of X] & S in bool S by ZFMISC_1:def 1; then
A2: the carrier' of X in Y by A1;
reconsider Y as non empty set by B1,A1;
reconsider C = meet Y as Subset of S by A2,SETFAM_1:4;
take C;
for x st x in Y holds s in x by A1;
hence s in C by SETFAM_1:def 1;
hereby
let e,s1; assume
A3: s1 in C;
now let x; assume
A6: x in Y; then
s1 in x by A3,SETFAM_1:def 1;
hence push(e,s1) in x by A1,A6;
end;
hence push(e,s1) in C by SETFAM_1:def 1;
assume
A4: not emp s1;
now let x; assume
A5: x in Y; then
s1 in x by A3,SETFAM_1:def 1;
hence pop s1 in x by A1,A4,A5;
end;
hence pop s1 in C by SETFAM_1:def 1;
end;
let A be Subset of the carrier' of X;
assume P[A]; then
A in Y by A1;
hence C c= A by SETFAM_1:4;
end;
uniqueness
proof let C1,C2 be Subset of the carrier' of X;
assume
A1: not thesis;
C1 = C2 proof thus C1 c= C2 & C2 c= C1 by A1; end;
hence thesis by A1;
end;
end;
theorem Th53:
(push(e,s) in coset s1 implies s in coset s1) &
(not emp s & pop s in coset s1 implies s in coset s1)
proof
pop push(e,s) = s & not emp push(e,s) by POPPUSH,PUSHNE;
hence push(e,s) in coset s1 implies s in coset s1 by COSET;
assume not emp s; then
push(top s, pop s) = s by PUSHPOP;
hence thesis by COSET;
end;
theorem
s in coset push(e,s) & (not emp s implies s in coset pop s)
proof
pop push(e,s) = s & not emp push(e,s) & push(e,s) in coset push(e,s)
by POPPUSH,PUSHNE,COSET;
hence s in coset push(e,s) by COSET;
assume not emp s; then
push(top s, pop s) = s & pop s in coset pop s by PUSHPOP,COSET;
hence thesis by COSET;
end;
theorem
ex s1 st emp s1 & s1 in coset s
proof
deffunc F(stack of X) = pop $1;
defpred P[set,stack of X,set] means
$3 = IFIN($2,the s_empty of X,s,pop $2);
A0: for n being Element of NAT for x being stack of X
ex y being stack of X st P[n,x,y];
consider f being Function of NAT, the carrier' of X such that
A1: f.0 = s & for i being Element of NAT holds P[i,f.i,f.(i+1)]
from RECDEF_1:sch 2(A0);
defpred Q[Nat] means f.$1 in coset s;
A2: Q[0] by A1,COSET;
A3: now let i; assume
B1: Q[i];
i in NAT by ORDINAL1:def 13; then
f.(i+1) = IFIN(f.i,the s_empty of X,s,pop(f.i)) by A1; then
(f.i in the s_empty of X implies f.(i+1) = s) &
(f.i nin the s_empty of X implies f.(i+1) = pop(f.i))
by MATRIX_7:def 1; then
f.(i+1) = s or not emp f.i & f.(i+1) = pop(f.i) by EMP;
hence Q[i+1] by B1,COSET;
end;
A4: Q[i] from NAT_1:sch 2(A2,A3);
consider i,s1 such that
A5: f.i = s1 & (not emp s1 implies f.(i+1) <> pop s1) by POPFIN;
take s1;
i in NAT by ORDINAL1:def 13; then
f.(i+1) = IFIN(f.i,the s_empty of X,s,pop(f.i)) by A1; then
(f.i in the s_empty of X implies f.(i+1) = s) &
(f.i nin the s_empty of X implies f.(i+1) = pop(f.i))
by MATRIX_7:def 1;
hence thesis by A5,A4,EMP;
end;
registration
let A;
let R be Relation of A;
cluster A-valued RedSequence of R;
existence
proof
set a = the Element of A;
reconsider t = <*a*> as RedSequence of R by REWRITE1:7;
take t; thus thesis;
end;
end;
definition
let X;
func ConstructionRed X -> Relation of the carrier' of X means:
CRED:
[s1,s2] in it iff (not emp s1 & s2 = pop s1) or ex e st s2 = push(e,s1);
existence
proof
defpred P[stack of X, stack of X] means
(not emp $1 & $2 = pop $1) or ex e st $2 = push(e,$1);
thus ex R being Relation of the carrier' of X st
for s1,s2 holds [s1,s2] in R iff P[s1,s2] from RELSET_1:sch 2;
end;
uniqueness
proof
defpred P[stack of X, stack of X] means
(not emp $1 & $2 = pop $1) or ex e st $2 = push(e,$1);
let R1,R2 be Relation of the carrier' of X such that
A1: [s1,s2] in R1 iff P[s1,s2] and
A2: [s1,s2] in R2 iff P[s1,s2];
thus thesis from RELSET_1:sch 4(A1,A2);
end;
end;
theorem Lem2:
for R being Relation of A
for t being RedSequence of R holds t.1 in A iff t is A-valued
proof
let R be Relation of A;
let t be RedSequence of R;
rng t <> {}; then
1 in dom t by FINSEQ_3:34; then
A2: t.1 in rng t by FUNCT_1:def 5;
hereby
assume
Z0: t.1 in A;
defpred P[Nat] means $1 in dom t implies t.$1 in A;
A3: P[0] by FINSEQ_3:26;
A4: P[i] implies P[i+1]
proof assume
P[i]; assume
B1: i+1 in dom t & t.(i+1) nin A;
i = 0 or i >= 0+1 by NAT_1:13; then
consider j being Nat such that
B2: i = j+1 by Z0,B1,NAT_1:6;
i <= i+1 & i+1 <= len t by B1,NAT_1:11,FINSEQ_3:27; then
1 <= i & i <= len t by B2,XXREAL_0:2,NAT_1:11; then
i in dom t by FINSEQ_3:27; then
[t.i, t.(i+1)] in R by B1,REWRITE1:def 2;
hence thesis by B1,ZFMISC_1:106;
end;
A5: P[i] from NAT_1:sch 2(A3,A4);
thus t is A-valued
proof
let x; assume x in rng t; then
consider y such that
C1: y in dom t & x = t.y by FUNCT_1:def 5;
reconsider y as Nat by C1;
thus thesis by C1,A5;
end;
end;
assume rng t c= A;
hence t.1 in A by A2;
end;
scheme PathIND{X() -> non empty set, x1,x2() -> Element of X(),
R() -> (Relation of X()), P[set]}:
P[x2()]
provided
W1: P[x1()] and
W2: R() reduces x1(),x2() and
W3: for x,y being Element of X() st R() reduces x1(),x & [x,y] in R() &
P[x] holds P[y]
proof
consider t being RedSequence of R() such that
A1: t.1 = x1() & t.len t = x2() by W2,REWRITE1:def 3;
reconsider t as X()-valued RedSequence of R() by A1,Lem2;
defpred Q[Nat] means $1 in dom t implies P[t.$1];
A2: Q[0] by FINSEQ_3:26;
A3: now let i; assume
A4: Q[i];
thus Q[i+1]
proof assume
A5: i+1 in dom t & not P[t.(i+1)];
i = 0 or i >= 0+1 by NAT_1:13; then
consider j being Nat such that
A6: i = j+1 by W1,A1,A5,NAT_1:6;
i <= i+1 & i+1 <= len t by A5,NAT_1:11,FINSEQ_3:27; then
A9: 1 <= i & i <= len t & rng t <> {} by A6,XXREAL_0:2,NAT_1:11; then
A7: i in dom t & 1 in dom t by FINSEQ_3:27,34;
A8: t.i = t/.i & t.(i+1) = t/.(i+1) by A5,A7,PARTFUN1:def 8; then
[t/.i,t/.(i+1)] in R() by A5,A7,REWRITE1:def 2;
hence thesis by W3,A4,A5,A7,A1,A9,A8,REWRITE1:18;
end;
end;
BB: Q[i] from NAT_1:sch 2(A2,A3);
len t in dom t by FINSEQ_5:6;
hence thesis by A1,BB;
end;
theorem Th57:
for t being RedSequence of ConstructionRed X
st s = t.1 holds rng t c= coset s
proof set R = ConstructionRed X;
let t be RedSequence of ConstructionRed X;
assume
Z0: s = t.1; then
reconsider u = t as the carrier' of X-valued RedSequence of R by Lem2;
defpred Q[Nat] means $1 in dom t implies t.$1 in coset s;
A2: Q[0] by FINSEQ_3:26;
A3: now let i; assume
A4: Q[i];
thus Q[i+1]
proof assume
A5: i+1 in dom t & t.(i+1) nin coset s;
i = 0 or i >= 0+1 by NAT_1:13; then
consider j being Nat such that
A6: i = j+1 by Z0,A5,COSET,NAT_1:6;
i <= i+1 & i+1 <= len t by A5,NAT_1:11,FINSEQ_3:27; then
A9: 1 <= i & i <= len t & rng t <> {} by A6,XXREAL_0:2,NAT_1:11; then
A7: i in dom t & 1 in dom t by FINSEQ_3:27,34; then
A8: t.i = u/.i & t.(i+1) = u/.(i+1) by A5,PARTFUN1:def 8; then
[u/.i,u/.(i+1)] in R by A5,A7,REWRITE1:def 2; then
(not emp u/.i & u/.(i+1) = pop(u/.i)) or
ex e st u/.(i+1) = push(e,u/.i) by CRED;
hence thesis by A4,A5,A9,A8,COSET,FINSEQ_3:27;
end;
end;
BB: Q[i] from NAT_1:sch 2(A2,A3);
let x; assume x in rng t; then
ex y st y in dom t & x = t.y by FUNCT_1:def 5;
hence thesis by BB;
end;
theorem Th58:
coset s = {s1: ConstructionRed X reduces s,s1}
proof set R = ConstructionRed X;
A0: {s1: R reduces s,s1} c= the carrier' of X
proof let x;
assume x in {s1: R reduces s,s1}; then
ex s1 st x = s1 & R reduces s,s1;
hence thesis;
end;
R reduces s,s by REWRITE1:13; then
A1: s in {s1: R reduces s,s1};
now let e,s2; assume
s2 in {s1: R reduces s,s1}; then
A2: ex s1 st s2 = s1 & R reduces s,s1;
[s2, push(e,s2)] in R by CRED; then
R reduces s2, push(e,s2) by REWRITE1:16; then
R reduces s, push(e,s2) by A2,REWRITE1:17;
hence push(e,s2) in {s1: R reduces s,s1};
assume not emp s2; then
[s2, pop s2] in R by CRED; then
R reduces s2, pop s2 by REWRITE1:16; then
R reduces s, pop s2 by A2,REWRITE1:17;
hence pop s2 in {s1: R reduces s,s1};
end;
hence coset s c= {s1: R reduces s,s1} by A0,A1,COSET;
let x; assume x in {s1: R reduces s,s1}; then
consider s1 such that
A3: x = s1 & R reduces s,s1;
consider t being RedSequence of R such that
A4: s = t.1 & s1 = t.len t by A3,REWRITE1:def 3;
len t in dom t by FINSEQ_5:6; then
x in rng t & rng t c= coset s by A3,A4,Th57,FUNCT_1:def 5;
hence thesis;
end;
definition
let X,s;
func core s -> stack of X means:
CORE:
emp it &
ex t being the carrier' of X-valued RedSequence of ConstructionRed X st
t.1 = s & t.len t = it &
for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i);
existence
proof set R = ConstructionRed X;
deffunc F(stack of X) = pop $1;
defpred P[set,stack of X,set] means
$3 = IFIN($2,the s_empty of X,s,pop $2);
A0: for n being Element of NAT for x being stack of X
ex y being stack of X st P[n,x,y];
consider f being Function of NAT, the carrier' of X such that
A1: f.0 = s & for i being Element of NAT holds P[i,f.i,f.(i+1)]
from RECDEF_1:sch 2(A0);
defpred R[Nat] means
ex s1 st f.$1 = s1 & (not emp s1 implies f.($1+1) <> pop s1);
A5: ex i st R[i] by POPFIN;
consider i such that
A6: R[i] & for j being Nat st R[j] holds i <= j from NAT_1:sch 5(A5);
deffunc F(Nat) = f.($1-'1);
consider t being FinSequence such that
A7: len t = i+1 & for j being Nat st j in dom t holds t.j = F(j)
from FINSEQ_1:sch 2;
consider s1 such that
A8: f.i = s1 & (not emp s1 implies f.(i+1) <> pop s1) by A6;
take s1;
i in NAT by ORDINAL1:def 13; then
f.(i+1) = IFIN(f.i,the s_empty of X,s,pop(f.i)) by A1; then
(f.i in the s_empty of X implies f.(i+1) = s) &
(f.i nin the s_empty of X implies f.(i+1) = pop(f.i))
by MATRIX_7:def 1;
hence emp s1 by A8,EMP;
A9: t is RedSequence of R
proof
thus len t > 0 by A7;
let j being Element of NAT; assume
B1: j in dom t & j+1 in dom t; then
j >= 1 & j <= i+1 & j+1 <= i+1 by A7,FINSEQ_3:27; then
B2: j-'1+1 = j & j+1-'1 = j & j <= i by NAT_D:34,XREAL_1:8,237;
j-'1 < i by B2,NAT_1:13; then
B7: not emp f.(j-'1) by A6; then
B4: f.(j-'1) nin the s_empty of X by EMP;
B5: t.j = f.(j-'1) & t.(j+1) = f.j by A7,B1,B2; then
P[j-'1,f.(j-'1),t.(j+1)] by A1,B2; then
t.(j+1) = pop(f.(j-'1)) by B4,MATRIX_7:def 1;
hence [t.j, t.(j+1)] in R by B5,B7,CRED;
end; then
1 in dom t by FINSEQ_5:6; then
C1: t.1 = f.(1-'1) by A7 .= s by A1,XREAL_1:234; then
reconsider t as the carrier' of X-valued RedSequence of R by A9,Lem2;
take t;
thus t.1 = s by C1;
len t in dom t by FINSEQ_5:6;
hence t.len t = f.(i+1-'1) by A7 .= s1 by A8,NAT_D:34;
let k be Nat; assume
C2: 1 <= k & k < len t; then
k in dom t by FINSEQ_3:27; then
C3: t.k = f.(k-'1) & t.k = t/.k by A7,PARTFUN1:def 8;
1 <= k+1 & k+1 <= len t by C2,NAT_1:13; then
k+1 in dom t by FINSEQ_3:27; then
C4: t.(k+1) = f.(k+1-'1) & t.(k+1) = t/.(k+1) by A7,PARTFUN1:def 8;
C6: k-'1+1 = k & k+1-'1 = k by C2,NAT_D:34,XREAL_1:237; then
k-'1 < i by A7,C2,XREAL_1:8;
hence not emp t/.k by A6,C3; then
C5: t/.k nin the s_empty of X by EMP;
f.k = IFIN(f.(k-'1),the s_empty of X,s,pop(f.(k-'1))) by A1,C6;
hence t/.(k+1) = pop(t/.k) by C3,C4,C6,C5,MATRIX_7:def 1;
end;
uniqueness
proof let x1,x2 be stack of X such that
A1: emp x1;
given t1 being the carrier' of X-valued RedSequence of ConstructionRed X
such that
A2: t1.1 = s & t1.len t1 = x1 and
A3: for i st 1 <= i & i < len t1 holds not emp t1/.i & t1/.(i+1) = pop(t1/.i);
assume
B1: emp x2;
given t2 being the carrier' of X-valued RedSequence of ConstructionRed X
such that
B2: t2.1 = s & t2.len t2 = x2 and
B3: for i st 1 <= i & i < len t2 holds not emp t2/.i & t2/.(i+1) = pop(t2/.i);
A4: len t1 in dom t1 & len t2 in dom t2 & 1 in dom t1 & 1 in dom t2
by FINSEQ_5:6;
defpred P[Nat] means ($1 in dom t1 iff $1 in dom t2) &
($1 in dom t1 implies t1.$1 = t2.$1);
I1: P[0] by FINSEQ_3:26;
I2: P[i] implies P[i+1]
proof assume
J1: P[i];
per cases by NAT_1:6;
suppose i = 0;
hence thesis by A2,B2,FINSEQ_5:6;
end;
suppose ex j st i = j+1; then
consider j such that
J2: i = j+1;
J4: i >= 1 by J2,NAT_1:11;
thus
JJ: now assume
i+1 in dom t1; then
i+1 <= len t1 by FINSEQ_3:27; then
i < len t1 by NAT_1:13; then
i in dom t1 & not emp t1/.i by A3,J4,FINSEQ_3:27; then
len t2 <> i & i <= len t2
by B1,B2,J1,PARTFUN1:def 8,FINSEQ_3:27; then
i < len t2 by XXREAL_0:1; then
1 <= i+1 & i+1 <= len t2 by NAT_1:11,13;
hence i+1 in dom t2 by FINSEQ_3:27;
end;
hereby assume
i+1 in dom t2; then
i+1 <= len t2 by FINSEQ_3:27; then
i < len t2 by NAT_1:13; then
i in dom t2 & not emp t2/.i by B3,J4,FINSEQ_3:27; then
len t1 <> i & i <= len t1
by A1,A2,J1,PARTFUN1:def 8,FINSEQ_3:27; then
i < len t1 by XXREAL_0:1; then
1 <= i+1 & i+1 <= len t1 by NAT_1:11,13;
hence i+1 in dom t1 by FINSEQ_3:27;
end;
assume
J3: i+1 in dom t1; then
i+1 <= len t1 & i+1 <= len t2 by JJ,FINSEQ_3:27; then
i < len t1 & i < len t2 by NAT_1:13; then
J5: i in dom t1 & t1/.(i+1) = pop(t1/.i) & i in dom t2 &
t2/.(i+1) = pop(t2/.i) by A3,B3,J4,FINSEQ_3:27; then
t1/.i = t1.i & t2/.i = t2.i & t1/.(i+1) = t1.(i+1) &
t2/.(i+1) = t2.(i+1) by J3,JJ,PARTFUN1:def 8;
hence thesis by J1,J5;
end;
end;
II: P[i] from NAT_1:sch 2(I1,I2);
dom t1 = dom t2
proof
thus dom t1 c= dom t2
proof
let x; thus thesis by II;
end;
let x; thus thesis by II;
end; then
len t1 = len t2 by FINSEQ_3:31;
hence thesis by A2,B2,A4,II;
end;
end;
theorem Th11:
emp s implies core s = s
proof set R = ConstructionRed X;
assume
A0: emp s;
consider t being the carrier' of X-valued RedSequence of R such that
A1: t.1 = s & t.len t = core s and
A2: for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by CORE;
A3: 1 in dom t by FINSEQ_5:6; then
t/.1 = t.1 by PARTFUN1:def 8; then
1 <= len t & len t <= 1 by A0,A1,A2,A3,FINSEQ_3:27;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th12:
core push(e,s) = core s
proof set R = ConstructionRed X;
set A = the carrier' of X;
A0: emp core s by CORE;
consider t being the carrier' of X-valued RedSequence of R such that
A1: t.1 = s & t.len t = core s and
A2: for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by CORE;
not emp push(e,s) & pop push(e,s) = s by POPPUSH,PUSHNE; then
[push(e,s),s] in R by CRED; then
reconsider u = <*push(e,s), s*> as RedSequence of R by REWRITE1:8;
u.2 = s & len u = 2 by FINSEQ_1:61; then
reconsider v = u$^t as RedSequence of R by A1,REWRITE1:9;
A3: v = <*push(e,s)*>^t by REWRITE1:2; then
A4: v.1 = push(e,s) by FINSEQ_1:58; then
reconsider v as A-valued RedSequence of R by Lem2;
A7: len <*push(e,s)*> = 1 by FINSEQ_1:57; then
A5: len v = 1 + len t by A3,FINSEQ_1:35;
len t in dom t by FINSEQ_5:6; then
A6: v.len v = t.len t by A3,A7,A5,FINSEQ_1:def 7;
now let i; assume
B1: 1 <= i & i < len v;
i in NAT by ORDINAL1:def 13; then
i in dom v & i+1 in dom v by B1,MSUALG_8:1; then
B3: v/.i = v.i & v/.(i+1) = v.(i+1) by PARTFUN1:def 8;
consider j such that
B4: i = 1+j by B1,NAT_1:10;
B5: j < len t by A5,B1,B4,XREAL_1:8;
per cases by B1,XXREAL_0:1;
suppose
C1: i = 1;
hence not emp v/.i by A4,B3,PUSHNE;
1 in dom t by FINSEQ_5:6;
hence v/.(i+1) = t.1 by A3,A7,B3,C1,FINSEQ_1:def 7
.= pop(v/.i) by C1,A1,A4,B3,POPPUSH;
end;
suppose i > 1; then
B6: j >= 1 & j in NAT by B4,NAT_1:13,ORDINAL1:def 13; then
j in dom t & i in dom t by B4,B5,MSUALG_8:1; then
t.j = v.i & t/.j = t.j & t.i = v.(i+1) & t/.i = t.i
by A3,A7,B4,FINSEQ_1:def 7,PARTFUN1:def 8;
hence not emp v/.i & v/.(i+1) = pop(v/.i) by A2,B3,B4,B5,B6;
end;
end;
hence thesis by A0,A1,A4,A6,CORE;
end;
theorem Th13:
not emp s implies core pop s = core s
proof set R = ConstructionRed X;
set A = the carrier' of X;
assume
AA: not emp s;
A0: emp core pop s by CORE;
consider t being the carrier' of X-valued RedSequence of R such that
A1: t.1 = pop s & t.len t = core pop s and
A2: for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by CORE;
[s,pop s] in R by AA,CRED; then
reconsider u = <*s, pop s*> as RedSequence of R by REWRITE1:8;
u.2 = pop s & len u = 2 by FINSEQ_1:61; then
reconsider v = u$^t as RedSequence of R by A1,REWRITE1:9;
A3: v = <*s*>^t by REWRITE1:2; then
A4: v.1 = s by FINSEQ_1:58; then
reconsider v as A-valued RedSequence of R by Lem2;
A7: len <*s*> = 1 by FINSEQ_1:57; then
A5: len v = 1 + len t by A3,FINSEQ_1:35;
len t in dom t by FINSEQ_5:6; then
A6: v.len v = t.len t by A3,A7,A5,FINSEQ_1:def 7;
now let i; assume
B1: 1 <= i & i < len v;
i in NAT by ORDINAL1:def 13; then
i in dom v & i+1 in dom v by B1,MSUALG_8:1; then
B3: v/.i = v.i & v/.(i+1) = v.(i+1) by PARTFUN1:def 8;
consider j such that
B4: i = 1+j by B1,NAT_1:10;
B5: j < len t by A5,B1,B4,XREAL_1:8;
per cases by B1,XXREAL_0:1;
suppose
C1: i = 1;
hence not emp v/.i by AA,A3,B3,FINSEQ_1:58;
1 in dom t by FINSEQ_5:6;
hence v/.(i+1) = t.1 by A3,A7,B3,C1,FINSEQ_1:def 7
.= pop(v/.i) by C1,A1,A3,B3,FINSEQ_1:58;
end;
suppose i > 1; then
B6: j >= 1 & j in NAT by B4,NAT_1:13,ORDINAL1:def 13; then
j in dom t & i in dom t by B4,B5,MSUALG_8:1; then
t.j = v.i & t/.j = t.j & t.i = v.(i+1) & t/.i = t.i
by A3,A7,B4,FINSEQ_1:def 7,PARTFUN1:def 8;
hence not emp v/.i & v/.(i+1) = pop(v/.i) by A2,B3,B4,B5,B6;
end;
end;
hence thesis by A0,A1,A4,A6,CORE;
end;
theorem Th59a:
core s in coset s
proof
consider t being the carrier' of X-valued RedSequence of ConstructionRed X
such that
A1: t.1 = s & t.len t = core s and
for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by CORE;
ConstructionRed X reduces s, core s by A1,REWRITE1:def 3; then
core s in {s1: ConstructionRed X reduces s,s1};
hence thesis by Th58;
end;
theorem Th17:
for x being Element of (the carrier of X)*
ex s1 st |.s1.| = x & s1 in coset s
proof set A = the carrier of X;
defpred P[FinSequence of A] means ex s1 st |.s1.| = $1 & s1 in coset s;
emp core s by CORE; then
|.core s.| = {} by Th31; then
A1: P[<*>A] by Th59a;
A2: now
let p be FinSequence of A;
let x be Element of A;
assume P[p]; then
consider s1 such that
A3: |.s1.| = p & s1 in coset s;
thus P[<*x*>^p]
proof
take s2 = push(x,s1);
thus thesis by A3,Th34,COSET;
end;
end;
for p being FinSequence of A holds P[p] from IndSeqD(A1,A2);
hence thesis;
end;
theorem Th14:
s1 in coset s implies core s1 = core s
proof assume
A0: s1 in coset s;
set R = ConstructionRed X;
defpred P[stack of X] means core $1 = core s;
W1: P[s];
coset s = {s2: R reduces s,s2} by Th58; then
ex s2 st s1 = s2 & R reduces s,s2 by A0; then
W2: R reduces s,s1;
W3: now let x,y be stack of X; assume
A2: R reduces s,x & [x,y] in R & P[x]; then
not emp x & y = pop x or ex e st y = push(e,x) by CRED;
hence P[y] by A2,Th12,Th13;
end;
thus P[s1] from PathIND(W1,W2,W3);
end;
theorem Th15:
s1 in coset s & s2 in coset s & |.s1.| = |.s2.| implies s1 = s2
proof
defpred P[stack of X] means
for s2 st $1 in coset s & s2 in coset s & |.$1.| = |.s2.| holds $1 = s2;
A1: for s1 st emp s1 holds P[s1]
proof
let s1; assume
AA: emp s1; then
A2: |.s1.| = {} by Th31;
let s2; assume
s1 in coset s & s2 in coset s & |.s1.| = |.s2.|; then
core s1 = core s & core s2 = core s & emp s2 by A2,Th351,Th14; then
core s = s1 & core s = s2 by AA,Th11;
hence thesis;
end;
A4: now let s1 be stack of X, e be Element of X such that
A5: P[s1];
thus P[push(e,s1)]
proof
let s2; assume
A6: push(e,s1) in coset s & s2 in coset s & |.push(e,s1).| = |.s2.|; then
A8: |.s2.| = <*e*>^|.s1.| by Th34; then
not emp s2 by Th31; then
A7: s2 = push(top s2, pop s2) by PUSHPOP; then
A9: s1 in coset s & pop s2 in coset s by A6,Th53;
|.s2.| = <*top s2*>^|.pop s2.| by A7,Th34; then
e = |.s2.|.1 & |.s2.|.1 = top s2 & |.s1.| = |.pop s2.|
by A8,FINSEQ_1:58,HILBERT2:2;
hence thesis by A5,A7,A9;
end;
end;
P[s1] from INDsch(A1,A4);
hence thesis;
end;
theorem Th60:
ex s st (coset s1)/\Class(==_X, s2) = {s}
proof
consider s such that
A1: |.s.| = |.s2.| & s in coset s1 by Th17;
take s;
thus (coset s1)/\Class(==_X, s2) c= {s}
proof let x; assume
A3: x in (coset s1)/\Class(==_X, s2); then
A2: x in coset s1 & x in Class(==_X, s2) by XBOOLE_0:def 4;
reconsider x as stack of X by A3;
[s2,x] in ==_X by A2,EQREL_1:26; then
s2 == x by REL; then
|.s2.| = |.x.| by CONG; then
s = x by A1,A2,Th15;
hence thesis by TARSKI:def 1;
end;
s == s2 by A1,CONG; then
[s2,s] in ==_X by REL; then
s in Class(==_X, s2) by EQREL_1:26; then
{s} c= Class(==_X, s2) & {s} c= coset s1 by A1,ZFMISC_1:37;
hence thesis by XBOOLE_1:19;
end;
begin :: Quotient Stack System
definition
let X;
func X/== -> strict StackSystem means:
QUOT:
the carrier of it = the carrier of X &
the carrier' of it = Class(==_X) &
the s_empty of it = {the s_empty of X} &
the s_push of it = (the s_push of X)/\/==_X &
the s_pop of it = ((the s_pop of X)+*(id the s_empty of X))/\/==_X &
for f being Choice_Function of Class(==_X) holds the s_top of it
= ((the s_top of X)*f)+*(the s_empty of X,the Element of the carrier of X);
uniqueness
proof let X1,X2 be strict StackSystem such that
A1: the carrier of X1 = the carrier of X &
the carrier' of X1 = Class(==_X) &
the s_empty of X1 = {the s_empty of X} &
the s_push of X1 = (the s_push of X)/\/==_X &
the s_pop of X1 = ((the s_pop of X)+*(id the s_empty of X))/\/==_X and
A2: for f being Choice_Function of Class(==_X) holds the s_top of X1
= ((the s_top of X)*f)+*(the s_empty of X,the Element of the carrier of X)
and
A3: the carrier of X2 = the carrier of X &
the carrier' of X2 = Class(==_X) &
the s_empty of X2 = {the s_empty of X} &
the s_push of X2 = (the s_push of X)/\/==_X &
the s_pop of X2 = ((the s_pop of X)+*(id the s_empty of X))/\/==_X and
A4: for f being Choice_Function of Class(==_X) holds the s_top of X2
= ((the s_top of X)*f)+*(the s_empty of X,the Element of the carrier of X);
set f = the Choice_Function of Class(==_X);
the s_top of X1 = (the s_top of X)*f+*(the s_empty of X,the Element of
the carrier of X) & the s_top of X2 = (the s_top of X)*f+*(the s_empty
of X, the Element of the carrier of X) by A2,A4;
hence thesis by A1,A3;
end;
existence
proof
set f = the Choice_Function of Class(==_X);
A0: union Class(==_X) = the carrier' of X by EQREL_1:def 6; then
reconsider f as Function of Class(==_X), the carrier' of X;
consider s such that
A1: emp s by Th1;
A2: Class(==_X, s) = the s_empty of X by A1,Th50;
reconsider E = Class(==_X, s) as Element of Class(==_X) by EQREL_1:def 5;
set g = (the s_top of X)*f;
take X1 = StackSystem(#the carrier of X, Class(==_X), {E},
(the s_push of X)/\/==_X,
((the s_pop of X)+*(id the s_empty of X))/\/==_X,
g+*(the s_empty of X,the Element of the carrier of X)#);
thus the carrier of X1 = the carrier of X &
the carrier' of X1 = Class(==_X) &
the s_empty of X1 = {the s_empty of X} &
the s_push of X1 = (the s_push of X)/\/==_X &
the s_pop of X1 = ((the s_pop of X)+*(id the s_empty of X))/\/==_X
by A1,Th50;
let h being Choice_Function of Class(==_X);
reconsider h0 = h as Function of Class(==_X), the carrier' of X by A0;
now let a be Element of Class(==_X);
consider s1 such that
A3: a = Class(==_X, s1) by EQREL_1:45;
per cases;
suppose
emp s1; then
s1 in the s_empty of X & dom g = Class(==_X) &
dom((the s_top of X)*h0) = Class(==_X) by EMP,FUNCT_2:def 1; then
A6: a = E & E in dom g & E in dom((the s_top of X)*h0)
by A2,A3,EQREL_1:31; then
g+*(the s_empty of X,the Element of the carrier of X).a =
the Element of the carrier of X by A2,FUNCT_7:33;
hence g+*(the s_empty of X,the Element of the carrier of X).a =
((the s_top of X)*h0+*(the s_empty of X,the Element of the carrier
of X)).a by A2,A6,FUNCT_7:33;
end;
suppose
A4: not emp s1; then s1 nin E by A2,EMP; then
A5: a <> E by A3,EQREL_1:31;
{} nin Class(==_X) by SETFAM_1:def 9; then
f.a in a & h.a in a by ORDERS_1:def 1; then
[s1,f.a] in ==_X & [s1,h.a] in ==_X by A3,EQREL_1:26; then
s1 == f.a & s1 == h0.a by REL; then
f.a == h0.a & not emp f.a by A4,Th41,Th42; then
top(f.a) = top(h0.a) by Th46; then
g.a = top(h0.a) by FUNCT_2:21; then
g.a = ((the s_top of X)*h0).a by FUNCT_2:21; then
g+*(the s_empty of X,the Element of the carrier of X).a =
((the s_top of X)*h0).a by A2,A5,FUNCT_7:34;
hence g+*(the s_empty of X,the Element of the carrier of X).a =
((the s_top of X)*h0+*(the s_empty of X,the Element of the carrier
of X)).a by A2,A5,FUNCT_7:34;
end;
end;
hence the s_top of X1 = (the s_top of X)*h+*(the s_empty of X,the Element
of the carrier of X) by FUNCT_2:113;
end;
end;
registration
let X;
cluster X/== -> non empty non void;
coherence
proof
the carrier of X/== = the carrier of X &
the carrier' of X/== = Class(==_X) by QUOT;
hence thesis;
end;
end;
theorem Th70:
for S being stack of X/== ex s st S = Class(==_X, s)
proof
let S be stack of X/==;
the carrier' of X/== = Class(==_X)by QUOT; then
S in Class(==_X); then
ex x st x in the carrier' of X & S = Class(==_X,x) by EQREL_1:def 5;
hence thesis;
end;
theorem Th70a:
Class(==_X, s) is stack of X/==
proof
the carrier' of X/== = Class(==_X)by QUOT;
hence thesis by EQREL_1:def 5;
end;
theorem Th71:
for S being stack of X/== st S = Class(==_X, s) holds emp s iff emp S
proof
let S be stack of X/==; assume
A1: S = Class(==_X, s);
consider s1 such that
A2: emp s1 by Th1;
emp S iff S in the s_empty of X/== by EMP; then
emp S iff S in {the s_empty of X} by QUOT; then
emp S iff S = the s_empty of X by TARSKI:def 1; then
emp S iff S = Class(==_X, s1) by A2,Th50; then
emp S iff [s,s1] in ==_X by A1,EQREL_1:44; then
emp S iff s == s1 by REL;
hence emp s iff emp S by A2,Th42,Th43;
end;
theorem Th71a:
for S being stack of X/== holds emp S iff S = the s_empty of X
proof let S be stack of X/==;
the carrier' of X/== = Class(==_X)by QUOT; then
S in Class(==_X); then
consider x such that
A1: x in the carrier' of X & S = Class(==_X,x) by EQREL_1:def 5;
reconsider x as stack of X by A1;
hereby assume
emp S; then
emp x by A1,Th71;
hence S = the s_empty of X by A1,Th50;
end;
assume S = the s_empty of X; then
x in the s_empty of X by A1,EQREL_1:28;then
emp x by EMP;
hence thesis by A1,Th71;
end;
theorem Th72:
for S being stack of X/==, E being Element of X/==
st S = Class(==_X, s) & E = e holds
push(e, s) in push(E, S) & Class(==_X, push(e, s)) = push(E, S)
proof
let S be stack of X/==;
let E be Element of X/==;
assume Z0: S = Class(==_X, s);
assume Z1: E = e;
A1: s in S by Z0,EQREL_1:28;
A2: S in Class(==_X) by Z0,EQREL_1:def 5;
A3: the s_push of X is BinOp of the carrier of X,the carrier' of X, ==_X
proof
let x be Element of X,y1,y2 be stack of X;
assume [y1,y2] in ==_X; then
y1 == y2 by REL; then
push(x,y1) == push(x,y2) by Th44;
hence [(the s_push of X).(x,y1),(the s_push of X).(x,y2)] in ==_X
by REL;
end;
push(E,S) = ((the s_push of X)/\/==_X).(E,S) by QUOT
.= Class(==_X, push(e, s)) by Z1,A1,A2,A3,Def4;
hence thesis by EQREL_1:28;
end;
theorem Th73:
for S being stack of X/== st S = Class(==_X, s) & not emp s holds
pop s in pop S & Class(==_X, pop s) = pop S
proof set p = the s_pop of X;
set i = id the s_empty of X;
let S be stack of X/==;
assume
Z0: S = Class(==_X, s);
assume
Z1: not emp s;
A1: s in S by Z0,EQREL_1:28;
A2: S in Class(==_X) by Z0,EQREL_1:def 5;
A6: dom i = the s_empty of X by RELAT_1:71;
A3: p+*i is UnOp of the carrier' of X, ==_X
proof
let y1,y2 be stack of X;
assume
B1: [y1,y2] in ==_X; then
A4: y1 == y2 by REL;
per cases;
suppose
A5: not emp y1; then
not emp y2 by A4,Th42; then
y1 nin the s_empty of X & y2 nin the s_empty of X by A5,EMP; then
A7: (p+*i).y1 = p.y1 & (p+*i).y2 = p.y2 by A6,FUNCT_4:12;
pop y1 == pop y2 by A4,A5,Th45;
hence [(p+*i).y1,(p+*i).y2] in ==_X by A7,REL;
end;
suppose
A5: emp y1; then
emp y2 by A4,Th42; then
y1 in the s_empty of X & y2 in the s_empty of X by A5,EMP; then
(p+*i).y1 = i.y1 & i.y1 = y1 & (p+*i).y2 = i.y2 & i.y2 = y2
by A6,FUNCT_1:35,FUNCT_4:14;
hence thesis by B1;
end;
end;
A8: s nin the s_empty of X by Z1,EMP;
pop S = ((p+*i)/\/==_X).S by QUOT
.= Class(==_X, (p+*i).s) by A1,A2,A3,FILTER_1:def 3
.= Class(==_X, pop s) by A6,A8,FUNCT_4:12;
hence thesis by EQREL_1:28;
end;
theorem Th74:
for S being stack of X/== st S = Class(==_X, s) & not emp s holds
top S = top s
proof set t = the s_top of X;
set A = the s_empty of X;
set e = the Element of the carrier of X;
let S be stack of X/==;
assume
Z0: S = Class(==_X, s);
assume
Z1: not emp s; then
not emp S by Z0,Th71; then
A2: S <> A by Th71a;
set f = the Choice_Function of Class(==_X);
A4: S in Class(==_X) & {} nin Class(==_X)
by Z0,SETFAM_1:def 9,EQREL_1:def 5; then
A3: f.S in S by ORDERS_1:def 1; then
reconsider x = f.S as stack of X by Z0;
[s,x] in ==_X by Z0,A3,EQREL_1:26; then
A6: s == x by REL;
A5: dom f = Class(==_X) by A4,RLVECT_3:35;
the s_top of X/== = (t*f)+*(A,e) by QUOT;
hence top S = (t*f).S by A2,FUNCT_7:34
.= top x by A4,A5,FUNCT_1:23
.= top s by A6,Z1,Th46;
end;
registration
let X;
cluster X/== -> pop-finite;
coherence
proof
let f be Function of NAT, the carrier' of X/==;
set s1 = the stack of X;
defpred P[set,set] means $2 in (coset s1)/\$1;
A1: for x st x in Class(==_X) ex y st y in the carrier' of X & P[x,y]
proof let x; assume
x in Class(==_X); then
consider s2 such that
B2: x = Class(==_X, s2) by EQREL_1:45;
consider s such that
B3: (coset s1)/\Class(==_X, s2) = {s} by Th60;
take s;
thus s in the carrier' of X;
thus s in (coset s1)/\x by B2,B3,TARSKI:def 1;
end;
consider g being Function such that
A2: dom g = Class(==_X) & rng g c= the carrier' of X &
for x st x in Class(==_X) holds P[x,g.x] from WELLORD2:sch 1(A1);
A4: the carrier' of X/== = Class(==_X) by QUOT; then
reconsider g as Function of the carrier' of X/==, the carrier' of X
by A2,FUNCT_2:4;
consider i,s such that
A3: (g*f).i = s & (not emp s implies (g*f).(i+1) <> pop s) by POPFIN;
reconsider S = Class(==_X,s) as stack of X/== by A4,EQREL_1:def 5;
take i,S;
consider s2 such that
A5: f.i = Class(==_X, s2) by A4,EQREL_1:45;
i in NAT by ORDINAL1:def 13; then
s = g.(f.i) by A3,FUNCT_2:21; then
s in (coset s1)/\(f.i) by A2,A4; then
A6: s in coset s1 & s in f.i by XBOOLE_0:def 4;
hence f.i = S by A5,EQREL_1:31;
assume
B2: not emp S; then
A8: not emp s by Th71;
assume
B1: f.(i+1) = pop S; then
A9: f.(i+1) = Class(==_X, pop s) by A8,Th73;
set s3 = g.(f.(i+1));
consider s4 being stack of X such that
A10: (coset s1)/\(f.(i+1)) = {s4} by A9,Th60;
pop s in coset s1 & pop s in pop S & pop S = f.(i+1)
by A6,B1,A8,COSET,Th73; then
A11: pop s in {s4} by A10,XBOOLE_0:def 4;
s3 in (coset s1)/\(f.(i+1)) by A2,A4; then
s3 = s4 & pop s = s4 by A10,A11,TARSKI:def 1;
hence thesis by A3,B2,Th71,FUNCT_2:21;
end;
cluster X/== -> push-pop;
coherence
proof
let S be stack of X/==;
consider s such that
A1: S = Class(==_X, s) by Th70;
assume not emp S; then
A3: not emp s by A1,Th71;
reconsider P = Class(==_X, pop s) as stack of X/== by Th70a;
reconsider E = top s as Element of X/== by QUOT;
thus S = Class(==_X, push(top s, pop s)) by A1,A3,PUSHPOP
.= push(E,P) by Th72
.= push(top S, P) by A1,A3,Th74
.= push(top S, pop S) by A1,A3,Th73;
end;
cluster X/== -> top-push;
coherence
proof
let S be stack of X/==, E be Element of X/==;
consider s such that
A1: S = Class(==_X, s) by Th70;
reconsider e = E as Element of X by QUOT;
reconsider P = Class(==_X, push(e, s)) as stack of X/== by Th70a;
A2: not emp push(e,s) by PUSHNE;
thus E = top push(e,s) by TOPPUSH
.= top P by A2,Th74
.= top push(E, S) by A1,Th72;
end;
cluster X/== -> pop-push;
coherence
proof
let S be stack of X/==, E be Element of X/==;
consider s such that
A1: S = Class(==_X, s) by Th70;
reconsider e = E as Element of X by QUOT;
reconsider P = Class(==_X, push(e, s)) as stack of X/== by Th70a;
A2: not emp push(e,s) by PUSHNE;
thus S = Class(==_X, pop push(e,s)) by A1,POPPUSH
.= pop P by A2,Th73
.= pop push(E, S) by A1,Th72;
end;
cluster X/== -> push-non-empty;
coherence
proof
let S be stack of X/==, E be Element of X/==;
consider s such that
A1: S = Class(==_X, s) by Th70;
reconsider e = E as Element of X by QUOT;
reconsider P = Class(==_X, push(e, s)) as stack of X/== by Th70a;
not emp push(e,s) by PUSHNE; then
not emp P by Th71;
hence thesis by A1,Th72;
end;
end;
theorem Th80:
for S being stack of X/== st S = Class(==_X, s) holds |.S.| = |.s.|
proof
defpred P[stack of X] means
for S being stack of X/== st S = Class(==_X, $1) holds |.S.| = |.$1.|;
A1: emp s1 implies P[s1]
proof assume
B1: emp s1;
let S be stack of X/==; assume
S = Class(==_X, s1); then
emp S by B1,Th71; then
|.S.| = {} by Th31;
hence thesis by B1,Th31;
end;
A2: P[s1] implies P[push(e,s1)]
proof assume
B3: P[s1];
reconsider E = e as Element of X/== by QUOT;
let S be stack of X/==; assume
B4: S = Class(==_X, push(e,s1));
reconsider P = Class(==_X, s1) as stack of X/== by Th70a;
S = push(E,P) by B4,Th72;
hence |.S.| = <*E*>^|.P.| by Th34 .= <*e*>^|.s1.| by B3
.= |.push(e,s1).| by Th34;
end;
thus P[s] from INDsch(A1,A2);
end;
registration
let X;
cluster X/== -> proper-for-identity;
coherence
proof
let S1,S2 be stack of X/==;
consider s1 such that
A1: S1 = Class(==_X, s1) by Th70;
consider s2 such that
A2: S2 = Class(==_X, s2) by Th70;
assume |.S1.| = |.S2.|; then
|.s1.| = |.S2.| by A1,Th80 .= |.s2.| by A2,Th80; then
s1 == s2 by CONG; then
[s1,s2] in ==_X by REL; then
s2 in S1 by A1,EQREL_1:26;
hence thesis by A1,A2,EQREL_1:31;
end;
end;
registration
cluster proper-for-identity StackAlgebra;
existence
proof
take (the StackAlgebra)/==;
thus thesis;
end;
end;
begin :: Representation Theorem for Stacks
definition
let X1,X2 be StackAlgebra;
let F,G be Function;
pred F,G form_isomorphism_between X1,X2 means:
ISO:
dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one &
dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one &
for s1 being stack of X1, s2 being stack of X2 st s2 = G.s1
holds (emp s1 iff emp s2) &
(not emp s1 implies pop s2 = G.pop s1 & top s2 = F.top s1) &
for e1 being Element of X1, e2 being Element of X2 st e2 = F.e1
holds push(e2,s2) = G.push(e1,s1);
end;
reserve X1,X2,X3 for StackAlgebra;
reserve F,F1,F2,G,G1,G2 for Function;
theorem ThI1:
id the carrier of X, id the carrier' of X form_isomorphism_between X,X
proof
set F = id the carrier of X, G = id the carrier' of X;
thus dom F = the carrier of X & rng F = the carrier of X & F is one-to-one
by RELAT_1:71;
thus dom G = the carrier' of X & rng G = the carrier' of X &
G is one-to-one by RELAT_1:71;
let s1 be stack of X, s2 be stack of X; assume
A0: s2 = G.s1; then
A1: s2 = s1 by FUNCT_1:34;
thus emp s1 iff emp s2 by A0,FUNCT_1:34;
thus not emp s1 implies pop s2 = G.pop s1 & top s2 = F.top s1
by A1,FUNCT_1:34;
let e1 be Element of X, e2 be Element of X; assume e2 = F.e1; then
e2 = e1 by FUNCT_1:34;
hence push(e2,s2) = G.push(e1,s1) by A1,FUNCT_1:34;
end;
theorem ThI2:
F,G form_isomorphism_between X1,X2 implies
F",G" form_isomorphism_between X2,X1
proof assume that
A1: dom F = the carrier of X1 & rng F = the carrier of X2 & F is one-to-one and
A2: dom G = the carrier' of X1 & rng G = the carrier' of X2 & G is one-to-one
and
A3: for s1 being stack of X1, s2 being stack of X2 st s2 = G.s1
holds (emp s1 iff emp s2) &
(not emp s1 implies pop s2 = G.pop s1 & top s2 = F.top s1) &
for e1 being Element of X1, e2 being Element of X2 st e2 = F.e1
holds push(e2,s2) = G.push(e1,s1);
thus dom(F") = the carrier of X2 & rng(F") = the carrier of X1 &
F" is one-to-one by A1,FUNCT_1:55;
thus dom(G") = the carrier' of X2 & rng(G") = the carrier' of X1 &
G" is one-to-one by A2,FUNCT_1:55;
let s1 be stack of X2, s2 be stack of X1; assume
s2 = G".s1; then
A6: G.s2 = s1 by A2,FUNCT_1:57;
hence
A5: emp s1 iff emp s2 by A3;
hereby assume not emp s1; then
pop s1 = G.pop s2 & top s1 = F.top s2 by A3,A5,A6;
hence pop s2 = G".pop s1 & top s2 = F".top s1 by A1,A2,FUNCT_1:56;
end;
let e1 be Element of X2, e2 be Element of X1; assume e2 = F".e1; then
F.e2 = e1 by A1,FUNCT_1:57; then
G.push(e2,s2) = push(e1,s1) by A3,A6;
hence thesis by A2,FUNCT_1:56;
end;
theorem Th90:
F1,G1 form_isomorphism_between X1,X2 &
F2,G2 form_isomorphism_between X2,X3 implies
F2*F1,G2*G1 form_isomorphism_between X1,X3
proof assume that
A1: dom F1 = the carrier of X1 & rng F1 = the carrier of X2 &
F1 is one-to-one and
A2: dom G1 = the carrier' of X1 & rng G1 = the carrier' of X2 &
G1 is one-to-one and
A3: for s1 being stack of X1, s2 being stack of X2 st s2 = G1.s1
holds (emp s1 iff emp s2) &
(not emp s1 implies pop s2 = G1.pop s1 & top s2 = F1.top s1) &
for e1 being Element of X1, e2 being Element of X2 st e2 = F1.e1
holds push(e2,s2) = G1.push(e1,s1) and
A4: dom F2 = the carrier of X2 & rng F2 = the carrier of X3 &
F2 is one-to-one and
A5: dom G2 = the carrier' of X2 & rng G2 = the carrier' of X3 &
G2 is one-to-one and
A6: for s1 being stack of X2, s2 being stack of X3 st s2 = G2.s1
holds (emp s1 iff emp s2) &
(not emp s1 implies pop s2 = G2.pop s1 & top s2 = F2.top s1) &
for e1 being Element of X2, e2 being Element of X3 st e2 = F2.e1
holds push(e2,s2) = G2.push(e1,s1);
thus dom(F2*F1) = the carrier of X1 & rng (F2*F1) = the carrier of X3 &
(F2*F1) is one-to-one by A1,A4,RELAT_1:46,47;
thus dom (G2*G1) = the carrier' of X1 & rng (G2*G1) = the carrier' of X3 &
(G2*G1) is one-to-one by A2,A5,RELAT_1:46,47;
let s1 be stack of X1, s2 be stack of X3;
reconsider s3 = G1.s1 as stack of X2 by A2,FUNCT_1:def 5;
assume s2 = (G2*G1).s1; then
A7: s2 = G2.s3 by A2,FUNCT_1:23;
emp s1 iff emp s3 by A3;
hence emp s1 iff emp s2 by A6,A7;
hereby assume not emp s1; then
pop s3 = G1.pop s1 & top s3 = F1.top s1 & not emp s3 by A3; then
pop s2 = G2.(G1.pop s1) & top s2 = F2.(F1.top s1) by A6,A7;
hence pop s2 = (G2*G1).pop s1 & top s2 = (F2*F1).top s1
by A1,A2,FUNCT_1:23;
end;
let e1 be Element of X1, e2 be Element of X3;
reconsider e3 = F1.e1 as Element of X2 by A1,FUNCT_1:def 5;
assume e2 = (F2*F1).e1; then
A8: e2 = F2.e3 by A1,FUNCT_1:23;
push(e3,s3) = G1.push(e1,s1) by A3; then
push(e2,s2) = G2.(G1.push(e1,s1)) by A7,A8,A6;
hence push(e2,s2) = (G2*G1).push(e1,s1) by A2,FUNCT_1:23;
end;
theorem Th97:
F,G form_isomorphism_between X1,X2 implies
for s1 being stack of X1, s2 being stack of X2 st s2 = G.s1
holds |.s2.| = F*|.s1.|
proof
assume that
A1: dom F = the carrier of X1 & rng F = the carrier of X2 &
F is one-to-one and
A2: dom G = the carrier' of X1 & rng G = the carrier' of X2 &
G is one-to-one and
A3: for s1 being stack of X1, s2 being stack of X2 st s2 = G.s1
holds (emp s1 iff emp s2) &
(not emp s1 implies pop s2 = G.pop s1 & top s2 = F.top s1) &
for e1 being Element of X1, e2 being Element of X2 st e2 = F.e1
holds push(e2,s2) = G.push(e1,s1);
reconsider F1 = F as Function of the carrier of X1, the carrier of X2
by A1,FUNCT_2:4;
reconsider G1 = G as Function of the carrier' of X1, the carrier' of X2
by A2,FUNCT_2:4;
let s1 be stack of X1;
defpred P[stack of X1] means
for s2 being stack of X2 st s2 = G.$1 holds |.s2.| = F*|.$1.|;
A4: for s1 being stack of X1 st emp s1 holds P[s1]
proof
let s1 be stack of X1;
assume
C1: emp s1;
let s2 be stack of X2; assume s2 = G.s1;
then emp s2 by A3,C1;
then |.s2.| = {} & |.s1.| = {} by C1,Th31;
hence |.s2.| = F*|.s1.|;
end;
A5: for s1 being stack of X1, e being Element of X1 st P[s1]
holds P[push(e,s1)]
proof
let s1 be stack of X1;
let e be Element of X1;
assume
Z1: P[s1];
let s2 be stack of X2;
Z2: |.G1.s1.| = F*|.s1.| by Z1;
Z3: <*F1.e*> = F*<*e*> by A1,FINSEQ_2:38;
assume s2 = G.push(e,s1); then
s2 = push(F1.e,G1.s1) by A3;
hence |.s2.| = <*F1.e*>^|.G1.s1.| by Th34
.= F*(<*e*>^|.s1.|) by Z2,Z3,FINSEQOP:10
.= F*|.push(e,s1).| by Th34;
end;
thus P[s1] from INDsch(A4,A5);
end;
definition
let X1,X2 be StackAlgebra;
pred X1,X2 are_isomorphic means
ex F,G being Function st F,G form_isomorphism_between X1,X2;
reflexivity
proof let X;
take F = id the carrier of X, G = id the carrier' of X;
thus thesis by ThI1;
end;
symmetry
proof
let X1,X2;
given F,G such that
A1: F,G form_isomorphism_between X1,X2;
take F",G"; thus thesis by A1,ThI2;
end;
end;
theorem
X1,X2 are_isomorphic & X2,X3 are_isomorphic implies X1,X3 are_isomorphic
proof
given F1,G1 such that
A1: F1,G1 form_isomorphism_between X1,X2;
given F2,G2 such that
A2: F2,G2 form_isomorphism_between X2,X3;
take F2*F1, G2*G1;
thus thesis by A1,A2,Th90;
end;
theorem
X1,X2 are_isomorphic & X1 is proper-for-identity implies
X2 is proper-for-identity
proof
given F,G such that
A1: F,G form_isomorphism_between X1,X2;
assume
A2: X1 is proper-for-identity;
let s1,s2 be stack of X2;
A3: dom G = the carrier' of X1 & rng G = the carrier' of X2 by A1,ISO; then
consider q1 being set such that
A4: q1 in dom G & s1 = G.q1 by FUNCT_1:def 5;
consider q2 being set such that
A5: q2 in dom G & s2 = G.q2 by A3,FUNCT_1:def 5;
reconsider q1,q2 as stack of X1 by A1,ISO,A4,A5;
A6: dom F = the carrier of X1 & rng F = the carrier of X2 &
F is one-to-one by A1,ISO;
A7: rng |.q1.| c= the carrier of X1 & rng |.q2.| c= the carrier of X1;
assume |.s1.| = |.s2.|; then
A8: F*|.q1.| = |.s2.| by A1,A4,Th97 .= F*|.q2.| by A1,A5,Th97;
dom (F*|.q1.|) = dom |.q1.| & dom (F*|.q2.|) = dom |.q2.|
by A6,A7,RELAT_1:46; then
|.q1.| = |.q2.| by A6,A7,A8,FUNCT_1:49; then
q1 == q2 by CONG;
hence thesis by A2,A4,A5,PROP;
end;
theorem Th100:
for X being proper-for-identity StackAlgebra holds
ex G st (for s being stack of X holds G.s = |.s.|) &
id the carrier of X, G form_isomorphism_between
X, StandardStackSystem the carrier of X
proof
let X be proper-for-identity StackAlgebra;
deffunc F(stack of X) = |.$1.|;
consider G being Function of the carrier' of X, (the carrier of X)* such
that
A1: for s being stack of X holds G.s = F(s) from FUNCT_2:sch 4;
take G;
thus for s being stack of X holds G.s = |.s.| by A1;
set F = id the carrier of X;
set X2 = StandardStackSystem the carrier of X;
set A = the carrier of X;
A2: the carrier of X2 = A &
the carrier' of X2 = A* &
for s being stack of X2 holds
(emp s iff s is empty) &
for g being FinSequence st g = s holds
(not emp s implies top s = g.1 & pop s = Del(g,1)) &
(emp s implies top s = the Element of X2 & pop s = {}) &
for e being Element of X2 holds push(e,s) = <*e*>^g by EXAM;
thus dom F = the carrier of X & rng F = the carrier of X2 & F is one-to-one
by A2,RELAT_1:71;
thus
A4: dom G = the carrier' of X by FUNCT_2:def 1;
thus rng G = the carrier' of X2
proof
thus rng G c= the carrier' of X2 by A2;
let x; assume x in the carrier' of X2; then
reconsider x as Element of A* by EXAM;
consider s being stack of X such that
A3: |.s.| = x by Th36;
x = G.s by A1,A3;
hence thesis by A4,FUNCT_1:def 5;
end;
thus G is one-to-one
proof
let x,y; assume x in dom G & y in dom G; then
reconsider s1 = x, s2 = y as stack of X;
assume G.x = G.y; then
|.s1.| = G.y by A1 .= |.s2.| by A1; then
s1 == s2 by CONG;
hence x = y by PROP;
end;
let s1 be stack of X, s2 be stack of X2; assume
s2 = G.s1; then
A6: s2 = |.s1.| by A1;
hereby assume emp s1; then
|.s1.| = {} by Th31;
hence emp s2 by A6,EXAM;
end;
thus
A8: now assume emp s2; then
s2 = {} by EXAM;
hence emp s1 by A6,Th351;
end;
hereby assume
A7: not emp s1;
thus pop s2 = Del(s2,1) by A7,A8,EXAM
.= |.pop s1.| by A6,A7,Th33 .= G.pop s1 by A1;
thus top s2 = s2.1 by A7,A8,EXAM
.= top s1 by A6,A7,Th35 .= F.top s1 by FUNCT_1:35;
end;
let e1 be Element of X, e2 be Element of X2; assume e2 = F.e1;
hence push(e2,s2) = <*F.e1*>^s2 by EXAM .= <*e1*>^s2 by FUNCT_1:35
.= |.push(e1,s1).| by A6,Th34 .= G.push(e1,s1) by A1;
end;
theorem
for X being proper-for-identity StackAlgebra holds
X, StandardStackSystem the carrier of X are_isomorphic
proof
let X be proper-for-identity StackAlgebra;
consider G such that
(for s being stack of X holds G.s = |.s.|) and
A2: id the carrier of X, G form_isomorphism_between
X, StandardStackSystem the carrier of X by Th100;
take id the carrier of X, G;
thus thesis by A2;
end;