let s be 0 -started State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
let P be Instruction-Sequence of SCM+FSA; ( Insert-Sort-Algorithm c= P implies ( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) ) )
assume A1:
Insert-Sort-Algorithm c= P
; ( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
A2:
IC (Comput (P,s,0)) = 0
by MEMSTR_0:def 11;
then A3: Comput (P,s,(0 + 1)) =
Exec ((P . 0),(Comput (P,s,0)))
by EXTPRO_1:6
.=
Exec (((intloc 2) := (intloc 0)),(Comput (P,s,0)))
by A1, Lm1
;
then A4: (Comput (P,s,1)) . (IC ) =
(IC (Comput (P,s,0))) + 1
by SCMFSA_2:63
.=
1
by A2
;
then
IC (Comput (P,s,1)) = 1
;
then A5: Comput (P,s,(1 + 1)) =
Exec ((P . 1),(Comput (P,s,1)))
by EXTPRO_1:6
.=
Exec ((goto 2),(Comput (P,s,1)))
by A1, Lm1
;
then A6:
(Comput (P,s,2)) . (IC ) = 2
by SCMFSA_2:69;
IC (Comput (P,s,2)) = 2
by A5, SCMFSA_2:69;
then A7: Comput (P,s,(2 + 1)) =
Exec ((P . 2),(Comput (P,s,2)))
by EXTPRO_1:6
.=
Exec (((intloc 3) := (intloc 0)),(Comput (P,s,2)))
by A1, Lm1
;
then A8: (Comput (P,s,3)) . (IC ) =
(IC (Comput (P,s,2))) + 1
by SCMFSA_2:63
.=
3
by A6
;
then
IC (Comput (P,s,3)) = 3
;
then A9: Comput (P,s,(3 + 1)) =
Exec ((P . 3),(Comput (P,s,3)))
by EXTPRO_1:6
.=
Exec ((goto 4),(Comput (P,s,3)))
by A1, Lm1
;
then A10:
(Comput (P,s,4)) . (IC ) = 4
by SCMFSA_2:69;
A11:
intloc 2 <> intloc 0
by SCMFSA_2:101;
then A12:
(Comput (P,s,1)) . (intloc 0) = s . (intloc 0)
by A3, SCMFSA_2:63;
then A13:
(Comput (P,s,2)) . (intloc 0) = s . (intloc 0)
by A5, SCMFSA_2:69;
then
(Comput (P,s,3)) . (intloc 3) = s . (intloc 0)
by A7, SCMFSA_2:63;
then A14:
(Comput (P,s,4)) . (intloc 3) = s . (intloc 0)
by A9, SCMFSA_2:69;
IC (Comput (P,s,4)) = 4
by A9, SCMFSA_2:69;
then A15: Comput (P,s,(4 + 1)) =
Exec ((P . 4),(Comput (P,s,4)))
by EXTPRO_1:6
.=
Exec (((intloc 4) := (intloc 0)),(Comput (P,s,4)))
by A1, Lm1
;
then A16: (Comput (P,s,5)) . (IC ) =
(IC (Comput (P,s,4))) + 1
by SCMFSA_2:63
.=
5
by A10
;
then
IC (Comput (P,s,5)) = 5
;
then A17: Comput (P,s,(5 + 1)) =
Exec ((P . 5),(Comput (P,s,5)))
by EXTPRO_1:6
.=
Exec ((goto 6),(Comput (P,s,5)))
by A1, Lm1
;
then A18:
(Comput (P,s,6)) . (IC ) = 6
by SCMFSA_2:69;
IC (Comput (P,s,6)) = 6
by A17, SCMFSA_2:69;
then A19: Comput (P,s,(6 + 1)) =
Exec ((P . 6),(Comput (P,s,6)))
by EXTPRO_1:6
.=
Exec (((intloc 5) := (intloc 0)),(Comput (P,s,6)))
by A1, Lm1
;
then A20: (Comput (P,s,7)) . (IC ) =
(IC (Comput (P,s,6))) + 1
by SCMFSA_2:63
.=
7
by A18
;
then
IC (Comput (P,s,7)) = 7
;
then A21: Comput (P,s,(7 + 1)) =
Exec ((P . 7),(Comput (P,s,7)))
by EXTPRO_1:6
.=
Exec ((goto 8),(Comput (P,s,7)))
by A1, Lm1
;
then A22:
(Comput (P,s,8)) . (IC ) = 8
by SCMFSA_2:69;
IC (Comput (P,s,8)) = 8
by A21, SCMFSA_2:69;
then A23: Comput (P,s,(8 + 1)) =
Exec ((P . 8),(Comput (P,s,8)))
by EXTPRO_1:6
.=
Exec (((intloc 6) := (intloc 0)),(Comput (P,s,8)))
by A1, Lm1
;
then A24: (Comput (P,s,9)) . (IC ) =
(IC (Comput (P,s,8))) + 1
by SCMFSA_2:63
.=
9
by A22
;
then
IC (Comput (P,s,9)) = 9
;
then A25: Comput (P,s,(9 + 1)) =
Exec ((P . 9),(Comput (P,s,9)))
by EXTPRO_1:6
.=
Exec ((goto 10),(Comput (P,s,9)))
by A1, Lm1
;
then A26:
(Comput (P,s,10)) . (IC ) = 10
by SCMFSA_2:69;
A27:
(Comput (P,s,1)) . (fsloc 0) = s . (fsloc 0)
by A3, SCMFSA_2:63;
then A28:
(Comput (P,s,2)) . (fsloc 0) = s . (fsloc 0)
by A5, SCMFSA_2:69;
then A29:
(Comput (P,s,3)) . (fsloc 0) = s . (fsloc 0)
by A7, SCMFSA_2:63;
then A30:
(Comput (P,s,4)) . (fsloc 0) = s . (fsloc 0)
by A9, SCMFSA_2:69;
then A31:
(Comput (P,s,5)) . (fsloc 0) = s . (fsloc 0)
by A15, SCMFSA_2:63;
then A32:
(Comput (P,s,6)) . (fsloc 0) = s . (fsloc 0)
by A17, SCMFSA_2:69;
then A33:
(Comput (P,s,7)) . (fsloc 0) = s . (fsloc 0)
by A19, SCMFSA_2:63;
then A34:
(Comput (P,s,8)) . (fsloc 0) = s . (fsloc 0)
by A21, SCMFSA_2:69;
then A35:
(Comput (P,s,9)) . (fsloc 0) = s . (fsloc 0)
by A23, SCMFSA_2:63;
then A36:
(Comput (P,s,10)) . (fsloc 0) = s . (fsloc 0)
by A25, SCMFSA_2:69;
A37:
(Comput (P,s,3)) . (intloc 0) = s . (intloc 0)
by A13, A7, SCMFSA_2:63;
then A38:
(Comput (P,s,4)) . (intloc 0) = s . (intloc 0)
by A9, SCMFSA_2:69;
then
(Comput (P,s,5)) . (intloc 4) = s . (intloc 0)
by A15, SCMFSA_2:63;
then A39:
(Comput (P,s,6)) . (intloc 4) = s . (intloc 0)
by A17, SCMFSA_2:69;
A40:
intloc 4 <> intloc 0
by SCMFSA_2:101;
then A41:
(Comput (P,s,5)) . (intloc 0) = s . (intloc 0)
by A38, A15, SCMFSA_2:63;
then A42:
(Comput (P,s,6)) . (intloc 0) = s . (intloc 0)
by A17, SCMFSA_2:69;
then
(Comput (P,s,7)) . (intloc 5) = s . (intloc 0)
by A19, SCMFSA_2:63;
then A43:
(Comput (P,s,8)) . (intloc 5) = s . (intloc 0)
by A21, SCMFSA_2:69;
intloc 4 <> intloc 5
by SCMFSA_2:101;
then
(Comput (P,s,7)) . (intloc 4) = s . (intloc 0)
by A39, A19, SCMFSA_2:63;
then A44:
(Comput (P,s,8)) . (intloc 4) = s . (intloc 0)
by A21, SCMFSA_2:69;
intloc 4 <> intloc 6
by SCMFSA_2:101;
then
(Comput (P,s,9)) . (intloc 4) = s . (intloc 0)
by A44, A23, SCMFSA_2:63;
then A45:
(Comput (P,s,10)) . (intloc 4) = s . (intloc 0)
by A25, SCMFSA_2:69;
intloc 5 <> intloc 6
by SCMFSA_2:101;
then
(Comput (P,s,9)) . (intloc 5) = s . (intloc 0)
by A43, A23, SCMFSA_2:63;
then A46:
(Comput (P,s,10)) . (intloc 5) = s . (intloc 0)
by A25, SCMFSA_2:69;
A47:
intloc 5 <> intloc 0
by SCMFSA_2:101;
then A48:
(Comput (P,s,7)) . (intloc 0) = s . (intloc 0)
by A42, A19, SCMFSA_2:63;
then A49:
(Comput (P,s,8)) . (intloc 0) = s . (intloc 0)
by A21, SCMFSA_2:69;
then
(Comput (P,s,9)) . (intloc 6) = s . (intloc 0)
by A23, SCMFSA_2:63;
then A50:
(Comput (P,s,10)) . (intloc 6) = s . (intloc 0)
by A25, SCMFSA_2:69;
IC (Comput (P,s,10)) = 10
by A25, SCMFSA_2:69;
then A51: Comput (P,s,(10 + 1)) =
Exec ((P . 10),(Comput (P,s,10)))
by EXTPRO_1:6
.=
Exec (((intloc 1) :=len (fsloc 0)),(Comput (P,s,10)))
by A1, Lm1
;
then A52: (Comput (P,s,11)) . (IC ) =
(IC (Comput (P,s,10))) + 1
by SCMFSA_2:74
.=
11
by A26
;
A53:
intloc 6 <> intloc 0
by SCMFSA_2:101;
then A54:
(Comput (P,s,9)) . (intloc 0) = s . (intloc 0)
by A49, A23, SCMFSA_2:63;
then A55:
(Comput (P,s,10)) . (intloc 0) = s . (intloc 0)
by A25, SCMFSA_2:69;
hereby ( (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
let k be
Nat;
( k > 0 & k < 12 implies ( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) ) )assume that A56:
k > 0
and A57:
k < 12
;
( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )set c1 =
(Comput (P,s,k)) . (IC );
set d1 =
k;
set c2 =
(Comput (P,s,k)) . (intloc 0);
set d2 =
s . (intloc 0);
set c3 =
(Comput (P,s,k)) . (fsloc 0);
set d3 =
s . (fsloc 0);
k < 11
+ 1
by A57;
then
k <= 11
by NAT_1:13;
then
not not
k = 0 & ... & not
k = 11
;
per cases then
( k = 1 or k = 2 or k = 3 or k = 4 or k = 5 or k = 6 or k = 7 or k = 8 or k = 9 or k = 10 or k = 11 )
by A56;
suppose
k = 3
;
( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput (P,s,k)) . (IC ) = k &
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0) &
(Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )
by A13, A28, A7, A8, SCMFSA_2:63;
verum end; suppose
k = 5
;
( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput (P,s,k)) . (IC ) = k &
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0) &
(Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )
by A38, A30, A15, A16, A40, SCMFSA_2:63;
verum end; suppose
k = 7
;
( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput (P,s,k)) . (IC ) = k &
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0) &
(Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )
by A42, A32, A19, A20, A47, SCMFSA_2:63;
verum end; suppose
k = 9
;
( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(
(Comput (P,s,k)) . (IC ) = k &
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0) &
(Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )
by A49, A34, A23, A24, A53, SCMFSA_2:63;
verum end; suppose A58:
k = 11
;
( (Comput (P,s,b1)) . (IC ) = b1 & (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,b1)) . (fsloc 0) = s . (fsloc 0) )hence
(Comput (P,s,k)) . (IC ) = k
by A52;
( (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) )thus
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
by A55, A51, A58, SCMFSA_2:74;
(Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0)thus
(Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0)
by A36, A51, A58, SCMFSA_2:74;
verum end; end;
end;
thus
(Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0))
by A36, A51, SCMFSA_2:74; ( (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
(Comput (P,s,1)) . (intloc 2) = s . (intloc 0)
by A3, SCMFSA_2:63;
then A59:
(Comput (P,s,2)) . (intloc 2) = s . (intloc 0)
by A5, SCMFSA_2:69;
intloc 2 <> intloc 3
by SCMFSA_2:101;
then
(Comput (P,s,3)) . (intloc 2) = s . (intloc 0)
by A59, A7, SCMFSA_2:63;
then A60:
(Comput (P,s,4)) . (intloc 2) = s . (intloc 0)
by A9, SCMFSA_2:69;
intloc 2 <> intloc 4
by SCMFSA_2:101;
then
(Comput (P,s,5)) . (intloc 2) = s . (intloc 0)
by A60, A15, SCMFSA_2:63;
then A61:
(Comput (P,s,6)) . (intloc 2) = s . (intloc 0)
by A17, SCMFSA_2:69;
intloc 2 <> intloc 5
by SCMFSA_2:101;
then
(Comput (P,s,7)) . (intloc 2) = s . (intloc 0)
by A61, A19, SCMFSA_2:63;
then A62:
(Comput (P,s,8)) . (intloc 2) = s . (intloc 0)
by A21, SCMFSA_2:69;
intloc 2 <> intloc 6
by SCMFSA_2:101;
then
(Comput (P,s,9)) . (intloc 2) = s . (intloc 0)
by A62, A23, SCMFSA_2:63;
then A63:
(Comput (P,s,10)) . (intloc 2) = s . (intloc 0)
by A25, SCMFSA_2:69;
intloc 3 <> intloc 4
by SCMFSA_2:101;
then
(Comput (P,s,5)) . (intloc 3) = s . (intloc 0)
by A14, A15, SCMFSA_2:63;
then A64:
(Comput (P,s,6)) . (intloc 3) = s . (intloc 0)
by A17, SCMFSA_2:69;
intloc 3 <> intloc 5
by SCMFSA_2:101;
then
(Comput (P,s,7)) . (intloc 3) = s . (intloc 0)
by A64, A19, SCMFSA_2:63;
then A65:
(Comput (P,s,8)) . (intloc 3) = s . (intloc 0)
by A21, SCMFSA_2:69;
intloc 3 <> intloc 6
by SCMFSA_2:101;
then
(Comput (P,s,9)) . (intloc 3) = s . (intloc 0)
by A65, A23, SCMFSA_2:63;
then A66:
(Comput (P,s,10)) . (intloc 3) = s . (intloc 0)
by A25, SCMFSA_2:69;
intloc 2 <> intloc 1
by SCMFSA_2:101;
hence
(Comput (P,s,11)) . (intloc 2) = s . (intloc 0)
by A63, A51, SCMFSA_2:74; ( (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
intloc 3 <> intloc 1
by SCMFSA_2:101;
hence
(Comput (P,s,11)) . (intloc 3) = s . (intloc 0)
by A66, A51, SCMFSA_2:74; ( (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
intloc 4 <> intloc 1
by SCMFSA_2:101;
hence
(Comput (P,s,11)) . (intloc 4) = s . (intloc 0)
by A45, A51, SCMFSA_2:74; ( (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) )
intloc 5 <> intloc 1
by SCMFSA_2:101;
hence
(Comput (P,s,11)) . (intloc 5) = s . (intloc 0)
by A46, A51, SCMFSA_2:74; (Comput (P,s,11)) . (intloc 6) = s . (intloc 0)
intloc 6 <> intloc 1
by SCMFSA_2:101;
hence
(Comput (P,s,11)) . (intloc 6) = s . (intloc 0)
by A50, A51, SCMFSA_2:74; verum