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

proof

let P, Q be Instruction-Sequence of SCM+FSA; :: thesis: ( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q implies for s1, s2 being State of SCM+FSA
for i being Element of NAT st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) ) )
assume A2: ( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q ) ; :: thesis: for s1, s2 being State of SCM+FSA
for i being Element of NAT st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
let s1, s2 be State of SCM+FSA; :: thesis: for i being Element of NAT st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 holds
( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
let i be Element of NAT ; :: thesis: ( Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & i <= 10 implies ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) ) )
assume that
A3: Initialized ((fsloc 0) .--> w) c= s1 and
A4: Initialized ((fsloc 0) .--> w) c= s2 and
A5: i <= 10 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
A6: Bubble-Sort-Algorithm c= P by A2;
A7: Bubble-Sort-Algorithm c= Q by A2;
A8: Comput (P,s1,0) = s1 ;
A9: s1 is 0 -started by A3, MEMSTR_0:17;
A10: s2 is 0 -started by A4, MEMSTR_0:17;
A11: s1 . (intloc 0) = 1 by A3, SCMFSA_M:33
.= s2 . (intloc 0) by A4, SCMFSA_M:33 ;
A12: s1 . (fsloc 0) = w by A3, SCMFSA_M:33
.= s2 . (fsloc 0) by A4, SCMFSA_M:33 ;
A13: IC s1 = 0 by A9, MEMSTR_0:def 11
.= IC s2 by A10, MEMSTR_0:def 11 ;

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 A5, NAT_1:34;

suppose A14: i = 0 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) by A8, A11, EXTPRO_1:2; :: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) by A8, A13, A14, EXTPRO_1:2; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) by A8, A12, A14, EXTPRO_1:2; :: thesis: verum

end;

suppose A15: i = 1 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A2, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A15, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 1 by A2, A9, A15, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A7, A10, A15, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A6, A9, A15, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A15, Lm21 ; :: thesis: verum

end;

suppose A16: i = 2 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A6, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A16, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 2 by A2, A9, A16, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A16, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A16, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A16, Lm21 ; :: thesis: verum

end;

suppose A17: i = 3 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A2, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A17, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 3 by A2, A9, A17, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A17, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A6, A9, A17, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A17, Lm21 ; :: thesis: verum

end;

suppose A18: i = 4 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A6, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A18, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 4 by A2, A9, A18, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A18, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A18, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A18, Lm21 ; :: thesis: verum

end;

suppose A19: i = 5 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A6, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A19, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 5 by A2, A9, A19, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A19, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A19, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A19, Lm21 ; :: thesis: verum

end;

suppose A20: i = 6 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A2, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A20, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 6 by A2, A9, A20, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A20, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A20, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A20, Lm21 ; :: thesis: verum

end;

suppose A21: i = 7 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A6, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A21, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 7 by A2, A9, A21, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A21, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A21, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A21, Lm21 ; :: thesis: verum

end;

suppose A22: i = 8 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A2, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A22, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 8 by A2, A9, A22, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A22, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A22, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A22, Lm21 ; :: thesis: verum

end;

suppose A23: i = 9 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A2, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A23, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 9 by A2, A9, A23, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A23, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A23, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A23, Lm21 ; :: thesis: verum

end;

suppose A24: i = 10 ; :: thesis: ( (Comput (P,s1,i)) . (intloc 0) = (Comput (Q,s2,i)) . (intloc 0) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )

hence (Comput (P,s1,i)) . (intloc 0) = s1 . (intloc 0) by A2, A9, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A2, A10, A11, A24, Lm21 ;
:: thesis: ( (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) & (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0) )
thus (Comput (P,s1,i)) . (IC ) = 10 by A2, A9, A24, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A2, A10, A24, Lm21 ; :: thesis: (Comput (P,s1,i)) . (fsloc 0) = (Comput (Q,s2,i)) . (fsloc 0)
thus (Comput (P,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A2, A9, A24, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A2, A10, A12, A24, 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);
A25: UsedInt*Loc Bubble-Sort-Algorithm = {(fsloc 0)} by Th35;
A26: UsedIntLoc Bubble-Sort-Algorithm = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by Th34;
then A27: (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 A25, ENUMSET1:22;
A28: for P, Q being Instruction-Sequence of SCM+FSA st Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q holds
for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )

proof

let P, Q be Instruction-Sequence of SCM+FSA; :: thesis: ( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q implies for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) ) )
assume A29: ( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q ) ; :: thesis: for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
let i be Element of NAT ; :: thesis: for s1, s2 being State of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
let s1, s2 be State of SCM+FSA; :: thesis: ( 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 implies ( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) ) )
assume that
A30: 11 <= i and
A31: Initialized ((fsloc 0) .--> w) c= s1 and
A32: Initialized ((fsloc 0) .--> w) c= s2 ; :: thesis: ( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) )
set Cs11 = Comput (P,s1,11);
set Cs21 = Comput (Q,s2,11);
A33: s1 is 0 -started by A31, MEMSTR_0:17;
A34: s2 is 0 -started by A32, MEMSTR_0:17;
A35: s1 . (intloc 0) = 1 by A31, SCMFSA_M:33
.= s2 . (intloc 0) by A32, SCMFSA_M:33 ;
A36: s1 . (fsloc 0) = w by A31, SCMFSA_M:33
.= s2 . (fsloc 0) by A32, SCMFSA_M:33 ;
A37: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (P,s1,11)) by Th32;
A38: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (Q,s2,11)) by Th32;

now :: thesis: for x being set st x in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) holds
(Comput (P,s1,11)) . x = (Comput (Q,s2,11)) . x

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

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 (P,s1,11)) . b₁ = (Comput (Q,s2,11)) . b₁

