let w be FinSequence of INT ; :: thesis: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) is autonomic
set p = (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w);
set q = Bubble-Sort-Algorithm ;
X: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) is 0 -started by Th47;
A1: for s1, s2 being State of SCM+FSA
for i being Element of NAT st (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

proof

let s1, s2 be State of SCM+FSA; :: thesis: for i being Element of NAT st (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
let i be Element of NAT ; :: thesis: ( (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 & i <= 10 implies ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) ) )
assume that
A2: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 and
A3: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 and
A4: i <= 10 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
B2: Bubble-Sort-Algorithm c= ProgramPart s1 by A2, Th53, RELAT_1:210;
B3: Bubble-Sort-Algorithm c= ProgramPart s2 by A3, Th53, RELAT_1:210;
A5: Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
A6: s1 is 0 -started by A2, X, COMPOS_1:8;
A7: s2 is 0 -started by A3, X, COMPOS_1:8;
A10: s1 . (intloc 0) = 1 by A2, Th54
.= s2 . (intloc 0) by A3, Th54 ;
A11: s1 . (fsloc 0) = w by A2, Th54
.= s2 . (fsloc 0) by A3, Th54 ;
A12: IC s1 = 0 by A6, COMPOS_1:def 16
.= IC s2 by A7, COMPOS_1:def 16 ;

per cases ( i = 0 or i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 ) by A4, NAT_1:35;

suppose A13: i = 0 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by A5, A10, EXTPRO_1:3; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by A5, A12, A13, EXTPRO_1:3; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by A5, A11, A13, EXTPRO_1:3; :: thesis: verum

end;

suppose A14: i = 1 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A14, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 1 by B2, A6, A14, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A14, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A14, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A14, Lm21 ; :: thesis: verum

end;

suppose A15: i = 2 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A15, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 2 by B2, A6, A15, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A15, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A15, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A15, Lm21 ; :: thesis: verum

end;

suppose A16: i = 3 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A16, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 3 by B2, A6, A16, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A16, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A16, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A16, Lm21 ; :: thesis: verum

end;

suppose A17: i = 4 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A17, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 4 by B2, A6, A17, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A17, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A17, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A17, Lm21 ; :: thesis: verum

end;

suppose A18: i = 5 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A18, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 5 by B2, A6, A18, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A18, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A18, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A18, Lm21 ; :: thesis: verum

end;

suppose A19: i = 6 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A19, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 6 by B2, A6, A19, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A19, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A19, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A19, Lm21 ; :: thesis: verum

end;

suppose A20: i = 7 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A20, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 7 by B2, A6, A20, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A20, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A20, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A20, Lm21 ; :: thesis: verum

end;

suppose A21: i = 8 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A21, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 8 by B2, A6, A21, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A21, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A21, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A21, Lm21 ; :: thesis: verum

end;

suppose A22: i = 9 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A22, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 9 by B2, A6, A22, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A22, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A22, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A22, Lm21 ; :: thesis: verum

end;

suppose A23: i = 10 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = (Comput ((ProgramPart s2),s2,i)) . (intloc 0) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )

hence (Comput ((ProgramPart s1),s1,i)) . (intloc 0) = s1 . (intloc 0) by B2, A6, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (intloc 0) by B3, A7, A10, A23, Lm21 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) & (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) )
thus (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = 10 by B2, A6, A23, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) by B3, A7, A23, Lm21 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = (Comput ((ProgramPart s2),s2,i)) . (fsloc 0)
thus (Comput ((ProgramPart s1),s1,i)) . (fsloc 0) = s1 . (fsloc 0) by B2, A6, A23, Lm21
.= (Comput ((ProgramPart s2),s2,i)) . (fsloc 0) by B3, A7, A11, A23, Lm21 ; :: thesis: verum

end;

end;

end;

set UD = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)};
set Us = (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm);
A24: UsedInt*Loc Bubble-Sort-Algorithm = {(fsloc 0)} by Th59;
A25: UsedIntLoc Bubble-Sort-Algorithm = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by Th58;
then A26: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A24, ENUMSET1:62;
A27: for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 holds
( (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) )

proof

