set Ba = Bubble-Sort-Algorithm ;
set Ib = Initialized Bubble-Sort-Algorithm;
let i be Element of NAT ; :: thesis: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Bubble-Sort-Algorithm c= P holds
for w being FinSequence of INT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st Bubble-Sort-Algorithm c= P holds
for w being FinSequence of INT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( Bubble-Sort-Algorithm c= P implies for w being FinSequence of INT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm )
assume A1: Bubble-Sort-Algorithm c= P ; :: thesis: for w being FinSequence of INT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s holds
IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
let w be FinSequence of INT ; :: thesis: ( NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s implies IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm )
set x = (fsloc 0) .--> w;
assume A2: NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s ; :: thesis: IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
x3: dom (NPP ((fsloc 0) .--> w)) c= dom ((fsloc 0) .--> w) by RELAT_1:25;
x4: dom ((fsloc 0) .--> w) = {(fsloc 0)} by FUNCOP_1:19;
x7: dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
x8: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:19;
x6: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
fsloc 0 <> IC by SCMFSA_2:82;
then x5: dom ((fsloc 0) .--> w) misses dom (Start-At (0,SCM+FSA)) by x4, x7, ZFMISC_1:17;
fsloc 0 <> intloc 0 by SCMFSA_2:83;
then dom ((fsloc 0) .--> w) misses dom ((intloc 0) .--> 1) by x4, x8, ZFMISC_1:17;
then dom ((fsloc 0) .--> w) misses dom (Initialize ((intloc 0) .--> 1)) by x5, x6, XBOOLE_1:70;
then x2: dom (Initialize ((intloc 0) .--> 1)) misses dom (NPP ((fsloc 0) .--> w)) by x3, XBOOLE_1:63;
NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) = (NPP (Initialized Bubble-Sort-Algorithm)) +* (NPP ((fsloc 0) .--> w)) by COMPOS_1:221
.= (Initialize ((intloc 0) .--> 1)) +* (NPP ((fsloc 0) .--> w)) by SCMFSA6A:79 ;
then x1: Initialize ((intloc 0) .--> 1) c= NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) by x2, FUNCT_4:33;
set BSA = Bubble-Sort-Algorithm ;
Initialize ((intloc 0) .--> 1) c= s by A2, x1, XBOOLE_1:1;
hence IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm by Lm26, A1, SCM_HALT:def 1; :: thesis: verum