hence (Comput (P,s1,11)) . x = s1 . (fsloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A36, A40, Lm21 ;
:: thesis: verum

end;

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

hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A35, A41, Lm21 ;
:: thesis: verum

end;

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

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

end;

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

hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A35, A43, Lm21 ;
:: thesis: verum

end;

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

hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A35, A44, Lm21 ;
:: thesis: verum

end;

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

hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A35, A45, Lm21 ;
:: thesis: verum

end;

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

hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A35, A46, Lm21 ;
:: thesis: verum

end;

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

hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A33, A29, Lm21
.= (Comput (Q,s2,11)) . x by A34, A29, A35, A47, Lm21 ;
:: thesis: verum

end;

end;

end;

then A48: (Comput (P,s1,11)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,11)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) by A37, A38, FUNCT_1:95;
A49: (Comput (P,s1,11)) . (IC ) = 11 by A33, A29, Lm21
.= (Comput (Q,s2,11)) . (IC ) by A34, A29, Lm21 ;
A50: for i being Element of NAT holds IC (Comput (P,s1,i)) in dom Bubble-Sort-Algorithm by A31, Th42, A29;
for i being Element of NAT holds IC (Comput (Q,s2,i)) in dom Bubble-Sort-Algorithm by A32, Th42, A29;
hence ( (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) & (Comput (P,s1,i)) . (IC ) = (Comput (Q,s2,i)) . (IC ) ) by A30, A48, A49, A50, Th15, A29; :: thesis: verum

end;

set DD = {(intloc 0),(IC ),(fsloc 0)};
let P, Q be Instruction-Sequence of SCM+FSA; :: according to EXTPRO_1:def 10 :: thesis: ( not Bubble-Sort-Algorithm c= P or not Bubble-Sort-Algorithm c= Q or for b₁, b₂ being set holds
( not Initialized ((fsloc 0) .--> w) c= b₁ or not Initialized ((fsloc 0) .--> w) c= b₂ or for b₃ being Element of NAT holds (Comput (P,b₁,b₃)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,b₂,b₃)) | (dom (Initialized ((fsloc 0) .--> w))) ) )
assume A51: ( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q ) ; :: thesis: for b₁, b₂ being set holds
( not Initialized ((fsloc 0) .--> w) c= b₁ or not Initialized ((fsloc 0) .--> w) c= b₂ or for b₃ being Element of NAT holds (Comput (P,b₁,b₃)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,b₂,b₃)) | (dom (Initialized ((fsloc 0) .--> w))) )
let s1, s2 be State of SCM+FSA; :: thesis: ( not Initialized ((fsloc 0) .--> w) c= s1 or not Initialized ((fsloc 0) .--> w) c= s2 or for b₁ being Element of NAT holds (Comput (P,s1,b₁)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,b₁)) | (dom (Initialized ((fsloc 0) .--> w))) )
assume that
A52: Initialized ((fsloc 0) .--> w) c= s1 and
A53: Initialized ((fsloc 0) .--> w) c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (P,s1,b₁)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,b₁)) | (dom (Initialized ((fsloc 0) .--> w)))
let i be Element of NAT ; :: thesis: (Comput (P,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))
set Cs1i = Comput (P,s1,i);
set Cs2i = Comput (Q,s2,i);
A54: dom (Initialized ((fsloc 0) .--> w)) = {(intloc 0),(IC ),(fsloc 0)} by SCMFSA_M:31;
A55: {(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P,s1,i)) by SCMFSA_M:34;
A56: {(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (Q,s2,i)) by SCMFSA_M:34;
A57: intloc 0 in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) by A27, ENUMSET1:def 6;
A58: fsloc 0 in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) by A27, ENUMSET1:def 6;
A59: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (P,s1,i)) by Th32;
A60: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (Q,s2,i)) by Th32;
A61: ( i > 10 implies 10 + 1 < i + 1 ) by XREAL_1:6;

now :: thesis: for x being set st x in {(intloc 0),(IC ),(fsloc 0)} holds
(Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x

let x be set ; :: thesis: ( x in {(intloc 0),(IC ),(fsloc 0)} implies (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁ )
assume A62: x in {(intloc 0),(IC ),(fsloc 0)} ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

per cases ( x = intloc 0 or x = IC or x = fsloc 0 ) by A62, ENUMSET1:def 1;

suppose A63: x = intloc 0 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

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

suppose i <= 10 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A1, A52, A53, A63, A51; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

then 11 <= i by A61, NAT_1:13;
then (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) by A28, A52, A53, A51;
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A57, A59, A60, A63, FUNCT_1:95; :: thesis: verum

end;

end;

end;

suppose A64: x = IC ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

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

suppose i <= 10 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

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

end;

suppose i > 10 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

then 11 <= i by A61, NAT_1:13;
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A28, A52, A53, A64, A51; :: thesis: verum

end;

end;

end;

suppose A65: x = fsloc 0 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

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

suppose i <= 10 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

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

end;

suppose i > 10 ; :: thesis: (Comput (P,s1,i)) . b₁ = (Comput (Q,s2,i)) . b₁

then 11 <= i by A61, NAT_1:13;
then (Comput (P,s1,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) = (Comput (Q,s2,i)) | ((UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm)) by A28, A52, A53, A51;
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A58, A59, A60, A65, FUNCT_1:95; :: thesis: verum

end;

end;

end;

end;

end;

hence (Comput (P,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,i)) | (dom (Initialized ((fsloc 0) .--> w))) by A54, A55, A56, FUNCT_1:95; :: thesis: verum