let w be FinSequence of INT ; :: thesis: (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) is autonomic
set p = (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w);
set q = Insert-Sort-Algorithm ;
A1: for s1, s2 being State of SCM+FSA
for i being Element of NAT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-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 SCM+FSA ; :: thesis: for i being Element of NAT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-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 Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-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 A2: ( (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 & 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 ) )
A3: ( Computation s1,0 = s1 & Computation s2,0 = s2 ) by AMI_1:13;
A4: s1 starts_at 0 by A2, AMI_1:92, SCMBSORT:47;
A5: s2 starts_at 0 by A2, AMI_1:92, SCMBSORT:47;
A6: ( Insert-Sort-Algorithm c= s1 & Insert-Sort-Algorithm c= s2 ) by A2, SCMBSORT:53;
A7: s1 . (intloc 0 ) = 1 by A2, SCMBSORT:54
.= s2 . (intloc 0 ) by A2, SCMBSORT:54 ;
A8: s1 . (fsloc 0 ) = w by A2, SCMBSORT:54
.= s2 . (fsloc 0 ) by A2, SCMBSORT:54 ;
A9: IC s1 = insloc 0 by A4, AMI_1:def 41
.= IC s2 by A5, 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 A2, NAT_1:35;
suppose A10: 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 A3, A7; :: 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 A3, A9, A10; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 ) by A3, A8, A10; :: thesis: verum
end;
suppose A11: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A11, Lm2 ;
:: 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 A4, A6, A11, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A11, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A11, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A11, Lm2 ; :: thesis: verum
end;
suppose A12: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A12, Lm2 ;
:: 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 A4, A6, A12, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A12, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A12, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A12, Lm2 ; :: thesis: verum
end;
suppose A13: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A13, Lm2 ;
:: 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 A4, A6, A13, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A13, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A13, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A13, Lm2 ; :: thesis: verum
end;
suppose A14: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A14, Lm2 ;
:: 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 A4, A6, A14, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A14, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A14, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A14, Lm2 ; :: thesis: verum
end;
suppose A15: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A15, Lm2 ;
:: 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 A4, A6, A15, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A15, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A15, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A15, Lm2 ; :: thesis: verum
end;
suppose A16: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A16, Lm2 ;
:: 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 A4, A6, A16, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A16, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A16, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A16, Lm2 ; :: thesis: verum
end;
suppose A17: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A17, Lm2 ;
:: 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 A4, A6, A17, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A17, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A17, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A17, Lm2 ; :: thesis: verum
end;
suppose A18: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A18, Lm2 ;
:: 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 A4, A6, A18, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A18, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A18, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A18, Lm2 ; :: thesis: verum
end;
suppose A19: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A19, Lm2 ;
:: 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 A4, A6, A19, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A19, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A19, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A19, Lm2 ; :: thesis: verum
end;
suppose A20: 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 A4, A6, Lm2
.= (Computation s2,i) . (intloc 0 ) by A5, A6, A7, A20, Lm2 ;
:: 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 A4, A6, A20, Lm2
.= (Computation s2,i) . (IC SCM+FSA ) by A5, A6, A20, Lm2 ; :: thesis: (Computation s1,i) . (fsloc 0 ) = (Computation s2,i) . (fsloc 0 )
thus (Computation s1,i) . (fsloc 0 ) = s1 . (fsloc 0 ) by A4, A6, A20, Lm2
.= (Computation s2,i) . (fsloc 0 ) by A5, A6, A8, A20, Lm2 ; :: 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 Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm );
A21: UsedInt*Loc Insert-Sort-Algorithm = {(fsloc 0 )} by Th39;
A22: UsedIntLoc Insert-Sort-Algorithm = {(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by Th38;
then A23: (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) = {(fsloc 0 ),(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A21, ENUMSET1:62;
A24: for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 holds
( (Computation s1,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-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 SCM+FSA st 11 <= i & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 holds
( (Computation s1,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) )
let s1, s2 be State of SCM+FSA ; :: thesis: ( 11 <= i & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 implies ( (Computation s1,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) ) )
assume that
A25: 11 <= i and
A26: (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 and
A27: (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 ; :: thesis: ( (Computation s1,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) )
set Cs11 = Computation s1,11;
set Cs21 = Computation s2,11;
A28: s1 starts_at 0 by A26, AMI_1:92, SCMBSORT:47;
A29: s2 starts_at 0 by A27, AMI_1:92, SCMBSORT:47;
A30: Insert-Sort-Algorithm c= s1 by A26, SCMBSORT:53;
A31: Insert-Sort-Algorithm c= s2 by A27, SCMBSORT:53;
A32: s1 . (intloc 0 ) = 1 by A26, SCMBSORT:54
.= s2 . (intloc 0 ) by A27, SCMBSORT:54 ;
A33: s1 . (fsloc 0 ) = w by A26, SCMBSORT:54
.= s2 . (fsloc 0 ) by A27, SCMBSORT:54 ;
A34: (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) c= dom (Computation s1,11) by SCMBSORT:56;
A35: (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) c= dom (Computation s2,11) by SCMBSORT:56;
now
let x be set ; :: thesis: ( x in (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) implies (Computation s1,11) . b1 = (Computation s2,11) . b1 )
assume x in (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
then A36: x in {(fsloc 0 ),(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A21, A22, 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 A36, ENUMSET1:def 6;
suppose A37: x = fsloc 0 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (fsloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A33, A37, Lm2 ;
:: thesis: verum
end;
suppose A38: x = intloc 0 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (intloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A32, A38, Lm2 ;
:: thesis: verum
end;
suppose A39: x = intloc 1 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = len (s1 . (fsloc 0 )) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A33, A39, Lm2 ;
:: thesis: verum
end;
suppose A40: x = intloc 2 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (intloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A32, A40, Lm2 ;
:: thesis: verum
end;
suppose A41: x = intloc 3 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (intloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A32, A41, Lm2 ;
:: thesis: verum
end;
suppose A42: x = intloc 4 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (intloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A32, A42, Lm2 ;
:: thesis: verum
end;
suppose A43: x = intloc 5 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (intloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A32, A43, Lm2 ;
:: thesis: verum
end;
suppose A44: x = intloc 6 ; :: thesis: (Computation s1,11) . b1 = (Computation s2,11) . b1
hence (Computation s1,11) . x = s1 . (intloc 0 ) by A28, A30, Lm2
.= (Computation s2,11) . x by A29, A31, A32, A44, Lm2 ;
:: thesis: verum
end;
end;
end;
then A45: (Computation s1,11) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) = (Computation s2,11) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) by A34, A35, FUNCT_1:165;
A46: (Computation s1,11) . (IC SCM+FSA ) = insloc 11 by A28, A30, Lm2
.= (Computation s2,11) . (IC SCM+FSA ) by A29, A31, Lm2 ;
A47: for i being Element of NAT holds IC (Computation s1,i) in dom Insert-Sort-Algorithm by A26, Th46;
for i being Element of NAT holds IC (Computation s2,i) in dom Insert-Sort-Algorithm by A27, Th46;
hence ( (Computation s1,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) = (Computation s2,i) | ((UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm )) & (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) ) by A25, A30, A31, A45, A46, A47, SCMBSORT:26; :: thesis: verum
end;
set DD = {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )};
A48: dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w)) = (dom Insert-Sort-Algorithm ) \/ {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} by SCMBSORT:42;
now
let s1, s2 be State of SCM+FSA ; :: thesis: for i being Element of NAT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 holds
(Computation s1,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w)))
let i be Element of NAT ; :: thesis: ( (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 implies (Computation s1,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) )
assume A49: ( (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 ) ; :: thesis: (Computation s1,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w)))
set Cs1i = Computation s1,i;
set Cs2i = Computation s2,i;
( Insert-Sort-Algorithm c= s1 & Insert-Sort-Algorithm c= s2 ) by A49, SCMBSORT:53;
then A50: (Computation s1,i) | (dom Insert-Sort-Algorithm ) = (Computation s2,i) | (dom Insert-Sort-Algorithm ) by AMI_1:124;
A51: {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} c= dom (Computation s1,i) by SCMBSORT:55;
A52: {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} c= dom (Computation s2,i) by SCMBSORT:55;
(Computation s1,i) | {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} = (Computation s2,i) | {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )}
proof
A53: intloc 0 in (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) by A23, ENUMSET1:def 6;
A54: fsloc 0 in (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) by A23, ENUMSET1:def 6;
A55: (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) c= dom (Computation s1,i) by SCMBSORT:56;
A56: (UsedInt*Loc Insert-Sort-Algorithm ) \/ (UsedIntLoc Insert-Sort-Algorithm ) c= dom (Computation s2,i) by SCMBSORT:56;
A57: ( 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) . b1 = (Computation s2,i) . b1 )
assume A58: x in {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} ; :: thesis: (Computation s1,i) . b1 = (Computation s2,i) . b1
per cases ( x = intloc 0 or x = IC SCM+FSA or x = fsloc 0 ) by A58, ENUMSET1:def 1;
suppose A59: x = intloc 0 ; :: thesis: (Computation s1,i) . b1 = (Computation s2,i) . b1
hence (Computation s1,i) . x = (Computation s2,i) . x ; :: thesis: verum
end;
suppose A60: x = IC SCM+FSA ; :: thesis: (Computation s1,i) . b1 = (Computation s2,i) . b1
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, A49, A60; :: thesis: verum
end;
suppose i > 10 ; :: thesis: (Computation s1,i) . x = (Computation s2,i) . x
then 11 <= i by A57, NAT_1:13;
hence (Computation s1,i) . x = (Computation s2,i) . x by A24, A49, A60; :: thesis: verum
end;
end;
end;
hence (Computation s1,i) . x = (Computation s2,i) . x ; :: thesis: verum
end;
suppose A61: x = fsloc 0 ; :: thesis: (Computation s1,i) . b1 = (Computation s2,i) . b1
hence (Computation s1,i) . x = (Computation s2,i) . x ; :: thesis: verum
end;
end;
end;
hence (Computation s1,i) | {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} = (Computation s2,i) | {(intloc 0 ),(IC SCM+FSA ),(fsloc 0 )} by A51, A52, FUNCT_1:165; :: thesis: verum
end;
hence (Computation s1,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) by A48, A50, RELAT_1:185; :: thesis: verum
end;
then for s1, s2 being State of SCM+FSA st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s1 & (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s2 holds
for i being Element of NAT holds (Computation s1,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) = (Computation s2,i) | (dom ((Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w))) ;
hence (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) is autonomic by AMI_1:def 25; :: thesis: verum