let s be State of SCM+FSA ; :: thesis: ( IC s = 0 implies for a being Int-Location
for k being Integer st a := k c= s holds
ProgramPart s halts_on s )
assume A1: IC s = 0 ; :: thesis: for a being Int-Location
for k being Integer st a := k c= s holds
ProgramPart s halts_on s
let a be Int-Location ; :: thesis: for k being Integer st a := k c= s holds
ProgramPart s halts_on s
let k be Integer; :: thesis: ( a := k c= s implies ProgramPart s halts_on s )
assume A2: a := k c= s ; :: thesis: ProgramPart s halts_on s

per cases ( k > 0 or k <= 0 ) ;

suppose A3: k > 0 ; :: thesis: ProgramPart s halts_on s

then consider k1 being Element of NAT such that
A4: k1 + 1 = k and
A5: a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:def 2;
A6: len (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (AddTo a,(intloc 0 )))) by FINSEQ_1:35
.= 1 + (len (k1 |-> (AddTo a,(intloc 0 )))) by FINSEQ_1:56
.= k by A4, FINSEQ_1:def 18 ;
set f = (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A7: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . 1 = (<*(a := (intloc 0 ))*> ^ ((k1 |-> (AddTo a,(intloc 0 ))) ^ <*(halt SCM+FSA )*>)) . 1 by FINSEQ_1:45
.= a := (intloc 0 ) by FINSEQ_1:58 ;
reconsider k = k as Element of NAT by A3, INT_1:16;
A8: len ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = (len (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))))) + (len <*(halt SCM+FSA )*>) by FINSEQ_1:35
.= k + 1 by A6, FINSEQ_1:56 ;
then A9: dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (k + 1) by FINSEQ_1:def 3;

A10: now

let i be Element of NAT ; :: thesis: ( 0 <= i & i <= k implies ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) )
assume that
0 <= i and
A11: i <= k ; :: thesis: ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) )
( 0 + 1 <= i + 1 & i + 1 <= k + 1 ) by A11, XREAL_1:8;
hence i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A9; :: thesis: i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))
A12: dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) = { m where m is Element of NAT : m < len ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) } by Th1;
i < k + 1 by A11, NAT_1:13;
hence i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A8, A12; :: thesis: verum

end;

A13: now

let i be Element of NAT ; :: thesis: ( 0 <= i & i <= k implies s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume that
0 <= i and
A14: i <= k ; :: thesis: s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1)
B15: i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A10, A14;
A15: i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A10, A14;
hence s . i = (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . i by A2, A5, GRFUNC_1:8
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A15, SCMFSA_7:def 1
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by B15, PARTFUN1:def 8 ;
:: thesis: verum

end;

then A16: s . 0 = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1)
.= a := (intloc 0 ) by A7 ;

A17: now

let n be Element of NAT ; :: thesis: ( n = 0 implies ( Comput (ProgramPart s),s,n = s & CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s ) )
Y: (ProgramPart (Comput (ProgramPart s),s,n)) /. (IC (Comput (ProgramPart s),s,n)) = (Comput (ProgramPart s),s,n) . (IC (Comput (ProgramPart s),s,n)) by COMPOS_1:38;
assume n = 0 ; :: thesis: ( Comput (ProgramPart s),s,n = s & CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A18: Comput (ProgramPart s),s,n = s by AMI_1:13; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A19: CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) by A1, A16, Y, COMPOS_1:def 10; :: thesis: Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s
thus Comput (ProgramPart s),s,(n + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A18, A19, AMI_1:def 18 ; :: thesis: verum

end;

A20: now

let i be Element of NAT ; :: thesis: ( 1 < i & i <= k implies ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = AddTo a,(intloc 0 ) )
assume that
A21: 1 < i and
A22: i <= k ; :: thesis: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = AddTo a,(intloc 0 )
A23: 1 <= i - 1 by A21, INT_1:79;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
i - 1 <= k - 1 by A22, XREAL_1:11;
then A24: i1 in Seg k1 by A4, A23;
A25: len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) = Seg k by A6, FINSEQ_1:def 3;
then i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) by A21, A22;
hence ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) . i by FINSEQ_1:def 7
.= (k1 |-> (AddTo a,(intloc 0 ))) . (i - 1) by A6, A21, A22, A25, FINSEQ_1:37
.= AddTo a,(intloc 0 ) by A24, FUNCOP_1:13 ;
:: thesis: verum

