let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
let s be State of SCM+FSA; for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
let t be FinSequence of INT ; ( (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p implies ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u ) )
set Ba = Bubble-Sort-Algorithm ;
set pp = Initialize ((intloc 0) .--> 1);
set x = (fsloc 0) .--> t;
set z = (IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0);
assume that
A1:
(Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s
and
A2:
Bubble-Sort-Algorithm c= p
; ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
A3:
p +* Bubble-Sort-Algorithm = p
by A2, FUNCT_4:98;
A4:
fsloc 0 in dom ((fsloc 0) .--> t)
by TARSKI:def 1;
then
fsloc 0 in dom ((Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t))
by FUNCT_4:12;
then A5: s . (fsloc 0) =
((Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t)) . (fsloc 0)
by A1, GRFUNC_1:2
.=
((fsloc 0) .--> t) . (fsloc 0)
by A4, FUNCT_4:13
.=
t
by FUNCOP_1:72
;
A6:
s . (fsloc 0),(IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) are_fiberwise_equipotent
by Th26;
reconsider u = (IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) as FinSequence of REAL by FINSEQ_3:117;
take
u
; ( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
thus
t,u are_fiberwise_equipotent
by A5, Th26; ( u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
A7:
dom (s . (fsloc 0)) = dom u
by A6, RFINSEQ:3;
now for i, j being Nat st i in dom u & j in dom u & i < j holds
u . i >= u . jlet i,
j be
Nat;
( i in dom u & j in dom u & i < j implies u . i >= u . j )assume that A8:
i in dom u
and A9:
j in dom u
and A10:
i < j
;
u . i >= u . jA11:
i >= 1
by A8, FINSEQ_3:25;
A12:
j <= len (s . (fsloc 0))
by A7, A9, FINSEQ_3:25;
reconsider y1 =
((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . i as
Integer ;
reconsider y2 =
((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . j as
Integer ;
thus
u . i >= u . j
by A10, A11, A12, Th26;
verum end;
hence
u is non-increasing
by RFINSEQ:19; ( u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
thus
u is FinSequence of INT
; (Result (p,s)) . (fsloc 0) = u
dom (Initialize ((intloc 0) .--> 1)) misses dom ((fsloc 0) .--> t)
by SCMFSA_M:32;
then
Initialize ((intloc 0) .--> 1) c= (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t)
by FUNCT_4:32;
then
s = s +* (Initialize ((intloc 0) .--> 1))
by A1, FUNCT_4:98, XBOOLE_1:1;
then
s = Initialized s
;
hence
(Result (p,s)) . (fsloc 0) = u
by Th20, A3; verum