let i be Element of NAT ; :: thesis: for s1, s2 being State of SCM+FSA st 11 <= i & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 holds
( (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) )
let s1, s2 be State of SCM+FSA; :: thesis: ( 11 <= i & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 implies ( (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) ) )
assume that
A28: 11 <= i and
A29: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 and
A30: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 ; :: thesis: ( (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) )
set Cs11 = Comput ((ProgramPart s1),s1,11);
set Cs21 = Comput ((ProgramPart s2),s2,11);
A31: s1 is 0 -started by A29, X, COMPOS_1:8;
A32: s2 is 0 -started by A30, X, COMPOS_1:8;
B33: Bubble-Sort-Algorithm c= s1 by A29, Th53;
A33: Bubble-Sort-Algorithm c= ProgramPart s1 by A29, Th53, RELAT_1:210;
B34: Bubble-Sort-Algorithm c= s2 by A30, Th53;
A34: Bubble-Sort-Algorithm c= ProgramPart s2 by A30, Th53, RELAT_1:210;
A35: s1 . (intloc 0) = 1 by A29, Th54
.= s2 . (intloc 0) by A30, Th54 ;
A36: s1 . (fsloc 0) = w by A29, Th54
.= s2 . (fsloc 0) by A30, Th54 ;
A37: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput ((ProgramPart s1),s1,11)) by Th56;
A38: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput ((ProgramPart s2),s2,11)) by Th56;

now