end;

A26: now

let i be Element of NAT ; :: thesis: ( 0 < i & i < k implies s . i = AddTo a,(intloc 0 ) )
assume that
A27: 0 < i and
A28: i < k ; :: thesis: s . i = AddTo a,(intloc 0 )
A29: ( 0 + 1 < i + 1 & i + 1 <= k ) by A27, A28, NAT_1:13, XREAL_1:8;
thus s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A13, A28
.= AddTo a,(intloc 0 ) by A20, A29 ; :: thesis: verum

end;

A30: for i being Element of NAT st i <= k holds
IC (Comput (ProgramPart s),s,i) = i

proof

defpred S₁[ Nat] means ( $1 <= k implies IC (Comput (ProgramPart s),s,$1) = $1 );
let i be Element of NAT ; :: thesis: ( i <= k implies IC (Comput (ProgramPart s),s,i) = i )
assume A31: i <= k ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
A32: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A33: S₁[n] ; :: thesis: S₁[n + 1]
assume A34: n + 1 <= k ; :: thesis: IC (Comput (ProgramPart s),s,(n + 1)) = n + 1
then A35: n < k by NAT_1:13;

per cases ( n = 0 or n > 0 ) ;

suppose A36: n = 0 ; :: thesis: IC (Comput (ProgramPart s),s,(n + 1)) = n + 1

hence IC (Comput (ProgramPart s),s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A17
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ n by A1, A36, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis: verum

end;

suppose A37: n > 0 ; :: thesis: IC (Comput (ProgramPart s),s,(n + 1)) = n + 1

Y: (ProgramPart (Comput (ProgramPart s),s,n)) /. (IC (Comput (ProgramPart s),s,n)) = (Comput (ProgramPart s),s,n) . (IC (Comput (ProgramPart s),s,n)) by COMPOS_1:38;
n + 0 <= n + 1 by XREAL_1:9;
then A38: CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = (Comput (ProgramPart s),s,n) . n by A33, A34, Y, COMPOS_1:def 10, XXREAL_0:2
.= s . n by AMI_1:54
.= AddTo a,(intloc 0 ) by A26, A35, A37 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,n) by AMI_1:123;
A39: Comput (ProgramPart s),s,(n + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,n) by AMI_1:14
.= Exec (AddTo a,(intloc 0 )),(Comput (ProgramPart s),s,n) by A38, T, AMI_1:def 18 ;
thus IC (Comput (ProgramPart s),s,(n + 1)) = (Comput (ProgramPart s),s,(n + 1)) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ (IC (Comput (ProgramPart s),s,n)) by A39, SCMFSA_2:90
.= n + 1 by A33, A34, NAT_1:13, NAT_1:39 ; :: thesis: verum

end;

end;

end;

A40: S₁[ 0 ] by A1, AMI_1:13;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A40, A32);
hence IC (Comput (ProgramPart s),s,i) = i by A31; :: thesis: verum

end;

((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (k + 1) = <*(halt SCM+FSA )*> . ((k + 1) - k) by A6, A8, FINSEQ_1:37, XREAL_1:31
.= halt SCM+FSA by FINSEQ_1:def 8 ;
then A41: s . k = halt SCM+FSA by A13;
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,k) by AMI_1:123;
Y: (ProgramPart (Comput (ProgramPart s),s,k)) /. (IC (Comput (ProgramPart s),s,k)) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by COMPOS_1:38;
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,k) = (Comput (ProgramPart s),s,k) . (IC (Comput (ProgramPart s),s,k)) by Y, TX, COMPOS_1:def 10
.= (Comput (ProgramPart s),s,k) . k by A30
.= halt SCM+FSA by A41, AMI_1:54 ;
hence ProgramPart s halts_on s by AMI_1:146; :: thesis: verum

end;

suppose A42: k <= 0 ; :: thesis: ProgramPart s halts_on s

