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 (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 (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 (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 (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: ( (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: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s ; :: thesis: IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm
dom (Initialized Bubble-Sort-Algorithm) misses dom ((fsloc 0) .--> w) by Th46;
then Initialized Bubble-Sort-Algorithm c= (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) by FUNCT_4:33;
then Initialized Bubble-Sort-Algorithm c= s by A2, XBOOLE_1:1;
hence IC (Comput (P,s,i)) in dom Bubble-Sort-Algorithm by Lm26, SCM_HALT:def 1, A1; :: thesis: verum