reconsider s0 = <*> A as Element of A * by FINSEQ_1:def 11;
set E = {s0};
deffunc H1( Element of A, Element of A * ) -> Element of A * = <*$1*> ^ $2;
deffunc H2( Element of A * ) -> Element of A * = Del ($1,1);
deffunc H3( Element of A * ) -> 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) = H1(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 = H2(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 = H3(s)
from FUNCT_2:sch 4();
take X = StackSystem(# A,(A *),{s0},psh,pp,tp #); ( the carrier of X = A & the carrier' of X = A * & ( for s being stack of X holds
( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) ) ) )
thus
( the carrier of X = A & the carrier' of X = A * )
; for s being stack of X holds
( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) )
let s be stack of X; ( ( emp s implies s is empty ) & ( s is empty implies emp s ) & ( 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) ) )
thus A4:
( emp s iff s is empty )
by TARSKI:def 1; 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 X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
let g be FinSequence; ( g = s implies ( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) ) )
assume A5:
g = s
; ( ( not emp s implies ( top s = g . 1 & pop s = Del (g,1) ) ) & ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
then reconsider h = g as Element of A * ;
hereby ( ( emp s implies ( top s = the Element of X & pop s = {} ) ) & ( for e being Element of X holds push (e,s) = <*e*> ^ g ) )
assume A6:
not
emp s
;
( top s = g . 1 & pop s = Del (g,1) )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
;
pop s = Del (g,1)thus
pop s = Del (
g,1)
by A5, A2;
verum
end;
hereby for e being Element of X holds push (e,s) = <*e*> ^ g
assume A8:
emp s
;
( top s = the Element of X & pop 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
;
pop s = {} thus pop s =
Del (
g,1)
by A5, A2
.=
{}
by A4, A5, A8, Th1
;
verum
end;
let e be Element of X; push (e,s) = <*e*> ^ g
thus
push (e,s) = <*e*> ^ g
by A1, A5; verum