then reconsider mk = - k as Element of NAT by INT_1:16;
consider k1 being Element of NAT such that
A43: k1 + k = 1 and
A44: a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A42, SCMFSA_7:def 2;
A45: len (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) = (len <*(a := (intloc 0 ))*>) + (len (k1 |-> (SubFrom a,(intloc 0 )))) by FINSEQ_1:35
.= 1 + (len (k1 |-> (SubFrom a,(intloc 0 )))) by FINSEQ_1:56
.= (mk + 1) + 1 by A43, FINSEQ_1:def 18 ;
set f = (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A46: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . 1 = (<*(a := (intloc 0 ))*> ^ ((k1 |-> (SubFrom a,(intloc 0 ))) ^ <*(halt SCM+FSA )*>)) . 1 by FINSEQ_1:45
.= a := (intloc 0 ) by FINSEQ_1:58 ;
A47: len ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = (len (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))))) + (len <*(halt SCM+FSA )*>) by FINSEQ_1:35
.= ((mk + 1) + 1) + 1 by A45, FINSEQ_1:56 ;
then A48: dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (((mk + 1) + 1) + 1) by FINSEQ_1:def 3;

A49: now

let i be Element of NAT ; :: thesis: ( 0 <= i & i <= (mk + 1) + 1 implies ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) )
assume that
0 <= i and
A50: i <= (mk + 1) + 1 ; :: thesis: ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) )
( 0 + 1 <= i + 1 & i + 1 <= ((mk + 1) + 1) + 1 ) by A50, XREAL_1:8;
hence i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A48; :: thesis: i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))
A51: dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) = { m where m is Element of NAT : m < len ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) } by Th1;
i < ((mk + 1) + 1) + 1 by A50, NAT_1:13;
hence i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A47, A51; :: thesis: verum

end;

A52: now

let i be Element of NAT ; :: thesis: ( 0 <= i & i <= (mk + 1) + 1 implies s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume that
0 <= i and
A53: i <= (mk + 1) + 1 ; :: thesis: s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1)
B54: i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A49, A53;
A54: i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A49, A53;
hence s . i = (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . i by A2, A44, GRFUNC_1:8
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A54, SCMFSA_7:def 1
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by B54, PARTFUN1:def 8 ;
:: thesis: verum

end;

then A55: s . 0 = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1)
.= a := (intloc 0 ) by A46 ;

A56: now

let n be Element of NAT ; :: thesis: ( n = 0 implies ( Comput (ProgramPart s),s,n = s & CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s ) )
Y: (ProgramPart (Comput (ProgramPart s),s,n)) /. (IC (Comput (ProgramPart s),s,n)) = (Comput (ProgramPart s),s,n) . (IC (Comput (ProgramPart s),s,n)) by COMPOS_1:38;
assume n = 0 ; :: thesis: ( Comput (ProgramPart s),s,n = s & CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A57: Comput (ProgramPart s),s,n = s by AMI_1:13; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) & Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A58: CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = a := (intloc 0 ) by A1, A55, Y, COMPOS_1:def 10; :: thesis: Comput (ProgramPart s),s,(n + 1) = Exec (a := (intloc 0 )),s
thus Comput (ProgramPart s),s,(n + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A57, A58, AMI_1:def 18 ; :: thesis: verum

end;

A59: now

A60: len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
let i be Element of NAT ; :: thesis: ( 1 < i & i <= (mk + 1) + 1 implies ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = SubFrom a,(intloc 0 ) )
assume that
A61: 1 < i and
A62: i <= (mk + 1) + 1 ; :: thesis: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = SubFrom a,(intloc 0 )
A63: i - 1 <= ((mk + 1) + 1) - 1 by A62, XREAL_1:11;
A64: 1 - 1 < i - 1 by A61, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
(1 - 1) + 1 <= i - 1 by A64, INT_1:20;
then A65: i1 in Seg k1 by A43, A63;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) = Seg ((mk + 1) + 1) by A45, FINSEQ_1:def 3;
then i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) by A61, A62;
hence ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) . i by FINSEQ_1:def 7
.= (k1 |-> (SubFrom a,(intloc 0 ))) . (i - 1) by A45, A61, A62, A60, FINSEQ_1:37
.= SubFrom a,(intloc 0 ) by A65, FUNCOP_1:13 ;
:: thesis: verum

end;

A66: now

