set DD = {(),(),()};
let w be FinSequence of INT ; :: thesis:
set p = Initialized (() .--> w);
set q = Insert-Sort-Algorithm ;
set UD = {(),(),(),(),(),(),(),()};
set Us = \/ ;
A1: UsedILoc Insert-Sort-Algorithm = {(),(),(),(),(),(),()} by Th18;
A2: UsedI*Loc Insert-Sort-Algorithm = {()} by Th19;
then A3: (UsedI*Loc Insert-Sort-Algorithm) \/ = {(),(),(),(),(),(),(),()} by ;
A4: for i being Nat
for s1, s2 being State of SCM+FSA
for P1, P2 being Instruction-Sequence of SCM+FSA st 11 <= i & Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
proof
let i be Nat; :: thesis: for s1, s2 being State of SCM+FSA
for P1, P2 being Instruction-Sequence of SCM+FSA st 11 <= i & Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )

let s1, s2 be State of SCM+FSA; :: thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st 11 <= i & Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )

let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: ( 11 <= i & Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 implies ( (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () ) )
assume that
A5: 11 <= i and
A6: Initialized (() .--> w) c= s1 and
A7: Initialized (() .--> w) c= s2 and
A8: Insert-Sort-Algorithm c= P1 and
A9: Insert-Sort-Algorithm c= P2 ; :: thesis: ( (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
A10: s1 . () = 1 by
.= s2 . () by ;
A11: s2 is 0 -started by ;
set Cs11 = Comput (P1,s1,11);
set Cs21 = Comput (P2,s2,11);
A12: s1 is 0 -started by ;
A13: s1 . () = w by
.= s2 . () by ;
A14: now :: thesis: for x being set st x in \/ holds
(Comput (P1,s1,11)) . x = (Comput (P2,s2,11)) . x
let x be set ; :: thesis: ( x in \/ implies (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1 )
assume x in \/ ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
then A15: x in {(),(),(),(),(),(),(),()} by ;
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 ;
suppose A16: x = fsloc 0 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A13, A16, Lm2, A9 ;
:: thesis: verum
end;
suppose A17: x = intloc 0 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A10, A17, Lm2, A9 ;
:: thesis: verum
end;
suppose A18: x = intloc 1 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = len (s1 . ()) by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A13, A18, Lm2, A9 ;
:: thesis: verum
end;
suppose A19: x = intloc 2 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A10, A19, Lm2, A9 ;
:: thesis: verum
end;
suppose A20: x = intloc 3 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A10, A20, Lm2, A9 ;
:: thesis: verum
end;
suppose A21: x = intloc 4 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A10, A21, Lm2, A9 ;
:: thesis: verum
end;
suppose A22: x = intloc 5 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A10, A22, Lm2, A9 ;
:: thesis: verum
end;
suppose A23: x = intloc 6 ; :: thesis: (Comput (P1,s1,11)) . b1 = (Comput (P2,s2,11)) . b1
hence (Comput (P1,s1,11)) . x = s1 . () by A12, Lm2, A8
.= (Comput (P2,s2,11)) . x by A11, A10, A23, Lm2, A9 ;
:: thesis: verum
end;
end;
end;
A24: for i being Nat holds IC (Comput (P2,s2,i)) in dom Insert-Sort-Algorithm by A7, Th26, A9;
A25: for i being Nat holds IC (Comput (P1,s1,i)) in dom Insert-Sort-Algorithm by A6, Th26, A8;
A26: (UsedI*Loc Insert-Sort-Algorithm) \/ c= dom (Comput (P2,s2,11)) by SCMBSORT:32;
(UsedI*Loc Insert-Sort-Algorithm) \/ c= dom (Comput (P1,s1,11)) by SCMBSORT:32;
then A27: (Comput (P1,s1,11)) | = (Comput (P2,s2,11)) | by ;
(Comput (P1,s1,11)) . () = 11 by A12, Lm2, A8
.= (Comput (P2,s2,11)) . () by A11, Lm2, A9 ;
hence ( (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () ) by ; :: thesis: verum
end;
A28: for s1, s2 being State of SCM+FSA
for P1, P2 being Instruction-Sequence of SCM+FSA
for i being Nat st Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 holds
( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
proof
let s1, s2 be State of SCM+FSA; :: thesis: for P1, P2 being Instruction-Sequence of SCM+FSA
for i being Nat st Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 holds
( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )

let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for i being Nat st Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 holds
( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )

let i be Nat; :: thesis: ( Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 implies ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () ) )
assume that
A29: Initialized (() .--> w) c= s1 and
A30: Initialized (() .--> w) c= s2 and
A31: Insert-Sort-Algorithm c= P1 and
A32: Insert-Sort-Algorithm c= P2 and
A33: i <= 10 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
A34: s2 is 0 -started by ;
A35: s1 . () = w by
.= s2 . () by ;
A36: s1 . () = 1 by
.= s2 . () by ;
A37: s1 is 0 -started by ;
then A38: IC s1 = 0
.= IC s2 by A34 ;
not not i = 0 & ... & not i = 10 by A33;
per cases then ( 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 ) ;
suppose A39: i = 0 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () by A36; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () by ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () by ; :: thesis: verum
end;
suppose A40: i = 1 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A40, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 1 by A37, A40, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A40, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A40, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A40, Lm2, A32 ; :: thesis: verum
end;
suppose A41: i = 2 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A41, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 2 by A37, A41, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A41, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A41, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A41, Lm2, A32 ; :: thesis: verum
end;
suppose A42: i = 3 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A42, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 3 by A37, A42, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A42, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A42, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A42, Lm2, A32 ; :: thesis: verum
end;
suppose A43: i = 4 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A43, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 4 by A37, A43, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A43, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A43, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A43, Lm2, A32 ; :: thesis: verum
end;
suppose A44: i = 5 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A44, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 5 by A37, A44, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A44, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A44, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A44, Lm2, A32 ; :: thesis: verum
end;
suppose A45: i = 6 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A45, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 6 by A37, A45, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A45, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A45, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A45, Lm2, A32 ; :: thesis: verum
end;
suppose A46: i = 7 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A46, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 7 by A37, A46, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A46, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A46, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A46, Lm2, A32 ; :: thesis: verum
end;
suppose A47: i = 8 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A47, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 8 by A37, A47, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A47, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A47, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A47, Lm2, A32 ; :: thesis: verum
end;
suppose A48: i = 9 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A48, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 9 by A37, A48, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A48, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A48, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A48, Lm2, A32 ; :: thesis: verum
end;
suppose A49: i = 10 ; :: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
hence (Comput (P1,s1,i)) . () = s1 . () by
.= (Comput (P2,s2,i)) . () by A34, A36, A49, Lm2, A32 ;
:: thesis: ( (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () & (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . () )
thus (Comput (P1,s1,i)) . () = 10 by A37, A49, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A49, Lm2, A32 ; :: thesis: (Comput (P1,s1,i)) . () = (Comput (P2,s2,i)) . ()
thus (Comput (P1,s1,i)) . () = s1 . () by A37, A49, Lm2, A31
.= (Comput (P2,s2,i)) . () by A34, A35, A49, Lm2, A32 ; :: thesis: verum
end;
end;
end;
A50: dom (Initialized (() .--> w)) = {(),(),()} by SCMFSA_M:31;
reconsider ini = () .--> 1 as data-only FinPartState of SCM+FSA ;
for P, Q being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P & Insert-Sort-Algorithm c= Q holds
for s1, s2 being State of SCM+FSA st Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 holds
for i being Nat holds (Comput (P,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (Q,s2,i)) | (dom (Initialized (() .--> w)))
proof
let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 implies for s1, s2 being State of SCM+FSA st Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 holds
for i being Nat holds (Comput (P1,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized (() .--> w))) )

assume that
A51: Insert-Sort-Algorithm c= P1 and
A52: Insert-Sort-Algorithm c= P2 ; :: thesis: for s1, s2 being State of SCM+FSA st Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 holds
for i being Nat holds (Comput (P1,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized (() .--> w)))

let s1, s2 be State of SCM+FSA; :: thesis: ( Initialized (() .--> w) c= s1 & Initialized (() .--> w) c= s2 implies for i being Nat holds (Comput (P1,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized (() .--> w))) )
assume that
A53: Initialized (() .--> w) c= s1 and
A54: Initialized (() .--> w) c= s2 ; :: thesis: for i being Nat holds (Comput (P1,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized (() .--> w)))
let i be Nat; :: thesis: (Comput (P1,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized (() .--> w)))
reconsider i = i as Nat ;
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
A55: (UsedI*Loc Insert-Sort-Algorithm) \/ c= dom (Comput (P1,s1,i)) by SCMBSORT:32;
A56: fsloc 0 in \/ by ;
A57: (UsedI*Loc Insert-Sort-Algorithm) \/ c= dom (Comput (P2,s2,i)) by SCMBSORT:32;
A58: ( i > 10 implies 10 + 1 < i + 1 ) by XREAL_1:6;
A59: intloc 0 in \/ by ;
A60: now :: thesis: for x being set st x in {(),(),()} holds
(Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x
let x be set ; :: thesis: ( x in {(),(),()} implies (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1 )
assume A61: x in {(),(),()} ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
per cases ( x = intloc 0 or x = IC or x = fsloc 0 ) by ;
suppose A62: x = intloc 0 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
per cases ( i <= 10 or i > 10 ) ;
suppose i <= 10 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A28, A53, A54, A62, A51, A52; :: thesis: verum
end;
suppose i > 10 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
then 11 <= i by ;
then (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | by A4, A53, A54, A51, A52;
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by ; :: thesis: verum
end;
end;
end;
suppose A63: x = IC ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
per cases ( i <= 10 or i > 10 ) ;
suppose i <= 10 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A28, A53, A54, A63, A51, A52; :: thesis: verum
end;
suppose i > 10 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
then 11 <= i by ;
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A4, A53, A54, A63, A51, A52; :: thesis: verum
end;
end;
end;
suppose A64: x = fsloc 0 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
per cases ( i <= 10 or i > 10 ) ;
suppose i <= 10 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A28, A53, A54, A64, A51, A52; :: thesis: verum
end;
suppose i > 10 ; :: thesis: (Comput (P1,s1,i)) . b1 = (Comput (P2,s2,i)) . b1
then 11 <= i by ;
then (Comput (P1,s1,i)) | = (Comput (P2,s2,i)) | by A4, A53, A54, A51, A52;
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by ; :: thesis: verum
end;
end;
end;
end;
end;
A65: {(),(),()} c= dom (Comput (P2,s2,i)) by SCMFSA_M:34;
{(),(),()} c= dom (Comput (P1,s1,i)) by SCMFSA_M:34;
then (Comput (P1,s1,i)) | {(),(),()} = (Comput (P2,s2,i)) | {(),(),()} by ;
hence (Comput (P1,s1,i)) | (dom (Initialized (() .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized (() .--> w))) by A50; :: thesis: verum
end;
hence Initialized (() .--> w) is Insert-Sort-Algorithm -autonomic ; :: thesis: verum