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