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: (Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w) is 0 -started by Th47;
A2: Bubble-Sort-Algorithm c= ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) by Th53;
A3: for P, Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q holds
for s1, s2 being State of SCM+FSA
for i being Element of NAT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q implies for s1, s2 being State of SCM+FSA
for i being Element of NAT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 A4: ( ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q ) ; :: thesis: for s1, s2 being State of SCM+FSA
for i being Element of NAT st NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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: ( NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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
A5: NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 and
A6: NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 and
A7: 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) )
A8: Bubble-Sort-Algorithm c= P by Th53, A4;
A9: Bubble-Sort-Algorithm c= Q by Th53, A4;
A10: Comput (P,s1,0) = s1 by EXTPRO_1:3;
A11: s1 is 0 -started by A5, A1, COMPOS_1:8;
A12: s2 is 0 -started by A6, A1, COMPOS_1:8;
A13: s1 . (intloc 0) = 1 by A5, Th54
.= s2 . (intloc 0) by A6, Th54 ;
A14: s1 . (fsloc 0) = w by A5, Th54
.= s2 . (fsloc 0) by A6, Th54 ;
A15: IC s1 = 0 by A11, COMPOS_1:def 16
.= IC s2 by A12, COMPOS_1:def 16 ;
per cases ( i = 0 or i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 ) by A7, NAT_1:35;
suppose A16: 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 A10, A13, EXTPRO_1:3; :: 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 A10, A15, A16, EXTPRO_1:3; :: 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 A10, A14, A16, EXTPRO_1:3; :: thesis: verum
end;
suppose A17: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 1 by A8, A11, A17, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A17, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A17, Lm21 ; :: thesis: verum
end;
suppose A18: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 2 by A8, A11, A18, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A18, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A18, Lm21 ; :: thesis: verum
end;
suppose A19: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 3 by A8, A11, A19, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A19, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A19, Lm21 ; :: thesis: verum
end;
suppose A20: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 4 by A8, A11, A20, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A20, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A20, Lm21 ; :: thesis: verum
end;
suppose A21: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 5 by A8, A11, A21, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A21, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A21, Lm21 ; :: thesis: verum
end;
suppose A22: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 6 by A8, A11, A22, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A22, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A22, Lm21 ; :: thesis: verum
end;
suppose A23: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 7 by A8, A11, A23, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A23, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A23, Lm21 ; :: thesis: verum
end;
suppose A24: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, 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 ) = 8 by A8, A11, A24, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, 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 A8, A11, A24, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A24, Lm21 ; :: thesis: verum
end;
suppose A25: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, A25, 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 A8, A11, A25, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, A25, 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 A8, A11, A25, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A25, Lm21 ; :: thesis: verum
end;
suppose A26: 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 A8, A11, Lm21
.= (Comput (Q,s2,i)) . (intloc 0) by A9, A12, A13, A26, 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 A8, A11, A26, Lm21
.= (Comput (Q,s2,i)) . (IC ) by A9, A12, A26, 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 A8, A11, A26, Lm21
.= (Comput (Q,s2,i)) . (fsloc 0) by A9, A12, A14, A26, 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);
A27: UsedInt*Loc Bubble-Sort-Algorithm = {(fsloc 0)} by Th59;
A28: UsedIntLoc Bubble-Sort-Algorithm = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by Th58;
then A29: (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 A27, ENUMSET1:62;
A30: for P, Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q holds
for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q implies for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 A31: ( ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q ) ; :: thesis: for i being Element of NAT
for s1, s2 being State of SCM+FSA st 11 <= i & NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 ) )
A32: ( Bubble-Sort-Algorithm c= P & Bubble-Sort-Algorithm c= Q ) by A31, A2, XBOOLE_1:1;
let i be Element of NAT ; :: thesis: for s1, s2 being State of SCM+FSA st 11 <= i & NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 & NPP ((Initialized Bubble-Sort-Algorithm) +* ((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
A33: 11 <= i and
A34: NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 and
A35: NPP ((Initialized Bubble-Sort-Algorithm) +* ((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);
A36: s1 is 0 -started by A34, A1, COMPOS_1:8;
A37: s2 is 0 -started by A35, A1, COMPOS_1:8;
A38: Bubble-Sort-Algorithm c= P by Th53, A31;
A39: Bubble-Sort-Algorithm c= Q by Th53, A31;
A40: s1 . (intloc 0) = 1 by A34, Th54
.= s2 . (intloc 0) by A35, Th54 ;
A41: s1 . (fsloc 0) = w by A34, Th54
.= s2 . (fsloc 0) by A35, Th54 ;
A42: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (P,s1,11)) by Th56;
A43: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (Q,s2,11)) by Th56;
now
let x be set ; :: thesis: ( x in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) implies (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1 )
assume x in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
then A44: x in {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A27, A28, 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 A44, ENUMSET1:def 6;
suppose A45: x = fsloc 0 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (fsloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A41, A45, Lm21 ;
:: thesis: verum
end;
suppose A46: x = intloc 0 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A40, A46, Lm21 ;
:: thesis: verum
end;
suppose A47: x = intloc 1 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = len (s1 . (fsloc 0)) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A41, A47, Lm21 ;
:: thesis: verum
end;
suppose A48: x = intloc 2 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A40, A48, Lm21 ;
:: thesis: verum
end;
suppose A49: x = intloc 3 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A40, A49, Lm21 ;
:: thesis: verum
end;
suppose A50: x = intloc 4 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A40, A50, Lm21 ;
:: thesis: verum
end;
suppose A51: x = intloc 5 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A40, A51, Lm21 ;
:: thesis: verum
end;
suppose A52: x = intloc 6 ; :: thesis: (Comput (P,s1,11)) . b1 = (Comput (Q,s2,11)) . b1
hence (Comput (P,s1,11)) . x = s1 . (intloc 0) by A36, A38, Lm21
.= (Comput (Q,s2,11)) . x by A37, A39, A40, A52, Lm21 ;
:: thesis: verum
end;
end;
end;
then A53: (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 A42, A43, FUNCT_1:165;
A54: (Comput (P,s1,11)) . (IC ) = 11 by A36, A38, Lm21
.= (Comput (Q,s2,11)) . (IC ) by A37, A39, Lm21 ;
A55: for i being Element of NAT holds IC (Comput (P,s1,i)) in dom Bubble-Sort-Algorithm by A34, Th66, A32;
for i being Element of NAT holds IC (Comput (Q,s2,i)) in dom Bubble-Sort-Algorithm by A35, Th66, A32;
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 A33, A53, A54, A55, Th26, A32; :: thesis: verum
end;
set DD = {(intloc 0),(IC ),(fsloc 0)};
A56: dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) = (dom Bubble-Sort-Algorithm) \/ {(intloc 0),(IC ),(fsloc 0)} by Th42;
let P, Q be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: according to EXTPRO_1:def 9 :: thesis: ( not ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P or not ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q or for b1, b2 being set holds
( not NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= b1 or not NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,b2,b3)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) ) )
assume A57: ( ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= P & ProgramPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= Q ) ; :: thesis: for b1, b2 being set holds
( not NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= b1 or not NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,b2,b3)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) )
let s1, s2 be State of SCM+FSA; :: thesis: ( not NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 or not NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 or for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,s2,b1)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) )
assume that
A58: NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s1 and
A59: NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) c= s2 ; :: thesis: for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,s2,b1)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))))
let i be Element of NAT ; :: thesis: (Comput (P,s1,i)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,s2,i)) | (proj1 (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))))
set Cs1i = Comput (P,s1,i);
set Cs2i = Comput (Q,s2,i);
fsloc 0 in FinSeq-Locations by SCMFSA_2:10;
then A60: fsloc 0 in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
intloc 0 in Int-Locations by SCMFSA_2:9;
then A61: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:127, XBOOLE_0:def 3;
A62: dom (DataPart ((fsloc 0) .--> w)) = (dom ((fsloc 0) .--> w)) /\ (Data-Locations SCM+FSA) by RELAT_1:90
.= {(fsloc 0)} /\ (Data-Locations SCM+FSA) by FUNCOP_1:19
.= {(fsloc 0)} by A60, ZFMISC_1:52 ;
A63: Data-Locations SCM+FSA misses NAT by COMPOS_1:51;
dom Bubble-Sort-Algorithm c= NAT by RELAT_1:def 18;
then A64: Data-Locations SCM+FSA misses dom Bubble-Sort-Algorithm by A63, XBOOLE_1:63;
A65: Initialized Bubble-Sort-Algorithm = Bubble-Sort-Algorithm +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 4
.= Initialize (Bubble-Sort-Algorithm +* ((intloc 0) .--> 1)) by FUNCT_4:15 ;
DataPart (Initialized Bubble-Sort-Algorithm) = ((Bubble-Sort-Algorithm +* ((intloc 0) .--> 1)) | (Data-Locations SCM+FSA)) +* (DataPart (Start-At (0,SCM+FSA))) by A65, FUNCT_4:75
.= ((Bubble-Sort-Algorithm +* ((intloc 0) .--> 1)) | (Data-Locations SCM+FSA)) +* {} by COMPOS_1:30
.= (Bubble-Sort-Algorithm +* ((intloc 0) .--> 1)) | (Data-Locations SCM+FSA) by FUNCT_4:22
.= (DataPart Bubble-Sort-Algorithm) +* (((intloc 0) .--> 1) | (Data-Locations SCM+FSA)) by FUNCT_4:75
.= {} +* (((intloc 0) .--> 1) | (Data-Locations SCM+FSA)) by A64, RELAT_1:95
.= ((intloc 0) .--> 1) | (Data-Locations SCM+FSA) by FUNCT_4:21 ;
then A66: dom (DataPart (Initialized Bubble-Sort-Algorithm)) = (dom ((intloc 0) .--> 1)) /\ (Data-Locations SCM+FSA) by RELAT_1:90
.= {(intloc 0)} /\ (Data-Locations SCM+FSA) by FUNCOP_1:19
.= {(intloc 0)} by A61, ZFMISC_1:52 ;
DataPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) = (DataPart (Initialized Bubble-Sort-Algorithm)) +* (DataPart ((fsloc 0) .--> w)) by FUNCT_4:75;
then A67: dom (DataPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = {(fsloc 0)} \/ {(intloc 0)} by A62, A66, FUNCT_4:def 1
.= {(intloc 0),(fsloc 0)} by ENUMSET1:41 ;
IC in {(intloc 0),(IC ),(fsloc 0)} by ENUMSET1:def 1;
then IC in dom ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)) by A56, XBOOLE_0:def 3;
then A68: dom (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w))) = {(IC )} \/ (dom (DataPart ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) by COMPOS_1:70
.= {(IC ),(intloc 0),(fsloc 0)} by A67, ENUMSET1:42
.= {(intloc 0),(IC ),(fsloc 0)} by ENUMSET1:99 ;
A69: {(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P,s1,i)) by Th55;
A70: {(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (Q,s2,i)) by Th55;
A71: intloc 0 in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) by A29, ENUMSET1:def 6;
A72: fsloc 0 in (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) by A29, ENUMSET1:def 6;
A73: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (P,s1,i)) by Th56;
A74: (UsedInt*Loc Bubble-Sort-Algorithm) \/ (UsedIntLoc Bubble-Sort-Algorithm) c= dom (Comput (Q,s2,i)) by Th56;
A75: ( i > 10 implies 10 + 1 < i + 1 ) by XREAL_1:8;
now
let x be set ; :: thesis: ( x in {(intloc 0),(IC ),(fsloc 0)} implies (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1 )
assume A76: x in {(intloc 0),(IC ),(fsloc 0)} ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
per cases ( x = intloc 0 or x = IC or x = fsloc 0 ) by A76, ENUMSET1:def 1;
suppose A77: x = intloc 0 ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
now
per cases ( i <= 10 or i > 10 ) ;
suppose i <= 10 ; :: thesis: (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A3, A58, A59, A77, A57; :: thesis: verum
end;
end;
end;
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x ; :: thesis: verum
end;
suppose A78: x = IC ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
per cases ( i <= 10 or i > 10 ) ;
suppose i <= 10 ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A3, A58, A59, A78, A57; :: thesis: verum
end;
suppose i > 10 ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
then 11 <= i by A75, NAT_1:13;
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A30, A58, A59, A78, A57; :: thesis: verum
end;
end;
end;
suppose A79: x = fsloc 0 ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
per cases ( i <= 10 or i > 10 ) ;
suppose i <= 10 ; :: thesis: (Comput (P,s1,i)) . b1 = (Comput (Q,s2,i)) . b1
hence (Comput (P,s1,i)) . x = (Comput (Q,s2,i)) . x by A3, A58, A59, A79, A57; :: thesis: verum
end;
end;
end;
end;
end;
then (Comput (P,s1,i)) | {(intloc 0),(IC ),(fsloc 0)} = (Comput (Q,s2,i)) | {(intloc 0),(IC ),(fsloc 0)} by A69, A70, FUNCT_1:165;
hence (Comput (P,s1,i)) | (dom (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) = (Comput (Q,s2,i)) | (dom (NPP ((Initialized Bubble-Sort-Algorithm) +* ((fsloc 0) .--> w)))) by A68; :: thesis: verum