let s be State of SCM+FSA ; :: thesis: ( IC s = insloc 0 implies for a being Int-Location
for k being Integer st a := k c= s holds
s is halting )
assume A1: IC s = insloc 0 ; :: thesis: for a being Int-Location
for k being Integer st a := k c= s holds
s is halting
let a be Int-Location ; :: thesis: for k being Integer st a := k c= s holds
s is halting
let k be Integer; :: thesis: ( a := k c= s implies s is halting )
assume A2: a := k c= s ; :: thesis: s is halting
per cases ( k > 0 or k <= 0 ) ;
suppose A3: k > 0 ; :: thesis: s is halting
then consider k1 being Element of NAT such that
A4: ( k1 + 1 = k & a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ) by SCMFSA_7:def 2;
set f = (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A5: 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 ;
reconsider k = k as Element of NAT by A3, INT_1:16;
A6: 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 A5, FINSEQ_1:56 ;
then A7: dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (k + 1) by FINSEQ_1:def 3;
A8: 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 )*>) & insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) )
assume A9: ( 0 <= i & i <= k ) ; :: thesis: ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) )
then ( 0 + 1 <= i + 1 & i + 1 <= k + 1 ) by XREAL_1:8;
hence i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A7, FINSEQ_1:3; :: thesis: insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))
( i < k + 1 & 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 A9, Th1, NAT_1:13;
hence insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A6; :: thesis: verum
end;
A10: now
let i be Element of NAT ; :: thesis: ( 0 <= i & i <= k implies s . (insloc i) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume ( 0 <= i & i <= k ) ; :: thesis: s . (insloc i) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A11: ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) by A8;
hence s . (insloc i) = (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . (insloc i) by A2, A4, GRFUNC_1:8
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A11, SCMFSA_7:def 1
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A11, PARTFUN1:def 8 ;
:: thesis: verum
end;
A12: ((<*(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 ;
A13: s . (insloc 0 ) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1) by A10
.= a := (intloc 0 ) by A12 ;
A14: 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 A15: ( 1 < i & i <= k ) ; :: thesis: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = AddTo a,(intloc 0 )
then A16: 1 <= i - 1 by INT_1:79;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
i - 1 <= k - 1 by A15, XREAL_1:11;
then A17: i1 in Seg k1 by A4, A16, FINSEQ_1:3;
A18: len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) = Seg k by A5, FINSEQ_1:def 3;
then i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) by A15, FINSEQ_1:3;
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 A5, A15, A18, FINSEQ_1:37
.= AddTo a,(intloc 0 ) by A17, FUNCOP_1:13 ;
:: thesis: verum
end;
A19: now
let i be Element of NAT ; :: thesis: ( 0 < i & i < k implies s . (insloc i) = AddTo a,(intloc 0 ) )
assume A20: ( 0 < i & i < k ) ; :: thesis: s . (insloc i) = AddTo a,(intloc 0 )
then A21: 0 + 1 < i + 1 by XREAL_1:8;
A22: i + 1 <= k by A20, NAT_1:13;
thus s . (insloc i) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A10, A20
.= AddTo a,(intloc 0 ) by A14, A21, A22 ; :: thesis: verum
end;
((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (k + 1) = <*(halt SCM+FSA )*> . ((k + 1) - k) by A5, A6, FINSEQ_1:37, XREAL_1:31
.= halt SCM+FSA by FINSEQ_1:def 8 ;
then A23: s . (insloc k) = halt SCM+FSA by A10;
A24: now
let n be Element of NAT ; :: thesis: ( n = 0 implies ( Computation s,n = s & CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s ) )
assume n = 0 ; :: thesis: ( Computation s,n = s & CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A25: Computation s,n = s by AMI_1:13; :: thesis: ( CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A26: CurInstr (Computation s,n) = a := (intloc 0 ) by A1, A13, AMI_1:def 17; :: thesis: Computation s,(n + 1) = Exec (a := (intloc 0 )),s
thus Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A25, A26, AMI_1:def 18 ; :: thesis: verum
end;
A27: for i being Element of NAT st i <= k holds
IC (Computation s,i) = insloc i
proof
let i be Element of NAT ; :: thesis: ( i <= k implies IC (Computation s,i) = insloc i )
assume A28: i <= k ; :: thesis: IC (Computation s,i) = insloc i
defpred S1[ Element of NAT ] means ( $1 <= k implies IC (Computation s,$1) = insloc $1 );
A29: S1[ 0 ] by A1, AMI_1:13;
A30: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A31: S1[n] ; :: thesis: S1[n + 1]
assume A32: n + 1 <= k ; :: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
then A33: n < k by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A34: n = 0 ; :: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
hence IC (Computation s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A24
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (insloc n) by A1, A34, SCMFSA_2:89
.= insloc (n + 1) by NAT_1:39 ;
:: thesis: verum
end;
suppose A35: n > 0 ; :: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
n + 0 <= n + 1 by XREAL_1:9;
then A36: CurInstr (Computation s,n) = (Computation s,n) . (insloc n) by A31, A32, AMI_1:def 17, XXREAL_0:2
.= s . (insloc n) by AMI_1:54
.= AddTo a,(intloc 0 ) by A19, A33, A35 ;
A37: Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (AddTo a,(intloc 0 )),(Computation s,n) by A36, AMI_1:def 18 ;
thus IC (Computation s,(n + 1)) = (Computation s,(n + 1)) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (IC (Computation s,n)) by A37, SCMFSA_2:90
.= insloc (n + 1) by A31, A32, NAT_1:13, NAT_1:39 ; :: thesis: verum
end;
end;
end;
for i being Element of NAT holds S1[i] from NAT_1:sch 1(A29, A30);
 hence IC (Computation s,i) = insloc i by A28; :: thesis: verum
end;
CurInstr (Computation s,k) = (Computation s,k) . (IC (Computation s,k)) by AMI_1:def 17
.= (Computation s,k) . (insloc k) by A27
.= halt SCM+FSA by A23, AMI_1:54 ;
hence s is halting by AMI_1:def 20; :: thesis: verum
end;
suppose A38: k <= 0 ; :: thesis: s is halting
then - 0 <= - k ;
then reconsider mk = - k as Element of NAT by INT_1:16;
consider k1 being Element of NAT such that
A39: ( k1 + k = 1 & a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) ) by A38, SCMFSA_7:def 2;
set f = (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A40: 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 A39, FINSEQ_1:def 18 ;
A41: 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 A40, FINSEQ_1:56 ;
then A42: dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (((mk + 1) + 1) + 1) by FINSEQ_1:def 3;
A43: 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 )*>) & insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) )
assume A44: ( 0 <= i & i <= (mk + 1) + 1 ) ; :: thesis: ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) )
then ( 0 + 1 <= i + 1 & i + 1 <= ((mk + 1) + 1) + 1 ) by XREAL_1:8;
hence i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) by A42, FINSEQ_1:3; :: thesis: insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))
( i < ((mk + 1) + 1) + 1 & 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 A44, Th1, NAT_1:13;
hence insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) by A41; :: thesis: verum
end;
A45: now
let i be Element of NAT ; :: thesis: ( 0 <= i & i <= (mk + 1) + 1 implies s . (insloc i) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume ( 0 <= i & i <= (mk + 1) + 1 ) ; :: thesis: s . (insloc i) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A46: ( i + 1 in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc i in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) by A43;
hence s . (insloc i) = (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . (insloc i) by A2, A39, GRFUNC_1:8
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A46, SCMFSA_7:def 1
.= ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A46, PARTFUN1:def 8 ;
:: thesis: verum
end;
A47: ((<*(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 ;
A48: s . (insloc 0 ) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1) by A45
.= a := (intloc 0 ) by A47 ;
A49: now
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 A50: ( 1 < i & i <= (mk + 1) + 1 ) ; :: thesis: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = SubFrom a,(intloc 0 )
then A51: 1 - 1 < i - 1 by XREAL_1:11;
then A52: (1 - 1) + 1 <= i - 1 by INT_1:20;
reconsider i1 = i - 1 as Element of NAT by A51, INT_1:16;
i - 1 <= ((mk + 1) + 1) - 1 by A50, XREAL_1:11;
then A53: i1 in Seg k1 by A39, A52, FINSEQ_1:3;
A54: len <*(a := (intloc 0 ))*> = 1 by FINSEQ_1:56;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) = Seg ((mk + 1) + 1) by A40, FINSEQ_1:def 3;
then i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) by A50, FINSEQ_1:3;
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 A40, A50, A54, FINSEQ_1:37
.= SubFrom a,(intloc 0 ) by A53, FUNCOP_1:13 ;
:: thesis: verum
end;
A55: now
let i be Element of NAT ; :: thesis: ( 0 < i & i < (mk + 1) + 1 implies s . (insloc i) = SubFrom a,(intloc 0 ) )
assume A56: ( 0 < i & i < (mk + 1) + 1 ) ; :: thesis: s . (insloc i) = SubFrom a,(intloc 0 )
then A57: 0 + 1 < i + 1 by XREAL_1:8;
A58: i + 1 <= (mk + 1) + 1 by A56, NAT_1:13;
thus s . (insloc i) = ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1) by A45, A56
.= SubFrom a,(intloc 0 ) by A49, A57, A58 ; :: 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 A40, A41, FINSEQ_1:37, XREAL_1:31
.= halt SCM+FSA by FINSEQ_1:def 8 ;
then A59: s . (insloc ((mk + 1) + 1)) = halt SCM+FSA by A45;
A60: now
let n be Element of NAT ; :: thesis: ( n = 0 implies ( Computation s,n = s & CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s ) )
assume n = 0 ; :: thesis: ( Computation s,n = s & CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A61: Computation s,n = s by AMI_1:13; :: thesis: ( CurInstr (Computation s,n) = a := (intloc 0 ) & Computation s,(n + 1) = Exec (a := (intloc 0 )),s )
hence A62: CurInstr (Computation s,n) = a := (intloc 0 ) by A1, A48, AMI_1:def 17; :: thesis: Computation s,(n + 1) = Exec (a := (intloc 0 )),s
thus Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (a := (intloc 0 )),s by A61, A62, AMI_1:def 18 ; :: thesis: verum
end;
A63: for i being Element of NAT st i <= (mk + 1) + 1 holds
IC (Computation s,i) = insloc i
proof
let i be Element of NAT ; :: thesis: ( i <= (mk + 1) + 1 implies IC (Computation s,i) = insloc i )
assume A64: i <= (mk + 1) + 1 ; :: thesis: IC (Computation s,i) = insloc i
defpred S1[ Element of NAT ] means ( $1 <= (mk + 1) + 1 implies IC (Computation s,$1) = insloc $1 );
A65: S1[ 0 ] by A1, AMI_1:13;
A66: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A67: S1[n] ; :: thesis: S1[n + 1]
assume A68: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
then A69: n < (mk + 1) + 1 by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A70: n = 0 ; :: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
hence IC (Computation s,(n + 1)) = IC (Exec (a := (intloc 0 )),s) by A60
.= (Exec (a := (intloc 0 )),s) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (insloc n) by A1, A70, SCMFSA_2:89
.= insloc (n + 1) by NAT_1:39 ;
:: thesis: verum
end;
suppose A71: n > 0 ; :: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
n + 0 <= n + 1 by XREAL_1:9;
then A72: CurInstr (Computation s,n) = (Computation s,n) . (insloc n) by A67, A68, AMI_1:def 17, XXREAL_0:2
.= s . (insloc n) by AMI_1:54
.= SubFrom a,(intloc 0 ) by A55, A69, A71 ;
A73: Computation s,(n + 1) = Following (Computation s,n) by AMI_1:14
.= Exec (SubFrom a,(intloc 0 )),(Computation s,n) by A72, AMI_1:def 18 ;
thus IC (Computation s,(n + 1)) = (Computation s,(n + 1)) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (IC (Computation s,n)) by A73, SCMFSA_2:91
.= insloc (n + 1) by A67, A68, NAT_1:13, NAT_1:39 ; :: thesis: verum
end;
end;
end;
for i being Element of NAT holds S1[i] from NAT_1:sch 1(A65, A66);
 hence IC (Computation s,i) = insloc i by A64; :: thesis: verum
end;
CurInstr (Computation s,((mk + 1) + 1)) = (Computation s,((mk + 1) + 1)) . (IC (Computation s,((mk + 1) + 1))) by AMI_1:def 17
.= (Computation s,((mk + 1) + 1)) . (insloc ((mk + 1) + 1)) by A63
.= halt SCM+FSA by A59, AMI_1:54 ;
hence s is halting by AMI_1:def 20; :: thesis: verum
end;
end;