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 ;
A1: for s1, s2 being State of
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
( (Computation s1,i) . (intloc 0 ) = (Computation s2,i) . (intloc 0 ) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )

proof

let s1, s2 be State of ; :: 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
( (Computation s1,i) . (intloc 0 ) = (Computation s2,i) . (intloc 0 ) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation 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 ( (Computation s1,i) . (intloc 0 ) = (Computation s2,i) . (intloc 0 ) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation 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: ( (Computation s1,i) . (intloc 0 ) = (Computation s2,i) . (intloc 0 ) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
A5: Computation s1,0 = s1 by AMI_1:13;
A6: s1 starts_at 0 by A2, Th47, AMI_1:92;
A7: s2 starts_at 0 by A3, Th47, AMI_1:92;
A8: Bubble-Sort-Algorithm c= s1 by A2, Th53;
A9: Bubble-Sort-Algorithm c= s2 by A3, Th53;
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 = insloc 0 by A6, AMI_1:def 41
.= IC s2 by A7, AMI_1:def 41 ;

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: ( (Computation s1,i) . (intloc 0 ) = (Computation s2,i) . (intloc 0 ) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )

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

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A14, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 1 by A6, A8, A14, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A14, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A14, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A14, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A15, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 2 by A6, A8, A15, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A15, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A15, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A15, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A16, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 3 by A6, A8, A16, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A16, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A16, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A16, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A17, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 4 by A6, A8, A17, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A17, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A17, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A17, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A18, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 5 by A6, A8, A18, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A18, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A18, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A18, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A19, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 6 by A6, A8, A19, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A19, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A19, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A19, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A20, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 7 by A6, A8, A20, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A20, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A20, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A20, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A21, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 8 by A6, A8, A21, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A21, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A21, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A21, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A22, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 9 by A6, A8, A22, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A22, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A22, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, A11, A22, Lm21 ; :: thesis: verum

end;

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

hence (Computation s1,i) . (intloc 0 ) = s1 . (intloc 0 ) by A6, A8, Lm21
.= (Computation s2,i) . (intloc 0 ) by A7, A9, A10, A23, Lm21 ;
:: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) )
thus (Computation s1,i) . (IC SCM+FSA ) = insloc 10 by A6, A8, A23, Lm21
.= (Computation s2,i) . (IC SCM+FSA ) by A7, A9, A23, Lm21 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A6, A8, A23, Lm21
.= (Computation s2,i) . (fsloc 0 ) by A7, A9, 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 st 11 <= i & (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 holds
( (Computation s1,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) )

proof

let i be Element of NAT ; :: thesis: for s1, s2 being State of st 11 <= i & (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 holds
( (Computation s1,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) )
let s1, s2 be State of ; :: thesis: ( 11 <= i & (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 implies ( (Computation s1,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation 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: ( (Computation s1,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) )
set Cs11 = Computation s1,11;
set Cs21 = Computation s2,11;
A31: s1 starts_at 0 by A29, Th47, AMI_1:92;
A32: s2 starts_at 0 by A30, Th47, AMI_1:92;
A33: Bubble-Sort-Algorithm c= s1 by A29, Th53;
A34: Bubble-Sort-Algorithm c= s2 by A30, Th53;
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 (Computation s1,11) by Th56;
A38: (UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm ) c= dom (Computation s2,11) by Th56;

now

let x be set ; :: thesis: ( x in (UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm ) implies (Computation s1,11) . b₁ = (Computation s2,11) . b₁ )
assume x in (UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm ) ; :: thesis: (Computation s1,11) . b₁ = (Computation 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: (Computation s1,11) . b₁ = (Computation s2,11) . b₁

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

then A48: (Computation s1,11) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) = (Computation s2,11) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) by A37, A38, FUNCT_1:165;
A49: (Computation s1,11) . (IC SCM+FSA ) = insloc 11 by A31, A33, Lm21
.= (Computation s2,11) . (IC SCM+FSA ) by A32, A34, Lm21 ;
A50: for i being Element of NAT holds IC (Computation s1,i) in dom Bubble-Sort-Algorithm by A29, Th66;
for i being Element of NAT holds IC (Computation s2,i) in dom Bubble-Sort-Algorithm by A30, Th66;
hence ( (Computation s1,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) ) by A28, A33, A34, A48, A49, A50, Th26; :: 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 ; :: 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
(Computation s1,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation 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 (Computation s1,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation 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: (Computation s1,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w)))
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
A54: Bubble-Sort-Algorithm c= s1 by A52, Th53;
Bubble-Sort-Algorithm c= s2 by A53, Th53;
then A55: (Computation s1,i) | (dom Bubble-Sort-Algorithm ) = (Computation s2,i) | (dom Bubble-Sort-Algorithm ) by A54, AMI_1:124;
A56: {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} c= dom (Computation s1,i) by Th55;
A57: {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} c= dom (Computation 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 (Computation s1,i) by Th56;
A61: (UsedInt*Loc Bubble-Sort-Algorithm ) \/ (UsedIntLoc Bubble-Sort-Algorithm ) c= dom (Computation 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 (Computation s1,i) . b₁ = (Computation s2,i) . b₁ )
assume A63: x in {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} ; :: thesis: (Computation s1,i) . b₁ = (Computation 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: (Computation s1,i) . b₁ = (Computation s2,i) . b₁

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

then (Computation s1,i) | {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} = (Computation s2,i) | {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} by A56, A57, FUNCT_1:165;
hence (Computation s1,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation 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 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 (Computation s1,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) ;
hence (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) is autonomic by AMI_1:def 25; :: thesis: verum