let i be Element of NAT ; :: thesis: ( 0 < i & i < (mk + 1) + 1 implies s . i = SubFrom a,(intloc 0 ) )
assume that
A67: 0 < i and
A68: i < (mk + 1) + 1 ; :: thesis: s . i = SubFrom a,(intloc 0 )
A69: ( 0 + 1 < i + 1 & i + 1 <= (mk + 1) + 1 ) by A67, A68, NAT_1:13, XREAL_1:8;
thus s . i = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A52, A68
.= SubFrom a,(intloc 0 ) by A59, A69 ; :: thesis: verum

end;

A70: for i being Element of NAT st i <= (mk + 1) + 1 holds
IC (Comput (ProgramPart s),s,i) = i

proof

defpred S₁[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (ProgramPart s),s,$1) = $1 );
let i be Element of NAT ; :: thesis: ( i <= (mk + 1) + 1 implies IC (Comput (ProgramPart s),s,i) = i )
assume A71: i <= (mk + 1) + 1 ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
A72: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A73: S₁[n] ; :: thesis: S₁[n + 1]
assume A74: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput (ProgramPart s),s,(n + 1)) = n + 1
then A75: n < (mk + 1) + 1 by NAT_1:13;

per cases ( n = 0 or n > 0 ) ;

suppose A76: n = 0 ; :: thesis: IC (Comput (ProgramPart s),s,(n + 1)) = n + 1

hence IC (Comput (ProgramPart s),s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A56
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ n by A1, A76, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis: verum

end;

suppose A77: n > 0 ; :: thesis: IC (Comput (ProgramPart s),s,(n + 1)) = n + 1

Y: (ProgramPart (Comput (ProgramPart s),s,n)) /. (IC (Comput (ProgramPart s),s,n)) = (Comput (ProgramPart s),s,n) . (IC (Comput (ProgramPart s),s,n)) by COMPOS_1:38;
n + 0 <= n + 1 by XREAL_1:9;
then A78: CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = (Comput (ProgramPart s),s,n) . n by A73, A74, Y, COMPOS_1:def 10, XXREAL_0:2
.= s . n by AMI_1:54
.= SubFrom a,(intloc 0 ) by A66, A75, A77 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,n) by AMI_1:123;
A79: Comput (ProgramPart s),s,(n + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,n) by AMI_1:14
.= Exec (SubFrom a,(intloc 0 )),(Comput (ProgramPart s),s,n) by A78, T, AMI_1:def 18 ;
thus IC (Comput (ProgramPart s),s,(n + 1)) = (Comput (ProgramPart s),s,(n + 1)) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ (IC (Comput (ProgramPart s),s,n)) by A79, SCMFSA_2:91
.= n + 1 by A73, A74, NAT_1:13, NAT_1:39 ; :: thesis: verum

end;

end;

end;

A80: S₁[ 0 ] by A1, AMI_1:13;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A80, A72);
hence IC (Comput (ProgramPart s),s,i) = i by A71; :: thesis: verum

end;

((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (((mk + 1) + 1) + 1) = <*(halt SCM+FSA )*> . ((((mk + 1) + 1) + 1) - ((mk + 1) + 1)) by A45, A47, FINSEQ_1:37, XREAL_1:31
.= halt SCM+FSA by FINSEQ_1:def 8 ;
then A81: s . ((mk + 1) + 1) = halt SCM+FSA by A52;
Y: (ProgramPart (Comput (ProgramPart s),s,((mk + 1) + 1))) /. (IC (Comput (ProgramPart s),s,((mk + 1) + 1))) = (Comput (ProgramPart s),s,((mk + 1) + 1)) . (IC (Comput (ProgramPart s),s,((mk + 1) + 1))) by COMPOS_1:38;
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,((mk + 1) + 1)) by AMI_1:123;
CurInstr (ProgramPart s),(Comput (ProgramPart s),s,((mk + 1) + 1)) = (Comput (ProgramPart s),s,((mk + 1) + 1)) . (IC (Comput (ProgramPart s),s,((mk + 1) + 1))) by Y, TX, COMPOS_1:def 10
.= (Comput (ProgramPart s),s,((mk + 1) + 1)) . ((mk + 1) + 1) by A70
.= halt SCM+FSA by A81, AMI_1:54 ;
hence ProgramPart s halts_on s by AMI_1:146; :: thesis: verum

end;

end;