:: Representation Theorem for Stacks
:: by Grzegorz Bancerek
::
:: Received February 22, 2011
:: Copyright (c) 2011-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 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, ORDINAL1, NUMBERS, XCMPLX_0, 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, FINSEQOP;
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, FUNCT_4;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, RELAT_2, PARTFUN1, FUNCT_2,
FILTER_1, REWRITE1;
equalities RELAT_1, FINSEQ_1, BINOP_1;
expansions TARSKI, XBOOLE_0, FUNCT_2, BINOP_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, 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, XTUPLE_0;
schemes RELSET_1, NAT_1, FUNCT_2, BINOP_1, RECDEF_1, ALTCAT_1, FUNCT_1,
FINSEQ_1, XFAMILY;
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*; :: redefines ^ (FINSEQ_1, definition)
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*; :: redefines Del (FINSEQ_3, definition)
coherence
proof
rng Del(s,i) c= rng s & rng s c= A by FINSEQ_3:106; then
rng Del(s,i) c= A; then
Del(s,i) is FinSequence of A by FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
end;
theorem Th1:
Del({},i) = {}
proof
dom Del({},i) c= dom {} by WSIERP_1:39;
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 FINSEQ_2:130;
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:
Def1:
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 5;
hence thesis by FUNCT_3:def 5;
end;
end;
scheme LambdaD2{ A,B,C() -> non empty set,
F(object,object) -> 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 2;
rng M c= C()
proof let y be object; assume y in rng M; then
consider x being object such that
A3: x in dom M & y = M.x by FUNCT_1:def 3;
consider x1,x2 being object such that
A4: x1 in A() & x2 in B() & x = [x1,x2] by 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:2;
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
:Def2:
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
for X being set st X in Class R holds X <> {};
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 FUNCT_1:111;
A4: rng g c= D
proof
let x be object;
assume x in rng g;
then consider y being object such that
A5: y in dom g and
A6: x = g.y by FUNCT_1:def 3;
reconsider y as set by TARSKI:1;
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:4;
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
A11: 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,A11;
A12: ex y2 being object st y2 in D & y9 = Class(R,y2) by EQREL_1:def 3;
g.y9 in y by A3;
then [g.y9,y19] in R by A11,A12,EQREL_1:22;
then [b.(x9,g.y9),b.(x9,y19)] in R by A1,Def1;
then
A13: b.(x9,g.y9) in EqClass(R,b.(x9,y19)) by EQREL_1:19;
A14: 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 A13,A14,EQREL_1:23;
end;
uniqueness
proof
let b1,b2 be Function of [:C, Class R:], Class R such that
A15: 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
A16: 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 object such that
A17: y1 in D and
A18: y = Class(R,y1) by EQREL_1:def 3;
b1.(x,y) = Class(R,b.(x,y1)) by A15,A17,A18,EQREL_1:20;
hence b1.(x,y) = b2.(x,y) by A16,A17,A18,EQREL_1:20;
end;
hence thesis;
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; :: redefines +* (FUNCT_4, definition)
coherence
proof per cases;
suppose D = {}; then
A1: g = {};
thus thesis by A1;
end;
suppose
A2: D <> {};
A3: dom(f+*g) = dom f \/ dom g by FUNCT_4:def 1
.= A \/ dom g by FUNCT_2:def 1
.= A \/ C by A2,FUNCT_2:def 1 .= A by XBOOLE_1:12;
A4: rng(f+*g) c= rng f \/ rng g by FUNCT_4:17;
rng f \/ rng g c= B \/ D & B \/ D = B by XBOOLE_1:12,13;
hence thesis by A3,A4,FUNCT_2:2,XBOOLE_1:1;
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 for 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 StackSystem;
let s be stack of X;
pred emp s means s in the s_empty of X;
end;
definition
let X be non void StackSystem;
let s be stack 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;
end;
definition
let X be non empty non void StackSystem;
let s be stack of X;
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:
Def7:
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
A1: 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
A2: 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
A3: 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;
thus
A4: emp s iff s is empty by TARSKI:def 1;
let g be FinSequence; assume
A5: g = s; then
reconsider h = g as Element of A*;
hereby assume
A6: not emp s; then
A7: 1 in dom h by A4,A5,FINSEQ_5:6;
thus top s = IFEQ(s,{}, the Element of A, h/.1) by A3,A5
.= h/.1 by A4,A6,FUNCOP_1:def 8 .= g.1 by A7,PARTFUN1:def 6;
thus pop s = Del(g,1) by A5,A2;
end;
hereby assume
A8: emp s;
thus top s = IFEQ(s,{}, the Element of A, h/.1) by A3,A5
.= the Element of X by A4,A8,FUNCOP_1:def 8;
thus pop s = Del(g,1) by A5,A2 .= {} by A4,A5,A8,Th1;
end;
let e be Element of X;
thus push(e,s) = <*e*>^g by A1,A5;
end;
uniqueness
proof let X1,X2 be non empty non void strict StackSystem such that
A9: the carrier of X1 = A and
A10: the carrier' of X1 = A* and
A11: 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
A12: the carrier of X2 = A and
A13: the carrier' of X2 = A* and
A14: 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 A9;
reconsider e2 = x as Element of X2 by A12;
let y be Element of A*;
reconsider s1 = y as stack of X1 by A10;
reconsider s2 = y as stack of X2 by A13;
thus (the s_push of X1).(x,y) = push(e1,s1)
.= <*x*>^y by A11
.= push(e2,s2) by A14
.= (the s_push of X2).(x,y);
end; then
A15: the s_push of X1 = the s_push of X2 by A9,A10,A12,A13,BINOP_1:2;
now
let x be Element of A*;
reconsider s1 = x as stack of X1 by A10;
reconsider s2 = x as stack of X2 by A13;
per cases;
suppose
A16: not emp s1; then s1 is non empty by A11; then
A17: not emp s2 by A14;
thus (the s_pop of X1).x = pop s1
.= Del(x,1) by A16,A11
.= pop s2 by A17,A14
.= (the s_pop of X2).x;
end;
suppose
A18: emp s1; then s1 is empty by A11; then
A19: emp s2 by A14;
thus (the s_pop of X1).x = pop s1
.= {} by A18,A11
.= pop s2 by A19,A14
.= (the s_pop of X2).x;
end;
end; then
A20: the s_pop of X1 = the s_pop of X2 by A10,A13;
A21: now
let x be Element of A*;
reconsider s1 = x as stack of X1 by A10;
reconsider s2 = x as stack of X2 by A13;
per cases;
suppose
A22: not emp s1; then s1 is non empty by A11; then
A23: not emp s2 by A14;
thus (the s_top of X1).x = top s1
.= x.1 by A22,A11
.= top s2 by A23,A14
.= (the s_top of X2).x;
end;
suppose
A24: emp s1; then s1 is empty by A11; then
A25: emp s2 by A14;
thus (the s_top of X1).x = top s1
.= the Element of A by A9,A24,A11
.= top s2 by A12,A25,A14
.= (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 object; assume
A26: x in the s_empty of X1; then
reconsider s1 = x as stack of X1;
reconsider s2 = s1 as stack of X2 by A10,A13;
emp s1 by A26; then
s1 is empty by A11; then
emp s2 by A14;
hence thesis;
end;
let x be object; assume
A27: x in the s_empty of X2; then
reconsider s2 = x as stack of X2;
reconsider s1 = s2 as stack of X1 by A10,A13;
emp s2 by A27; then
s2 is empty by A14; then
emp s1 by A11;
hence thesis;
end;
hence thesis by A9,A10,A12,A15,A20,A21,FUNCT_2:63;
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 the carrier' of StandardStackSystem A -> functional;
coherence
proof
the carrier' of StandardStackSystem A = A* by Def7;
hence thesis;
end;
end;
registration
let A;
cluster -> FinSequence-like for stack of StandardStackSystem A;
coherence
proof
the carrier' of StandardStackSystem A = A* by Def7;
hence thesis;
end;
end;
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:Def8:
for f being sequence of 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:Def9:
not emp s implies s = push(top s, pop s);
attr X is top-push means:Def10:
e = top push(e,s);
attr X is pop-push means:Def11:
s = pop push(e,s);
attr X is push-non-empty means:Def12:
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 sequence of the carrier' of X such that
A1: 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 Def7;
defpred P[Nat] means
ex i st ex g being Element of A* st g = f.i & $1 = len g;
A2: ex k being Nat st P[k]
proof take k = len g, i = 1, g;
thus thesis;
end;
A3: for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n]
proof let k be Nat;assume
A4: k <> 0; then
consider n0 being Nat such that
A5: k = n0+1 by NAT_1:6;
given i being Nat, g being Element of A* such that
A6: g = f.i & k = len g;
reconsider s = g as stack of X by A6;
reconsider h = pop s as Element of A* by Def7;
take n = len h;
A7: s is non empty by A4,A6; then
not emp s by Def7; then
A8: f.(i+1) = pop s & h = Del(g,1) by A1,A6,Def7;
1 in dom g by A7,FINSEQ_5:6; then
n0 = n by A5,A6,A8,FINSEQ_3:109;
hence thesis by A5,A8,NAT_1:13;
end;
P[0] from NAT_1:sch 7(A2,A3); then
consider i being Nat, g being Element of A* such that
A9: g = f.i & 0 = len g;
reconsider s = g as stack of X by A9;
g is empty & not emp s by A1,A9;
hence thesis by Def7;
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 Def7;
assume
A10: not emp s; then
A11: s is non empty by Def7; then
A12: g = <*g.1*>^Del(g,1) by FINSEQ_5:86;
reconsider h = Del(g,1) as stack of X by Def7;
1 in dom g by A11,FINSEQ_5:6; then
g.1 in A by FUNCT_1:102; then
reconsider x = g.1 as Element of X by Def7;
thus s = push(x, h) by A12,Def7 .= push(top s, h) by A10,Def7
.= push(top s, pop s) by A10,Def7;
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 Def7;
reconsider h = push(e,s) as Element of A* by Def7;
A13: h = <*e*>^g by Def7; then
A14: not emp push(e,s) by Def7;
thus e = h.1 by A13,FINSEQ_1:41 .= top push(e,s) by A14,Def7;
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 Def7;
reconsider h = push(e,s) as Element of A* by Def7;
A15: h = <*e*>^g by Def7; then
A16: not emp push(e,s) by Def7;
thus s = Del(<*e*>^g,1) by WSIERP_1:40 .= pop push(e,s) by A15,A16,Def7;
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 Def7;
push(e,s) = <*e*>^g by Def7;
hence not emp push(e,s) by Def7;
end;
end;
registration
cluster pop-finite push-pop top-push pop-push push-non-empty
strict for non empty non void StackSystem;
existence
proof
take StandardStackSystem the non empty set; 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 Th2:
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
A1: X is pop-finite;
set s1 = the stack of X;
defpred P[set, stack of X, stack of X] means $3 = pop $2;
A2: for n being Nat for x being stack of X
ex y being stack of X st P[n,x,y];
consider f being sequence of the carrier' of X such that
A3: f.0 = s1 & for n being Nat holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A2);
consider i being Nat, s being stack of X such that
A4: f.i = s & (not emp s implies f.(i+1) <> pop s) by A1;
take s;
thus thesis by A3,A4;
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 Th2;
hence thesis;
end;
end;
theorem Th3:
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);
assume X is pop-push; then
s1 = pop push(e1,s1) & s2 = pop push(e2,s2);
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 A1: X is push-pop;
assume not emp s1; then
s1 = push(top s1, pop s1) by A1;
hence thesis by A1;
end;
begin :: Schemes of Induction
scheme
INDsch{X() -> StackAlgebra, s() -> stack of X(), P[set]}:
P[s()]
provided
A1: for s being stack of X() st emp s holds P[s] and
A2: 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;
A3: for n being Nat for x being stack of X()
ex y being stack of X() st Q[n,x,y];
consider f being sequence of the carrier' of X() such that
A4: f.0 = s() & for n being Nat holds Q[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A3);
consider i being Nat, s being stack of X() such that
A5: f.i = s & (not emp s implies f.(i+1) <> pop s) by Def8;
defpred R[Nat] means P[f.(i-'$1)];
i-'0 = i by NAT_D:40; then
A6: R[0] by A5,A4,A1;
A7: now let j be Nat; assume
A8: R[j];
A9: i-'(j+1) = i-'j-'1 by NAT_2:30;
per cases;
suppose i-'j >= 1; then
i-'(j+1)+1 = i-'j by A9,XREAL_1:235; then
f.(i-'j) = pop (f.(i-'(j+1))) by A4; then
not emp f.(i-'(j+1)) implies
f.(i-'(j+1)) = push(top(f.(i-'(j+1))),f.(i-'j)) by Def9;
hence R[j+1] by A1,A2,A8;
end;
suppose
A10: i-'j < 0+1; then
A11: i-'j <= 0 by NAT_1:13;
A12: i-'j = 0 by A10,NAT_1:13;
i-'(j+1) = 0-'1 by A12,NAT_2:30 .= 0 by NAT_2:8;
hence R[j+1] by A8,A11;
end;
end;
for j being Nat holds R[j] from NAT_1:sch 2(A6,A7); then
R[i];
hence thesis by A4,XREAL_1:232;
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 XFAMILY:sch 1;
A2: G[[:the carrier' of X(),A():]] & [:the carrier' of X(),A():] in
bool [:the carrier' of X(),A():] by ZFMISC_1:def 1; then
A3: [:the carrier' of X(),A():] in M by A1;
reconsider M as non empty set by A1,A2;
set F = meet M;
reconsider F as Subset of [:the carrier' of X(),A():] by A3,SETFAM_1:3;
defpred P[stack of X()] means
for y1,y2 being object st [$1,y1] in F & [$1,y2] in F holds y1 = y2;
A4: 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
A5: [s,v] in F;
now let Y be set; assume Y in M; then
G[Y] & [s,v] in Y by A5,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
A7: emp s;
take y = e();
for Y being set st Y in M holds [s,e()] in Y by A7,A1;
hence thesis by SETFAM_1:def 1;
end;
A8: 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
A9: [s,y] in F;
reconsider y as Element of A() by A9,ZFMISC_1:87;
take z = d(e,y);
now let Y be set; assume
A10: Y in M; then
[s,y] in Y by A9,SETFAM_1:def 1;
hence [push(e,s),z] in Y by A10,A1;
end;
hence thesis by SETFAM_1:def 1;
end;
A11: for s being stack of X() st emp s holds P[s]
proof let s be stack of X(); assume
A12: emp s;
let y1,y2 be object; assume
A13: [s,y1] in F & [s,y2] in F;
set Y1 = F \ {[s,y1]}, Y2 = F \ {[s,y2]};
A14: now assume
A15: y1 <> e();
G[Y1]
proof
hereby let s1 be stack of X(); assume emp s1; then
A16: [s1,e()] in F by A4;
[s,y1] <> [s1,e()] by A15,XTUPLE_0:1; then
[s1,e()] nin {[s,y1]} by TARSKI:def 1;
hence [s1,e()] in Y1 by A16,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
A17: [push(a,s1),d(a,v)] in F by A4;
push(a,s1) <> s by A12,Def12; then
[s,y1] <> [push(a,s1),d(a,v)] by XTUPLE_0:1; then
[push(a,s1),d(a,v)] nin {[s,y1]} by TARSKI:def 1;
hence [push(a,s1),d(a,v)] in Y1 by A17,XBOOLE_0:def 5;
end; then
Y1 in M by A1; then
F c= Y1 by SETFAM_1:3; then
[s,y1] in Y1 & [s,y1] in {[s,y1]} by A13,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
now assume
A18: y2 <> e();
G[Y2]
proof
hereby let s1 be stack of X(); assume emp s1; then
A19: [s1,e()] in F by A4;
[s,y2] <> [s1,e()] by A18,XTUPLE_0:1; then
[s1,e()] nin {[s,y2]} by TARSKI:def 1;
hence [s1,e()] in Y2 by A19,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
A20: [push(a,s1),d(a,v)] in F by A4;
push(a,s1) <> s by A12,Def12; then
[s,y2] <> [push(a,s1),d(a,v)] by XTUPLE_0:1; then
[push(a,s1),d(a,v)] nin {[s,y2]} by TARSKI:def 1;
hence [push(a,s1),d(a,v)] in Y2 by A20,XBOOLE_0:def 5;
end; then
Y2 in M by A1; then
F c= Y2 by SETFAM_1:3; then
[s,y2] in Y2 & [s,y2] in {[s,y2]} by A13,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
hence y1 = y2 by A14;
end;
A21: 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
A22: P[s];
let y1,y2 be object;assume
A23: [push(e,s),y1] in F & [push(e,s),y2] in F;
Q[s] from INDsch(A6,A8); then
consider y being set such that
A24: [s,y] in F;
reconsider y as Element of A() by A24,ZFMISC_1:87;
set Y1 = F \ {[push(e,s),y1]}, Y2 = F \ {[push(e,s),y2]};
A25: now assume
A26: y1 <> d(e,y);
G[Y1]
proof
hereby let s1 be stack of X(); assume
A27: emp s1; then
A28: [s1,e()] in F by A4;
not emp push(e,s) by Def12; then
[push(e,s),y1] <> [s1,e()] by A27,XTUPLE_0:1; then
[s1,e()] nin {[push(e,s),y1]} by TARSKI:def 1;
hence [s1,e()] in Y1 by A28,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
A29: [s1,v] in F by XBOOLE_0:def 5; then
A30: [push(a,s1),d(a,v)] in F by A4;
now assume [push(e,s),y1] = [push(a,s1),d(a,v)]; then
A31: push(e,s) = push(a,s1) & y1 = d(a,v) by XTUPLE_0:1; then
e = a & s = s1 by Th3;
hence contradiction by A22,A24,A29,A26,A31;
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 A30,XBOOLE_0:def 5;
end; then
Y1 in M by A1; then
F c= Y1 by SETFAM_1:3; then
[push(e,s),y1] in Y1 & [push(e,s),y1] in {[push(e,s),y1]}
by A23,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
now assume
A32: y2 <> d(e,y);
G[Y2]
proof
hereby let s1 be stack of X(); assume
A33: emp s1; then
A34: [s1,e()] in F by A4;
not emp push(e,s) by Def12; then
[push(e,s),y2] <> [s1,e()] by A33,XTUPLE_0:1; then
[s1,e()] nin {[push(e,s),y2]} by TARSKI:def 1;
hence [s1,e()] in Y2 by A34,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
A35: [s1,v] in F by XBOOLE_0:def 5; then
A36: [push(a,s1),d(a,v)] in F by A4;
now assume [push(e,s),y2] = [push(a,s1),d(a,v)]; then
A37: push(e,s) = push(a,s1) & y2 = d(a,v) by XTUPLE_0:1; then
e = a & s = s1 by Th3;
hence contradiction by A22,A24,A35,A32,A37;
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 A36,XBOOLE_0:def 5;
end; then
Y2 in M by A1; then
F c= Y2 by SETFAM_1:3; then
[push(e,s),y2] in Y2 & [push(e,s),y2] in {[push(e,s),y2]}
by A23,TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5;
end;
hence y1 = y2 by A25;
end;
A38: F is Function-like
proof
let x,y1,y2 be object; assume
A39: [x,y1] in F & [x,y2] in F; then
reconsider x as stack of X() by ZFMISC_1:87;
P[x] from INDsch(A11,A21);
hence thesis by A39;
end;
F is quasi_total
proof
per cases;
case A() <> {};
thus the carrier' of X() c= dom F
proof
let x be object; assume x in the carrier' of X();
then reconsider x as stack of X();
Q[x] from INDsch(A6,A8);
hence thesis by XTUPLE_0:def 12;
end;
thus thesis;
end;
case A() = {};
hence thesis;
end;
end; then
reconsider F as Function of the carrier' of X(),A() by A38;
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 A4;
hence F.s1 = e() by FUNCT_1:1;
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 2; then
[push(e,s1),d(e,F.s1)] in F by A4;
hence F.push(e,s1) = d(e,F.s1) by FUNCT_1:1;
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:
Def13:
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 Th5:
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 Def13;
hence thesis;
end;
theorem Th6:
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 Def13;
A2: |.pop s.| = F.pop s by A1,Def13;
assume not emp s; then
s = push(top s, pop s) by Def9;
hence thesis by A1,A2;
end;
theorem Th7:
not emp s implies |.pop s.| = Del(|.s.|,1)
proof
assume not emp s; then
|.s.| = <*top s*>^|.pop s.| by Th6;
hence thesis by WSIERP_1:40;
end;
theorem Th8:
|.push(e,s).| = <*e*>^|.s.|
proof
not emp push(e,s) by Def12;
hence |.push(e,s).| = <*top push(e,s)*>^|.pop push(e,s).| by Th6
.= <*e*>^|.pop push(e,s).| by Def10
.= <*e*>^|.s.| by Def11;
end;
theorem Th9:
not emp s implies top s = |.s.|.1
proof
assume not emp s; then
|.s.| = <*top s*>^|.pop s.| by Th6;
hence top s = |.s.|.1 by FINSEQ_1:41;
end;
theorem Th10:
|.s.| = {} implies emp s
proof assume |.s.| = {} & not emp s; then
{} = <*top s*>^|.pop s.| by Th6;
hence thesis;
end;
theorem Th11:
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 Def7,Th5;
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 Th8;
hence P[push(e,s)] by Def7;
end;
let s be stack of StandardStackSystem A;
thus P[s] from INDsch(A1,A2);
end;
theorem Th12:
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
A2: emp s by Th2;
take s; thus thesis by A2,Th5;
end;
A3: 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
A4: |.s.| = p;
take s2 = push(x,s);
thus thesis by A4,Th8;
end;
for p being FinSequence of D holds P[p] from IndSeqD(A1,A3);
hence thesis;
end;
definition
let X,s1,s2;
pred s1 == s2 means |.s1.| = |.s2.|;
reflexivity;
symmetry;
end;
theorem
s1 == s2 & s2 == s3 implies s1 == s3;
theorem Th14:
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 Th6;
hence thesis by A1,Th5;
end;
theorem Th15:
emp s1 & emp s2 implies s1 == s2
proof
assume emp s1 & emp s2; then
|.s1.| = {} & |.s2.| = {} by Th5;
hence |.s1.| = |.s2.|;
end;
theorem Th16:
s1 == s2 implies push(e,s1) == push(e,s2)
proof
assume |.s1.| = |.s2.|;
hence |.push(e,s1).| = <*e*>^|.s2.| by Th8 .= |.push(e,s2).| by Th8;
end;
theorem Th17:
s1 == s2 & not emp s1 implies pop s1 == pop s2
proof
assume
A1: s1 == s2 & not emp s1; then
A2: |.s1.| = |.s2.| & not emp s2 by Th14;
thus |.pop s1.| = Del(|.s1.|,1) by A1,Th7 .= |.pop s2.| by A2,Th7;
end;
theorem Th18:
s1 == s2 & not emp s1 implies top s1 = top s2
proof
assume
A1: s1 == s2 & not emp s1; then
A2: |.s1.| = |.s2.| & not emp s2 by Th14;
thus top s1 = |.s1.|.1 by A1,Th9 .= top s2 by A2,Th9;
end;
definition
let X;
attr X is proper-for-identity means:
Def15:
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 Th11 .= s2 by Th11;
end;
end;
definition
let X;
func ==_X -> Relation of the carrier' of X means:
Def16:
[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 be object; assume x in the carrier' of X; then
reconsider s = x as stack of X;
[s,s] in R by Def16;
hence thesis by XTUPLE_0:def 12;
end;
A2: field R = dom R \/ rng R
.= the carrier' of X by A1,XBOOLE_1:12;
thus ==_X is symmetric
proof
let x,y be object; assume
x in field R & y in field R; then
reconsider s1 = x, s2 = y as stack of X by A2;
assume [x,y] in R; then
s1 == s2 by Def16;
hence thesis by Def16;
end;
let x,y,z be object; 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 A2;
assume [x,y] in R & [y,z] in R; then
s1 == s2 & s2 == s3 by Def16; then
s1 == s3;
hence thesis by Def16;
end;
end;
theorem Th19:
emp s implies Class(==_X, s) = the s_empty of X
proof
assume
A1: emp s;
thus Class(==_X, s) c= the s_empty of X
proof
let x be object; assume
A2: x in Class(==_X, s); then
reconsider s1 = x as stack of X;
[s,s1] in ==_X by A2,EQREL_1:18; then
s == s1 by Def16; then
emp s1 by A1,Th14;
hence thesis;
end;
let x be object; assume
A3: x in the s_empty of X; then
reconsider s1 = x as stack of X;
emp s1 by A3; then
s == s1 by A1,Th15; then
[s,s1] in ==_X by Def16;
hence thesis by EQREL_1:18;
end;
definition
let X,s;
func coset s -> Subset of the carrier' of X means:
Def17:
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 XFAMILY:sch 1;
set S = the carrier' of X;
A2: P[the carrier' of X] & S in bool S by ZFMISC_1:def 1; then
A3: the carrier' of X in Y by A1;
reconsider Y as non empty set by A2,A1;
reconsider C = meet Y as Subset of S by A3,SETFAM_1:3;
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
A4: s1 in C;
now let x; assume
A5: x in Y; then
s1 in x by A4,SETFAM_1:def 1;
hence push(e,s1) in x by A1,A5;
end;
hence push(e,s1) in C by SETFAM_1:def 1;
assume
A6: not emp s1;
now let x; assume
A7: x in Y; then
s1 in x by A4,SETFAM_1:def 1;
hence pop s1 in x by A1,A6,A7;
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:3;
end;
uniqueness;
end;
theorem Th20:
(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 Def11,Def12;
hence push(e,s) in coset s1 implies s in coset s1 by Def17;
assume not emp s; then
push(top s, pop s) = s by Def9;
hence thesis by Def17;
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 Def11,Def12,Def17;
hence s in coset push(e,s) by Def17;
assume not emp s; then
push(top s, pop s) = s & pop s in coset pop s by Def9,Def17;
hence thesis by Def17;
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);
A1: for n being Nat for x being stack of X
ex y being stack of X st P[n,x,y];
consider f being sequence of the carrier' of X such that
A2: f.0 = s & for i being Nat holds P[i,f.i,f.(i+1)]
from RECDEF_1:sch 2(A1);
defpred Q[Nat] means f.$1 in coset s;
A3: Q[0] by A2,Def17;
A4: now let i; assume
A5: Q[i];
f.(i+1) = IFIN(f.i,the s_empty of X,s,pop(f.i)) by A2; 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);
hence Q[i+1] by A5,Def17;
end;
A6: Q[i] from NAT_1:sch 2(A3,A4);
consider i,s1 such that
A7: f.i = s1 & (not emp s1 implies f.(i+1) <> pop s1) by Def8;
take s1;
f.(i+1) = IFIN(f.i,the s_empty of X,s,pop(f.i)) by A2; 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 A7,A6;
end;
registration
let A;
let R be Relation of A;
cluster A-valued for RedSequence of R;
existence
proof
set a = the Element of A;
reconsider t = <*a*> as RedSequence of R by REWRITE1:6;
take t; thus thesis;
end;
end;
definition
let X;
func ConstructionRed X -> Relation of the carrier' of X means:
Def18:
[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 Th23:
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:32; then
A1: t.1 in rng t by FUNCT_1:def 3;
hereby
assume
A2: t.1 in A;
defpred P[Nat] means $1 in dom t implies t.$1 in A;
A3: P[0] by FINSEQ_3:24;
A4: P[i] implies P[i+1]
proof assume
P[i]; assume
A5: 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
A6: i = j+1 by A2,A5,NAT_1:6;
i <= i+1 & i+1 <= len t by A5,FINSEQ_3:25,NAT_1:11; then
1 <= i & i <= len t by A6,NAT_1:11,XXREAL_0:2; then
i in dom t by FINSEQ_3:25; then
[t.i, t.(i+1)] in R by A5,REWRITE1:def 2;
hence thesis by A5,ZFMISC_1:87;
end;
A7: P[i] from NAT_1:sch 2(A3,A4);
thus t is A-valued
proof
let x be object; assume x in rng t; then
consider y being object such that
A8: y in dom t & x = t.y by FUNCT_1:def 3;
reconsider y as Nat by A8;
thus thesis by A8,A7;
end;
end;
assume rng t c= A;
hence t.1 in A by A1;
end;
scheme PathIND{X() -> non empty set, x1,x2() -> Element of X(),
R() -> (Relation of X()), P[set]}:
P[x2()]
provided
A1: P[x1()] and
A2: R() reduces x1(),x2() and
A3: 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
A4: t.1 = x1() & t.len t = x2() by A2;
reconsider t as X()-valued RedSequence of R() by A4,Th23;
defpred Q[Nat] means $1 in dom t implies P[t.$1];
A5: Q[0] by FINSEQ_3:24;
A6: now let i; assume
A7: Q[i];
thus Q[i+1]
proof assume
A8: 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
A9: i = j+1 by A1,A4,A8,NAT_1:6;
i <= i+1 & i+1 <= len t by A8,FINSEQ_3:25,NAT_1:11; then
A10: 1 <= i & i <= len t & rng t <> {} by A9,NAT_1:11,XXREAL_0:2; then
A11: i in dom t & 1 in dom t by FINSEQ_3:25,32;
A12: t.i = t/.i & t.(i+1) = t/.(i+1) by A8,A11,PARTFUN1:def 6; then
[t/.i,t/.(i+1)] in R() by A8,A11,REWRITE1:def 2;
hence thesis by A3,A7,A8,A11,A4,A10,A12,REWRITE1:17;
end;
end;
A13: Q[i] from NAT_1:sch 2(A5,A6);
len t in dom t by FINSEQ_5:6;
hence thesis by A4,A13;
end;
theorem Th24:
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
A1: s = t.1; then
reconsider u = t as the carrier' of X-valued RedSequence of R by Th23;
defpred Q[Nat] means $1 in dom t implies t.$1 in coset s;
A2: Q[0] by FINSEQ_3:24;
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 A1,A5,Def17,NAT_1:6;
i <= i+1 & i+1 <= len t by A5,FINSEQ_3:25,NAT_1:11; then
A7: 1 <= i & i <= len t & rng t <> {} by A6,NAT_1:11,XXREAL_0:2; then
A8: i in dom t & 1 in dom t by FINSEQ_3:25,32; then
A9: t.i = u/.i & t.(i+1) = u/.(i+1) by A5,PARTFUN1:def 6; then
[u/.i,u/.(i+1)] in R by A5,A8,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 Def18;
hence thesis by A4,A5,A7,A9,Def17,FINSEQ_3:25;
end;
end;
A10: Q[i] from NAT_1:sch 2(A2,A3);
let x be object; assume x in rng t; then
ex y being object st y in dom t & x = t.y by FUNCT_1:def 3;
hence thesis by A10;
end;
theorem Th25:
coset s = {s1: ConstructionRed X reduces s,s1}
proof set R = ConstructionRed X;
A1: {s1: R reduces s,s1} c= the carrier' of X
proof let x be object;
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:12; then
A2: s in {s1: R reduces s,s1};
now let e,s2; assume
s2 in {s1: R reduces s,s1}; then
A3: ex s1 st s2 = s1 & R reduces s,s1;
[s2, push(e,s2)] in R by Def18; then
R reduces s2, push(e,s2) by REWRITE1:15; then
R reduces s, push(e,s2) by A3,REWRITE1:16;
hence push(e,s2) in {s1: R reduces s,s1};
assume not emp s2; then
[s2, pop s2] in R by Def18; then
R reduces s2, pop s2 by REWRITE1:15; then
R reduces s, pop s2 by A3,REWRITE1:16;
hence pop s2 in {s1: R reduces s,s1};
end;
hence coset s c= {s1: R reduces s,s1} by A1,A2,Def17;
let x be object; assume x in {s1: R reduces s,s1}; then
consider s1 such that
A4: x = s1 & R reduces s,s1;
consider t being RedSequence of R such that
A5: s = t.1 & s1 = t.len t by A4;
len t in dom t by FINSEQ_5:6; then
x in rng t & rng t c= coset s by A4,A5,Th24,FUNCT_1:def 3;
hence thesis;
end;
definition
let X,s;
func core s -> stack of X means:
Def19:
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);
A1: for n being Nat for x being stack of X
ex y being stack of X st P[n,x,y];
consider f being sequence of the carrier' of X such that
A2: f.0 = s & for i being Nat holds P[i,f.i,f.(i+1)]
from RECDEF_1:sch 2(A1);
defpred R[Nat] means
ex s1 st f.$1 = s1 & (not emp s1 implies f.($1+1) <> pop s1);
A3: ex i st R[i] by Def8;
consider i such that
A4: R[i] & for j being Nat st R[j] holds i <= j from NAT_1:sch 5(A3);
deffunc F(Nat) = f.($1-'1);
consider t being FinSequence such that
A5: 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
A6: f.i = s1 & (not emp s1 implies f.(i+1) <> pop s1) by A4;
take s1;
f.(i+1) = IFIN(f.i,the s_empty of X,s,pop(f.i)) by A2; 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 A6;
A7: t is RedSequence of R
proof
thus len t > 0 by A5;
let j being Nat; assume
A8: j in dom t & j+1 in dom t; then
j >= 1 & j <= i+1 & j+1 <= i+1 by A5,FINSEQ_3:25; then
A9: j-'1+1 = j & j+1-'1 = j & j <= i by NAT_D:34,XREAL_1:6,235;
j-'1 < i by A9,NAT_1:13; then
A10: not emp f.(j-'1) by A4; then
A11: f.(j-'1) nin the s_empty of X;
A12: t.j = f.(j-'1) & t.(j+1) = f.j by A5,A8,A9; then
P[j-'1,f.(j-'1),t.(j+1)] by A2,A9; then
t.(j+1) = pop(f.(j-'1)) by A11,MATRIX_7:def 1;
hence [t.j, t.(j+1)] in R by A12,A10,Def18;
end; then
1 in dom t by FINSEQ_5:6; then
A13: t.1 = f.(1-'1) by A5 .= s by A2,XREAL_1:232; then
reconsider t as the carrier' of X-valued RedSequence of R by A7,Th23;
take t;
thus t.1 = s by A13;
len t in dom t by FINSEQ_5:6;
hence t.len t = f.(i+1-'1) by A5 .= s1 by A6,NAT_D:34;
let k be Nat; assume
A14: 1 <= k & k < len t; then
k in dom t by FINSEQ_3:25; then
A15: t.k = f.(k-'1) & t.k = t/.k by A5,PARTFUN1:def 6;
1 <= k+1 & k+1 <= len t by A14,NAT_1:13; then
k+1 in dom t by FINSEQ_3:25; then
A16: t.(k+1) = f.(k+1-'1) & t.(k+1) = t/.(k+1) by A5,PARTFUN1:def 6;
A17: k-'1+1 = k & k+1-'1 = k by A14,NAT_D:34,XREAL_1:235; then
k-'1 < i by A5,A14,XREAL_1:6;
hence not emp t/.k by A4,A15; then
A18: t/.k nin the s_empty of X;
f.k = IFIN(f.(k-'1),the s_empty of X,s,pop(f.(k-'1))) by A2,A17;
hence t/.(k+1) = pop(t/.k) by A15,A16,A17,A18,MATRIX_7:def 1;
end;
uniqueness
proof let x1,x2 be stack of X such that
A19: emp x1;
given t1 being the carrier' of X-valued RedSequence of ConstructionRed X
such that
A20: t1.1 = s & t1.len t1 = x1 and
A21: for i st 1 <= i & i < len t1 holds not emp t1/.i & t1/.(i+1) = pop(t1/.i);
assume
A22: emp x2;
given t2 being the carrier' of X-valued RedSequence of ConstructionRed X
such that
A23: t2.1 = s & t2.len t2 = x2 and
A24: for i st 1 <= i & i < len t2 holds not emp t2/.i & t2/.(i+1) = pop(t2/.i);
A25: 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);
A26: P[0] by FINSEQ_3:24;
A27: P[i] implies P[i+1]
proof assume
A28: P[i];
per cases by NAT_1:6;
suppose i = 0;
hence thesis by A20,A23,FINSEQ_5:6;
end;
suppose ex j st i = j+1; then
consider j such that
A29: i = j+1;
A30: i >= 1 by A29,NAT_1:11;
thus
A31: now assume
i+1 in dom t1; then
i+1 <= len t1 by FINSEQ_3:25; then
i < len t1 by NAT_1:13; then
i in dom t1 & not emp t1/.i by A21,A30,FINSEQ_3:25; then
len t2 <> i & i <= len t2
by A22,A23,A28,FINSEQ_3:25,PARTFUN1:def 6; 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:25;
end;
hereby assume
i+1 in dom t2; then
i+1 <= len t2 by FINSEQ_3:25; then
i < len t2 by NAT_1:13; then
i in dom t2 & not emp t2/.i by A24,A30,FINSEQ_3:25; then
len t1 <> i & i <= len t1
by A19,A20,A28,FINSEQ_3:25,PARTFUN1:def 6; 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:25;
end;
assume
A32: i+1 in dom t1; then
i+1 <= len t1 & i+1 <= len t2 by A31,FINSEQ_3:25; then
i < len t1 & i < len t2 by NAT_1:13; then
A33: i in dom t1 & t1/.(i+1) = pop(t1/.i) & i in dom t2 &
t2/.(i+1) = pop(t2/.i) by A21,A24,A30,FINSEQ_3:25; then
t1/.i = t1.i & t2/.i = t2.i & t1/.(i+1) = t1.(i+1) &
t2/.(i+1) = t2.(i+1) by A32,A31,PARTFUN1:def 6;
hence thesis by A28,A33;
end;
end;
A34: P[i] from NAT_1:sch 2(A26,A27);
dom t1 = dom t2
proof
thus dom t1 c= dom t2
by A34;
let x be object; thus thesis by A34;
end; then
len t1 = len t2 by FINSEQ_3:29;
hence thesis by A20,A23,A25,A34;
end;
end;
theorem Th26:
emp s implies core s = s
proof set R = ConstructionRed X;
assume
A1: emp s;
consider t being the carrier' of X-valued RedSequence of R such that
A2: t.1 = s & t.len t = core s and
A3: for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by Def19;
A4: 1 in dom t by FINSEQ_5:6; then
t/.1 = t.1 by PARTFUN1:def 6; then
1 <= len t & len t <= 1 by A1,A2,A3,A4,FINSEQ_3:25;
hence thesis by A2,XXREAL_0:1;
end;
theorem Th27:
core push(e,s) = core s
proof set R = ConstructionRed X;
set A = the carrier' of X;
A1: emp core s by Def19;
consider t being the carrier' of X-valued RedSequence of R such that
A2: t.1 = s & t.len t = core s and
A3: for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by Def19;
not emp push(e,s) & pop push(e,s) = s by Def11,Def12; then
[push(e,s),s] in R by Def18; then
reconsider u = <*push(e,s), s*> as RedSequence of R by REWRITE1:7;
u.2 = s & len u = 2 by FINSEQ_1:44; then
reconsider v = u$^t as RedSequence of R by A2,REWRITE1:8;
A4: v = <*push(e,s)*>^t by REWRITE1:2; then
A5: v.1 = push(e,s) by FINSEQ_1:41; then
reconsider v as A-valued RedSequence of R by Th23;
A6: len <*push(e,s)*> = 1 by FINSEQ_1:40; then
A7: len v = 1 + len t by A4,FINSEQ_1:22;
len t in dom t by FINSEQ_5:6; then
A8: v.len v = t.len t by A4,A6,A7,FINSEQ_1:def 7;
now let i; assume
A9: 1 <= i & i < len v;
i in dom v & i+1 in dom v by A9,MSUALG_8:1; then
A10: v/.i = v.i & v/.(i+1) = v.(i+1) by PARTFUN1:def 6;
consider j such that
A11: i = 1+j by A9,NAT_1:10;
A12: j < len t by A7,A9,A11,XREAL_1:6;
per cases by A9,XXREAL_0:1;
suppose
A13: i = 1;
hence not emp v/.i by A5,A10,Def12;
1 in dom t by FINSEQ_5:6;
hence v/.(i+1) = t.1 by A4,A6,A10,A13,FINSEQ_1:def 7
.= pop(v/.i) by A13,A2,A5,A10,Def11;
end;
suppose i > 1; then
A14: j >= 1 & j in NAT by A11,NAT_1:13,ORDINAL1:def 12; then
j in dom t & i in dom t by A11,A12,MSUALG_8:1; then
t.j = v.i & t/.j = t.j & t.i = v.(i+1) & t/.i = t.i
by A4,A6,A11,FINSEQ_1:def 7,PARTFUN1:def 6;
hence not emp v/.i & v/.(i+1) = pop(v/.i) by A3,A10,A11,A12,A14;
end;
end;
hence thesis by A1,A2,A5,A8,Def19;
end;
theorem Th28:
not emp s implies core pop s = core s
proof set R = ConstructionRed X;
set A = the carrier' of X;
assume
A1: not emp s;
A2: emp core pop s by Def19;
consider t being the carrier' of X-valued RedSequence of R such that
A3: t.1 = pop s & t.len t = core pop s and
A4: for i st 1 <= i & i < len t holds not emp t/.i & t/.(i+1) = pop(t/.i)
by Def19;
[s,pop s] in R by A1,Def18; then
reconsider u = <*s, pop s*> as RedSequence of R by REWRITE1:7;
u.2 = pop s & len u = 2 by FINSEQ_1:44; then
reconsider v = u$^t as RedSequence of R by A3,REWRITE1:8;
A5: v = <*s*>^t by REWRITE1:2; then
A6: v.1 = s by FINSEQ_1:41; then
reconsider v as A-valued RedSequence of R by Th23;
A7: len <*s*> = 1 by FINSEQ_1:40; then
A8: len v = 1 + len t by A5,FINSEQ_1:22;
len t in dom t by FINSEQ_5:6; then
A9: v.len v = t.len t by A5,A7,A8,FINSEQ_1:def 7;
now let i; assume
A10: 1 <= i & i < len v;
i in dom v & i+1 in dom v by A10,MSUALG_8:1; then
A11: v/.i = v.i & v/.(i+1) = v.(i+1) by PARTFUN1:def 6;
consider j such that
A12: i = 1+j by A10,NAT_1:10;
A13: j < len t by A8,A10,A12,XREAL_1:6;
per cases by A10,XXREAL_0:1;
suppose
A14: i = 1;
hence not emp v/.i by A1,A5,A11,FINSEQ_1:41;
1 in dom t by FINSEQ_5:6;
hence v/.(i+1) = t.1 by A5,A7,A11,A14,FINSEQ_1:def 7
.= pop(v/.i) by A14,A3,A5,A11,FINSEQ_1:41;
end;
suppose i > 1; then
A15: j >= 1 & j in NAT by A12,NAT_1:13,ORDINAL1:def 12; then
j in dom t & i in dom t by A12,A13,MSUALG_8:1; then
t.j = v.i & t/.j = t.j & t.i = v.(i+1) & t/.i = t.i
by A5,A7,A12,FINSEQ_1:def 7,PARTFUN1:def 6;
hence not emp v/.i & v/.(i+1) = pop(v/.i) by A4,A11,A12,A13,A15;
end;
end;
hence thesis by A2,A3,A6,A9,Def19;
end;
theorem Th29:
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 Def19;
ConstructionRed X reduces s, core s by A1; then
core s in {s1: ConstructionRed X reduces s,s1};
hence thesis by Th25;
end;
theorem Th30:
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 Def19; then
|.core s.| = {} by Th5; then
A1: P[<*>A] by Th29;
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,Th8,Def17;
end;
end;
for p being FinSequence of A holds P[p] from IndSeqD(A1,A2);
hence thesis;
end;
theorem Th31:
s1 in coset s implies core s1 = core s
proof assume
A1: s1 in coset s;
set R = ConstructionRed X;
defpred P[stack of X] means core $1 = core s;
A2: P[s];
coset s = {s2: R reduces s,s2} by Th25; then
ex s2 st s1 = s2 & R reduces s,s2 by A1; then
A3: R reduces s,s1;
A4: now let x,y be stack of X; assume
A5: 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 Def18;
hence P[y] by A5,Th27,Th28;
end;
thus P[s1] from PathIND(A2,A3,A4);
end;
theorem Th32:
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
A2: emp s1; then
A3: |.s1.| = {} by Th5;
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 A3,Th10,Th31; then
core s = s1 & core s = s2 by A2,Th26;
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
A7: |.s2.| = <*e*>^|.s1.| by Th8; then
not emp s2 by Th5; then
A8: s2 = push(top s2, pop s2) by Def9; then
A9: s1 in coset s & pop s2 in coset s by A6,Th20;
|.s2.| = <*top s2*>^|.pop s2.| by A8,Th8; then
e = |.s2.|.1 & |.s2.|.1 = top s2 & |.s1.| = |.pop s2.|
by A7,FINSEQ_1:41,HILBERT2:2;
hence thesis by A5,A8,A9;
end;
end;
P[s1] from INDsch(A1,A4);
hence thesis;
end;
theorem Th33:
ex s st (coset s1)/\Class(==_X, s2) = {s}
proof
consider s such that
A1: |.s.| = |.s2.| & s in coset s1 by Th30;
take s;
thus (coset s1)/\Class(==_X, s2) c= {s}
proof let x be object; assume
A2: x in (coset s1)/\Class(==_X, s2); then
A3: x in coset s1 & x in Class(==_X, s2) by XBOOLE_0:def 4;
reconsider x as stack of X by A2;
[s2,x] in ==_X by A3,EQREL_1:18; then
s2 == x by Def16; then
|.s2.| = |.x.|; then
s = x by A1,A3,Th32;
hence thesis by TARSKI:def 1;
end;
s == s2 by A1; then
[s2,s] in ==_X by Def16; then
s in Class(==_X, s2) by EQREL_1:18; then
{s} c= Class(==_X, s2) & {s} c= coset s1 by A1,ZFMISC_1:31;
hence thesis by XBOOLE_1:19;
end;
begin :: Quotient Stack System
definition
let X;
func X/== -> strict StackSystem means:
Def20:
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);
not {} in Class(==_X);
then
A5: f is Function of Class(==_X), union Class(==_X) by ORDERS_1:90;
A6: union Class(==_X) = the carrier' of X by EQREL_1:def 4; then
reconsider f as Function of Class(==_X), the carrier' of X by A5;
consider s such that
A7: emp s by Th2;
A8: Class(==_X, s) = the s_empty of X by A7,Th19;
reconsider E = Class(==_X, s) as Element of Class(==_X) by EQREL_1:def 3;
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 A7,Th19;
let h being Choice_Function of Class(==_X);
not {} in Class(==_X);
then
h is Function of Class(==_X), union Class(==_X) by ORDERS_1:90;
then reconsider h0 = h as Function of Class(==_X), the carrier' of X by A6;
now let a be Element of Class(==_X);
consider s1 such that
A9: a = Class(==_X, s1) by EQREL_1:36;
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 FUNCT_2:def 1; then
A10: a = E & E in dom g & E in dom((the s_top of X)*h0)
by A8,A9,EQREL_1:23; then
g+*(the s_empty of X,the Element of the carrier of X).a =
the Element of the carrier of X by A8,FUNCT_7:31;
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 A8,A10,FUNCT_7:31;
end;
suppose
A11: not emp s1; then s1 nin E by A8; then
A12: a <> E by A9,EQREL_1:23;
{} nin Class(==_X); then
f.a in a & h.a in a by ORDERS_1:89; then
[s1,f.a] in ==_X & [s1,h.a] in ==_X by A9,EQREL_1:18; then
s1 == f.a & s1 == h0.a by Def16; then
f.a == h0.a & not emp f.a by A11,Th14; then
top(f.a) = top(h0.a) by Th18; then
g.a = top(h0.a) by FUNCT_2:15; then
g.a = ((the s_top of X)*h0).a by FUNCT_2:15; then
g+*(the s_empty of X,the Element of the carrier of X).a =
((the s_top of X)*h0).a by A8,A12,FUNCT_7:32;
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 A8,A12,FUNCT_7:32;
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:63;
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 Def20;
hence thesis;
end;
end;
theorem Th34:
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 Def20; then
S in Class(==_X); then
ex x being object
st x in the carrier' of X & S = Class(==_X,x) by EQREL_1:def 3;
hence thesis;
end;
theorem Th35:
Class(==_X, s) is stack of X/==
proof
the carrier' of X/== = Class(==_X)by Def20;
hence thesis by EQREL_1:def 3;
end;
theorem Th36:
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 Th2;
emp S iff S in {the s_empty of X} by Def20; then
emp S iff S = the s_empty of X by TARSKI:def 1; then
emp S iff S = Class(==_X, s1) by A2,Th19; then
emp S iff [s,s1] in ==_X by A1,EQREL_1:35; then
emp S iff s == s1 by Def16;
hence emp s iff emp S by A2,Th14,Th15;
end;
theorem Th37:
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 Def20; then
S in Class(==_X); then
consider x being object such that
A1: x in the carrier' of X & S = Class(==_X,x) by EQREL_1:def 3;
reconsider x as stack of X by A1;
hereby assume
emp S; then
emp x by A1,Th36;
hence S = the s_empty of X by A1,Th19;
end;
assume S = the s_empty of X; then
x in the s_empty of X by A1,EQREL_1:20;then
emp x;
hence thesis by A1,Th36;
end;
theorem Th38:
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 A1: S = Class(==_X, s);
assume A2: E = e;
A3: s in S by A1,EQREL_1:20;
A4: S in Class(==_X) by A1,EQREL_1:def 3;
A5: 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 Def16; then
push(x,y1) == push(x,y2) by Th16;
hence [(the s_push of X).(x,y1),(the s_push of X).(x,y2)] in ==_X
by Def16;
end;
push(E,S) = ((the s_push of X)/\/==_X).(E,S) by Def20
.= Class(==_X, push(e, s)) by A2,A3,A4,A5,Def2;
hence thesis by EQREL_1:20;
end;
theorem Th39:
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
A1: S = Class(==_X, s);
assume
A2: not emp s;
A3: s in S by A1,EQREL_1:20;
A4: S in Class(==_X) by A1,EQREL_1:def 3;
A5: dom i = the s_empty of X;
A6: p+*i is UnOp of the carrier' of X, ==_X
proof
let y1,y2 be stack of X;
assume
A7: [y1,y2] in ==_X; then
A8: y1 == y2 by Def16;
per cases;
suppose
A9: not emp y1; then
not emp y2 by A8,Th14; then
y1 nin the s_empty of X & y2 nin the s_empty of X by A9; then
A10: (p+*i).y1 = p.y1 & (p+*i).y2 = p.y2 by A5,FUNCT_4:11;
pop y1 == pop y2 by A8,A9,Th17;
hence [(p+*i).y1,(p+*i).y2] in ==_X by A10,Def16;
end;
suppose
A11: emp y1; then
emp y2 by A8,Th14; then
y1 in the s_empty of X & y2 in the s_empty of X by A11; then
(p+*i).y1 = i.y1 & i.y1 = y1 & (p+*i).y2 = i.y2 & i.y2 = y2
by A5,FUNCT_1:18,FUNCT_4:13;
hence thesis by A7;
end;
end;
A12: s nin the s_empty of X by A2;
pop S = ((p+*i)/\/==_X).S by Def20
.= Class(==_X, (p+*i).s) by A3,A4,A6,FILTER_1:def 3
.= Class(==_X, pop s) by A5,A12,FUNCT_4:11;
hence thesis by EQREL_1:20;
end;
theorem Th40:
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
A1: S = Class(==_X, s);
assume
A2: not emp s; then
not emp S by A1,Th36; then
A3: S <> A by Th37;
set f = the Choice_Function of Class(==_X);
A4: S in Class(==_X) & {} nin Class(==_X)
by A1,EQREL_1:def 3; then
A5: f.S in S by ORDERS_1:89; then
reconsider x = f.S as stack of X by A1;
[s,x] in ==_X by A1,A5,EQREL_1:18; then
A6: s == x by Def16;
A7: dom f = Class(==_X) by A4,RLVECT_3:28;
the s_top of X/== = (t*f)+*(A,e) by Def20;
hence top S = (t*f).S by A3,FUNCT_7:32
.= top x by A4,A7,FUNCT_1:13
.= top s by A6,A2,Th18;
end;
registration
let X;
cluster X/== -> pop-finite;
coherence
proof
let f be sequence of the carrier' of X/==;
set s1 = the stack of X;
defpred P[object,object] means
ex B being set st B = $1 & $2 in (coset s1)/\B;
A1: for x being object st x in Class(==_X)
ex y being object st y in the carrier' of X & P[x,y]
proof let x be object; assume
x in Class(==_X); then
consider s2 such that
A2: x = Class(==_X, s2) by EQREL_1:36;
consider s such that
A3: (coset s1)/\Class(==_X, s2) = {s} by Th33;
take s;
thus s in the carrier' of X;
reconsider B = x as set by TARSKI:1;
take B;
thus B = x;
thus s in (coset s1)/\B by A2,A3,TARSKI:def 1;
end;
consider g being Function such that
A4: dom g = Class(==_X) & rng g c= the carrier' of X &
for x being object st x in Class(==_X) holds P[x,g.x]
from FUNCT_1:sch 6(A1);
A5: the carrier' of X/== = Class(==_X) by Def20; then
reconsider g as Function of the carrier' of X/==, the carrier' of X
by A4,FUNCT_2:2;
consider i,s such that
A6: (g*f).i = s & (not emp s implies (g*f).(i+1) <> pop s) by Def8;
reconsider S = Class(==_X,s) as stack of X/== by A5,EQREL_1:def 3;
take i,S;
consider s2 such that
A7: f.i = Class(==_X, s2) by A5,EQREL_1:36;
i in NAT by ORDINAL1:def 12; then
A8: s = g.(f.i) by A6,FUNCT_2:15;
P[f.i,g.(f.i)] by A4,A5;
then s in (coset s1)/\(f.i) by A8; then
A9: s in coset s1 & s in f.i by XBOOLE_0:def 4;
hence f.i = S by A7,EQREL_1:23;
assume
A10: not emp S; then
A11: not emp s by Th36;
assume
A12: f.(i+1) = pop S; then
A13: f.(i+1) = Class(==_X, pop s) by A11,Th39;
set s3 = g.(f.(i+1));
consider s4 being stack of X such that
A14: (coset s1)/\(f.(i+1)) = {s4} by A13,Th33;
pop s in coset s1 & pop s in pop S & pop S = f.(i+1)
by A9,A12,A11,Def17,Th39; then
A15: pop s in {s4} by A14,XBOOLE_0:def 4;
P[f.(i+1),g.(f.(i+1))] by A4,A5;
then s3 in (coset s1)/\(f.(i+1)); then
s3 = s4 & pop s = s4 by A14,A15,TARSKI:def 1;
hence thesis by A6,A10,Th36,FUNCT_2:15;
end;
cluster X/== -> push-pop;
coherence
proof
let S be stack of X/==;
consider s such that
A16: S = Class(==_X, s) by Th34;
assume not emp S; then
A17: not emp s by A16,Th36;
reconsider P = Class(==_X, pop s) as stack of X/== by Th35;
reconsider E = top s as Element of X/== by Def20;
thus S = Class(==_X, push(top s, pop s)) by A16,A17,Def9
.= push(E,P) by Th38
.= push(top S, P) by A16,A17,Th40
.= push(top S, pop S) by A16,A17,Th39;
end;
cluster X/== -> top-push;
coherence
proof
let S be stack of X/==, E be Element of X/==;
consider s such that
A18: S = Class(==_X, s) by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class(==_X, push(e, s)) as stack of X/== by Th35;
A19: not emp push(e,s) by Def12;
thus E = top push(e,s) by Def10
.= top P by A19,Th40
.= top push(E, S) by A18,Th38;
end;
cluster X/== -> pop-push;
coherence
proof
let S be stack of X/==, E be Element of X/==;
consider s such that
A20: S = Class(==_X, s) by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class(==_X, push(e, s)) as stack of X/== by Th35;
A21: not emp push(e,s) by Def12;
thus S = Class(==_X, pop push(e,s)) by A20,Def11
.= pop P by A21,Th39
.= pop push(E, S) by A20,Th38;
end;
cluster X/== -> push-non-empty;
coherence
proof
let S be stack of X/==, E be Element of X/==;
consider s such that
A22: S = Class(==_X, s) by Th34;
reconsider e = E as Element of X by Def20;
reconsider P = Class(==_X, push(e, s)) as stack of X/== by Th35;
not emp push(e,s) by Def12; then
not emp P by Th36;
hence thesis by A22,Th38;
end;
end;
theorem Th41:
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
A2: emp s1;
let S be stack of X/==; assume
S = Class(==_X, s1); then
emp S by A2,Th36; then
|.S.| = {} by Th5;
hence thesis by A2,Th5;
end;
A3: P[s1] implies P[push(e,s1)]
proof assume
A4: P[s1];
reconsider E = e as Element of X/== by Def20;
let S be stack of X/==; assume
A5: S = Class(==_X, push(e,s1));
reconsider P = Class(==_X, s1) as stack of X/== by Th35;
S = push(E,P) by A5,Th38;
hence |.S.| = <*E*>^|.P.| by Th8 .= <*e*>^|.s1.| by A4
.= |.push(e,s1).| by Th8;
end;
thus P[s] from INDsch(A1,A3);
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 Th34;
consider s2 such that
A2: S2 = Class(==_X, s2) by Th34;
assume |.S1.| = |.S2.|; then
|.s1.| = |.S2.| by A1,Th41 .= |.s2.| by A2,Th41; then
s1 == s2; then
[s1,s2] in ==_X by Def16; then
s2 in S1 by A1,EQREL_1:18;
hence thesis by A1,A2,EQREL_1:23;
end;
end;
registration
cluster proper-for-identity for 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
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
id the carrier of X, id the carrier' of X form_isomorphism_between X,X;
theorem Th43:
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:33;
thus dom(G") = the carrier' of X2 & rng(G") = the carrier' of X1 &
G" is one-to-one by A2,FUNCT_1:33;
let s1 be stack of X2, s2 be stack of X1; assume
s2 = G".s1; then
A4: G.s2 = s1 by A2,FUNCT_1:35;
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,A4;
hence pop s2 = G".pop s1 & top s2 = F".top s1 by A1,A2,FUNCT_1:34;
end;
let e1 be Element of X2, e2 be Element of X1; assume e2 = F".e1; then
F.e2 = e1 by A1,FUNCT_1:35; then
G.push(e2,s2) = push(e1,s1) by A3,A4;
hence thesis by A2,FUNCT_1:34;
end;
theorem Th44:
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:27,28;
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:27,28;
let s1 be stack of X1, s2 be stack of X3;
reconsider s3 = G1.s1 as stack of X2 by A2,FUNCT_1:def 3;
assume s2 = (G2*G1).s1; then
A7: s2 = G2.s3 by A2,FUNCT_1:13;
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:13;
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 3;
assume e2 = (F2*F1).e1; then
A8: e2 = F2.e3 by A1,FUNCT_1:13;
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:13;
end;
theorem Th45:
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:2;
reconsider G1 = G as Function of the carrier' of X1, the carrier' of X2
by A2,FUNCT_2:2;
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
A5: emp s1;
let s2 be stack of X2; assume s2 = G.s1;
then emp s2 by A3,A5;
then |.s2.| = {} & |.s1.| = {} by A5,Th5;
hence |.s2.| = F*|.s1.|;
end;
A6: 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
A7: P[s1];
let s2 be stack of X2;
A8: |.G1.s1.| = F*|.s1.| by A7;
A9: <*F1.e*> = F*<*e*> by A1,FINSEQ_2:34;
assume s2 = G.push(e,s1); then
s2 = push(F1.e,G1.s1) by A3;
hence |.s2.| = <*F1.e*>^|.G1.s1.| by Th8
.= F*(<*e*>^|.s1.|) by A8,A9,FINSEQOP:9
.= F*|.push(e,s1).| by Th8;
end;
thus P[s1] from INDsch(A4,A6);
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;
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,Th43;
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,Th44;
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; then
consider q1 being object such that
A4: q1 in dom G & s1 = G.q1 by FUNCT_1:def 3;
consider q2 being object such that
A5: q2 in dom G & s2 = G.q2 by A3,FUNCT_1:def 3;
reconsider q1,q2 as stack of X1 by A1,A4,A5;
A6: dom F = the carrier of X1 & rng F = the carrier of X2 &
F is one-to-one by A1;
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,Th45 .= F*|.q2.| by A1,A5,Th45;
dom (F*|.q1.|) = dom |.q1.| & dom (F*|.q2.|) = dom |.q2.|
by A6,A7,RELAT_1:27; then
|.q1.| = |.q2.| by A6,A7,A8,FUNCT_1:27; then
q1 == q2;
hence thesis by A2,A4,A5;
end;
theorem Th48:
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 Def7;
thus dom F = the carrier of X & rng F = the carrier of X2 & F is one-to-one
by A2;
thus
A3: 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 be object; assume x in the carrier' of X2; then
reconsider x as Element of A* by Def7;
consider s being stack of X such that
A4: |.s.| = x by Th12;
x = G.s by A1,A4;
hence thesis by A3,FUNCT_1:def 3;
end;
thus G is one-to-one
proof
let x,y be object; 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;
hence x = y by Def15;
end;
let s1 be stack of X, s2 be stack of X2; assume
s2 = G.s1; then
A5: s2 = |.s1.| by A1;
hereby assume emp s1; then
|.s1.| = {} by Th5;
hence emp s2 by A5,Def7;
end;
thus
A6: now assume emp s2; then
s2 = {} by Def7;
hence emp s1 by A5,Th10;
end;
hereby assume
A7: not emp s1;
hence pop s2 = Del(s2,1) by A6,Def7
.= |.pop s1.| by A5,A7,Th7 .= G.pop s1 by A1;
thus top s2 = s2.1 by A7,A6,Def7
.= top s1 by A5,A7,Th9 .= F.top s1;
end;
let e1 be Element of X, e2 be Element of X2; assume e2 = F.e1;
hence push(e2,s2) = <*F.e1*>^s2 by Def7 .= <*e1*>^s2
.= |.push(e1,s1).| by A5,Th8 .= 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
A1: id the carrier of X, G form_isomorphism_between
X, StandardStackSystem the carrier of X by Th48;
take id the carrier of X, G;
thus thesis by A1;
end;