let x be set ; :: thesis: ( x in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) implies (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁ )
assume x in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁
then A39: x in {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A24, A25, ENUMSET1:62;

per cases ( x = fsloc 0 or x = intloc 0 or x = intloc 1 or x = intloc 2 or x = intloc 3 or x = intloc 4 or x = intloc 5 or x = intloc 6 ) by A39, ENUMSET1:def 6;

suppose A40: x = fsloc 0 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (fsloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A36, A40, Lm21 ;
:: thesis: verum

end;

suppose A41: x = intloc 0 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (intloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A35, A41, Lm21 ;
:: thesis: verum

end;

suppose A42: x = intloc 1 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = len (s1 . (fsloc 0)) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A36, A42, Lm21 ;
:: thesis: verum

end;

suppose A43: x = intloc 2 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (intloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A35, A43, Lm21 ;
:: thesis: verum

end;

suppose A44: x = intloc 3 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (intloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A35, A44, Lm21 ;
:: thesis: verum

end;

suppose A45: x = intloc 4 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (intloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A35, A45, Lm21 ;
:: thesis: verum

end;

suppose A46: x = intloc 5 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (intloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A35, A46, Lm21 ;
:: thesis: verum

end;

suppose A47: x = intloc 6 ; :: thesis: (Comput ((ProgramPart s1),s1,11)) . b₁ = (Comput ((ProgramPart s2),s2,11)) . b₁

hence (Comput ((ProgramPart s1),s1,11)) . x = s1 . (intloc 0) by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . x by A32, A34, A35, A47, Lm21 ;
:: thesis: verum

end;

end;

end;

then A48: (Comput ((ProgramPart s1),s1,11)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,11)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) by A37, A38, FUNCT_1:165;
A49: (Comput ((ProgramPart s1),s1,11)) . (IC SCM+FSA) = 11 by A31, A33, Lm21
.= (Comput ((ProgramPart s2),s2,11)) . (IC SCM+FSA) by A32, A34, Lm21 ;
A50: for i being Element of NAT holds IC (Comput ((ProgramPart s1),s1,i)) in dom Bubble-Sort-Algorithm by A29, Th66;
for i being Element of NAT holds IC (Comput ((ProgramPart s2),s2,i)) in dom Bubble-Sort-Algorithm by A30, Th66;
hence ( (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput ((ProgramPart s1),s1,i)) . (IC SCM+FSA) = (Comput ((ProgramPart s2),s2,i)) . (IC SCM+FSA) ) by A28, A48, A49, A50, Th26, B33, B34; :: thesis: verum

end;

set DD = {(intloc 0),(IC SCM+FSA),(fsloc 0)};
A51: dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) = (dom Bubble-Sort-Algorithm) \/ {(intloc 0),(IC SCM+FSA),(fsloc 0)} by Th42;

now

let s1, s2 be State of SCM+FSA; :: thesis: for i being Element of NAT st (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 holds
(Comput ((ProgramPart s1),s1,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = (Comput ((ProgramPart s2),s2,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))
let i be Element of NAT ; :: thesis: ( (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 implies (Comput ((ProgramPart s1),s1,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = (Comput ((ProgramPart s2),s2,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) )
assume that
A52: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 and
A53: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = (Comput ((ProgramPart s2),s2,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))
set Cs1i = Comput ((ProgramPart s1),s1,i);
set Cs2i = Comput ((ProgramPart s2),s2,i);
A54: Bubble-Sort-Algorithm c= s1 by A52, Th53;
Bubble-Sort-Algorithm c= s2 by A53, Th53;
then A55: (Comput ((ProgramPart s1),s1,i)) | (dom Bubble-Sort-Algorithm) = (Comput ((ProgramPart s2),s2,i)) | (dom Bubble-Sort-Algorithm) by A54, AMI_1:124;
A56: {(intloc 0),(IC SCM+FSA),(fsloc 0)} c= dom (Comput ((ProgramPart s1),s1,i)) by Th55;
A57: {(intloc 0),(IC SCM+FSA),(fsloc 0)} c= dom (Comput ((ProgramPart s2),s2,i)) by Th55;
A58: intloc 0 in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) by A26, ENUMSET1:def 6;
A59: fsloc 0 in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) by A26, ENUMSET1:def 6;
A60: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput ((ProgramPart s1),s1,i)) by Th56;
A61: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput ((ProgramPart s2),s2,i)) by Th56;
A62: ( i > 10 implies 10 + 1 < i + 1 ) by XREAL_1:8;

now

let x be set ; :: thesis: ( x in {(intloc 0),(IC SCM+FSA),(fsloc 0)} implies (Comput ((ProgramPart s1),s1,i)) . b₁ = (Comput ((ProgramPart s2),s2,i)) . b₁ )
assume A63: x in {(intloc 0),(IC SCM+FSA),(fsloc 0)} ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . b₁ = (Comput ((ProgramPart s2),s2,i)) . b₁

per cases ( x = intloc 0 or x = IC SCM+FSA or x = fsloc 0 ) by A63, ENUMSET1:def 1;

suppose A64: x = intloc 0 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . b₁ = (Comput ((ProgramPart s2),s2,i)) . b₁

now

per cases ( i <= 10 or i > 10 ) ;

suppose i <= 10 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x

hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x by A1, A52, A53, A64; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x

then 11 <= i by A62, NAT_1:13;
then (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) by A27, A52, A53;
hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x by A58, A60, A61, A64, FUNCT_1:165; :: thesis: verum

end;

end;

end;

hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x ; :: thesis: verum

end;

suppose A65: x = IC SCM+FSA ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . b₁ = (Comput ((ProgramPart s2),s2,i)) . b₁

now

per cases ( i <= 10 or i > 10 ) ;

suppose i <= 10 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x

hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x by A1, A52, A53, A65; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x

then 11 <= i by A62, NAT_1:13;
hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x by A27, A52, A53, A65; :: thesis: verum

end;

end;

end;

hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x ; :: thesis: verum

end;

suppose A66: x = fsloc 0 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . b₁ = (Comput ((ProgramPart s2),s2,i)) . b₁

now

per cases ( i <= 10 or i > 10 ) ;

suppose i <= 10 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x

hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x by A1, A52, A53, A66; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x

then 11 <= i by A62, NAT_1:13;
then (Comput ((ProgramPart s1),s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput ((ProgramPart s2),s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) by A27, A52, A53;
hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x by A59, A60, A61, A66, FUNCT_1:165; :: thesis: verum

end;

end;

end;

hence (Comput ((ProgramPart s1),s1,i)) . x = (Comput ((ProgramPart s2),s2,i)) . x ; :: thesis: verum

end;

end;

end;

then (Comput ((ProgramPart s1),s1,i)) | {(intloc 0),(IC SCM+FSA),(fsloc 0)} = (Comput ((ProgramPart s2),s2,i)) | {(intloc 0),(IC SCM+FSA),(fsloc 0)} by A56, A57, FUNCT_1:165;
hence (Comput ((ProgramPart s1),s1,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = (Comput ((ProgramPart s2),s2,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) by A51, A55, RELAT_1:185; :: thesis: verum

end;

then for s1, s2 being State of SCM+FSA st (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) c= s2 holds
for i being Element of NAT holds (Comput ((ProgramPart s1),s1,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = (Comput ((ProgramPart s2),s2,i)) | (dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) ;
hence (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) is autonomic by EXTPRO_1:def 9; :: thesis: verum