let s be State of SCM+FSA ; :: thesis: ( IC s = insloc 0 & s . (intloc 0 ) = 1 implies for a being Int-Location
for k being Integer st a := k c= s & a <> intloc 0 holds
( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) ) )
assume that
A1:
IC s = insloc 0
and
A2:
s . (intloc 0 ) = 1
; :: thesis: for a being Int-Location
for k being Integer st a := k c= s & a <> intloc 0 holds
( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )
let a be Int-Location ; :: thesis: for k being Integer st a := k c= s & a <> intloc 0 holds
( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )
let k be Integer; :: thesis: ( a := k c= s & a <> intloc 0 implies ( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) ) )
assume that
A3:
a := k c= s
and
A4:
a <> intloc 0
; :: thesis: ( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )
per cases
( k > 0 or k <= 0 )
;
suppose A5:
k > 0
;
:: thesis: ( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )then consider k1 being
Element of
NAT such that A6:
(
k1 + 1
= k &
a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
by Def2;
set f =
(<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A7:
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 A6, FINSEQ_1:def 18
;
reconsider k =
k as
Element of
NAT by A5, 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 A7, 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: ( 1 <= i & i <= k + 1 implies ( i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) )assume A11:
( 1
<= i &
i <= k + 1 )
;
:: thesis: ( i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc (i -' 1) 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 -' 1) where m is Element of NAT : m in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) }
by Def1;
thus
i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)
by A9, A11, FINSEQ_1:3;
:: thesis: insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))hence
insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))
by A12;
:: thesis: verum end; A15:
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 A16:
(
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 A13;
hence s . (insloc i) =
(Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . (insloc i)
by A3, A6, GRFUNC_1:8
.=
((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1)
by A16, Def1
.=
((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1)
by A16, PARTFUN1:def 8
;
:: thesis: verum end; A17:
((<*(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
;
A18:
s . (insloc 0 ) =
((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1)
by A15
.=
a := (intloc 0 )
by A17
;
A19:
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 A20:
( 1
< i &
i <= k )
;
:: thesis: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = AddTo a,(intloc 0 )then A21:
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 A20, XREAL_1:11;
then A22:
i1 in Seg k1
by A6, A21, FINSEQ_1:3;
A23:
len <*(a := (intloc 0 ))*> = 1
by FINSEQ_1:56;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) = Seg k
by A7, FINSEQ_1:def 3;
then
i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 ))))
by A20, 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 A7, A20, A23, FINSEQ_1:37
.=
AddTo a,
(intloc 0 )
by A22, FUNCOP_1:13
;
:: thesis: verum end; ((<*(a := (intloc 0 ))*> ^ (k1 |-> (AddTo a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (k + 1) =
<*(halt SCM+FSA )*> . ((k + 1) - k)
by A7, A8, FINSEQ_1:37, XREAL_1:31
.=
halt SCM+FSA
by FINSEQ_1:def 8
;
then A28:
s . (insloc k) = halt SCM+FSA
by A15;
A29:
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 A30:
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
CurInstr (Computation s,n) = a := (intloc 0 )
by A1, A18;
:: thesis: Computation s,(n + 1) = Exec (a := (intloc 0 )),sthus Computation s,
(n + 1) =
Following (Computation s,n)
by AMI_1:14
.=
Exec (a := (intloc 0 )),
s
by A1, A18, A30
;
:: thesis: verum end; A31:
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 A32:
i <= k
;
:: thesis: IC (Computation s,i) = insloc i
defpred S1[
Element of
NAT ]
means ( $1
<= k implies
IC (Computation s,$1) = insloc $1 );
A33:
S1[
0 ]
by A1, AMI_1:13;
A34:
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 A35:
S1[
n]
;
:: thesis: S1[n + 1]
assume A36:
n + 1
<= k
;
:: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
then A37:
n < k
by NAT_1:13;
per cases
( n = 0 or n > 0 )
;
suppose A39:
n > 0
;
:: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
n + 0 <= n + 1
by XREAL_1:9;
then A40:
CurInstr (Computation s,n) =
s . (insloc n)
by A35, A36, AMI_1:54, XXREAL_0:2
.=
AddTo a,
(intloc 0 )
by A24, A37, A39
;
Computation s,
(n + 1) =
Following (Computation s,n)
by AMI_1:14
.=
Exec (AddTo a,(intloc 0 )),
(Computation s,n)
by A40
;
hence IC (Computation s,(n + 1)) =
Next (IC (Computation s,n))
by SCMFSA_2:90
.=
insloc (n + 1)
by A35, A36, NAT_1:13, NAT_1:39
;
:: thesis: verum end;
end;
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A33, A34);
hence
IC (Computation s,i) = insloc i
by A32;
:: thesis: verum
end; defpred S1[
Element of
NAT ]
means ( $1
<= k implies ( ( 1
<= $1 implies
(Computation s,$1) . a = $1 ) & ( for
b being
Int-Location st
b <> a holds
(Computation s,$1) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Computation s,$1) . f = s . f ) ) );
A41:
S1[
0 ]
by AMI_1:13;
A42:
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 A43:
S1[
n]
;
:: thesis: S1[n + 1]
assume A44:
n + 1
<= k
;
:: thesis: ( ( 1 <= n + 1 implies (Computation s,(n + 1)) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,(n + 1)) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,(n + 1)) . f = s . f ) )
per cases
( n = 0 or n > 0 )
;
suppose A47:
n > 0
;
:: thesis: ( ( 1 <= n + 1 implies (Computation s,(n + 1)) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,(n + 1)) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,(n + 1)) . f = s . f ) )then A48:
0 + 1
<= n
by INT_1:20;
A49:
n + 0 <= n + 1
by XREAL_1:9;
A50:
(
0 < n &
n < k )
by A44, A47, NAT_1:13;
A51:
CurInstr (Computation s,n) =
(Computation s,n) . (insloc n)
by A31, A44, A49, XXREAL_0:2
.=
s . (insloc n)
by AMI_1:54
.=
AddTo a,
(intloc 0 )
by A24, A50
;
A52:
Computation s,
(n + 1) =
Following (Computation s,n)
by AMI_1:14
.=
Exec (AddTo a,(intloc 0 )),
(Computation s,n)
by A51
;
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Computation s,(n + 1)) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,(n + 1)) . f = s . f ) )
assume
1
<= n + 1
;
:: thesis: (Computation s,(n + 1)) . a = n + 1thus (Computation s,(n + 1)) . a =
n + ((Computation s,n) . (intloc 0 ))
by A43, A44, A48, A49, A52, SCMFSA_2:90, XXREAL_0:2
.=
n + 1
by A2, A4, A43, A44, A49, XXREAL_0:2
;
:: thesis: verum
end; let f be
FinSeq-Location ;
:: thesis: (Computation s,(n + 1)) . f = s . fthus (Computation s,(n + 1)) . f =
(Computation s,n) . f
by A52, SCMFSA_2:90
.=
s . f
by A43, A44, A49, XXREAL_0:2
;
:: thesis: verum end;
end; A54:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A41, A42);
A55:
CurInstr (Computation s,k) =
(Computation s,k) . (insloc k)
by A31
.=
halt SCM+FSA
by A28, AMI_1:54
;
hence
s is
halting
by AMI_1:def 20;
:: thesis: ( (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )then A56:
Computation s,
k = Result s
by A55, AMI_1:def 22;
0 + 1
< k + 1
by A5, XREAL_1:8;
then
1
<= k
by NAT_1:13;
hence
(
(Result s) . a = k & ( for
b being
Int-Location st
b <> a holds
(Result s) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Result s) . f = s . f ) )
by A54, A56;
:: thesis: verum end; suppose A57:
k <= 0
;
:: thesis: ( s is halting & (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )then
- 0 <= - k
;
then reconsider mk =
- k as
Element of
NAT by INT_1:16;
consider k1 being
Element of
NAT such that A58:
(
k1 + k = 1 &
a := k = Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) )
by A57, Def2;
set f =
(<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>;
A59:
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 A58, FINSEQ_1:def 18
;
A60:
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 A59, FINSEQ_1:56
;
then A61:
dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) = Seg (((mk + 1) + 1) + 1)
by FINSEQ_1:def 3;
A62:
now let i be
Element of
NAT ;
:: thesis: ( 1 <= i & i <= ((mk + 1) + 1) + 1 implies ( i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) ) )assume A63:
( 1
<= i &
i <= ((mk + 1) + 1) + 1 )
;
:: thesis: ( i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) & insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) )A64:
dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) = { (m -' 1) where m is Element of NAT : m in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) }
by Def1;
thus
i in dom ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)
by A61, A63, FINSEQ_1:3;
:: thesis: insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))hence
insloc (i -' 1) in dom (Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>))
by A64;
:: thesis: verum end; A67:
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 A68:
(
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 A65;
hence s . (insloc i) =
(Load ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>)) . (insloc i)
by A3, A58, GRFUNC_1:8
.=
((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) /. (i + 1)
by A68, Def1
.=
((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (i + 1)
by A68, PARTFUN1:def 8
;
:: thesis: verum end; A69:
((<*(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
;
A70:
s . (insloc 0 ) =
((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . (0 + 1)
by A67
.=
a := (intloc 0 )
by A69
;
A71:
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 A72:
( 1
< i &
i <= (mk + 1) + 1 )
;
:: thesis: ((<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) ^ <*(halt SCM+FSA )*>) . i = SubFrom a,(intloc 0 )then A73:
1
- 1
< i - 1
by XREAL_1:11;
then A74:
(1 - 1) + 1
<= i - 1
by INT_1:20;
reconsider i1 =
i - 1 as
Element of
NAT by A73, INT_1:16;
i - 1
<= ((mk + 1) + 1) - 1
by A72, XREAL_1:11;
then A75:
i1 in Seg k1
by A58, A74, FINSEQ_1:3;
A76:
len <*(a := (intloc 0 ))*> = 1
by FINSEQ_1:56;
dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 )))) = Seg ((mk + 1) + 1)
by A59, FINSEQ_1:def 3;
then
i in dom (<*(a := (intloc 0 ))*> ^ (k1 |-> (SubFrom a,(intloc 0 ))))
by A72, 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 A59, A72, A76, FINSEQ_1:37
.=
SubFrom a,
(intloc 0 )
by A75, FUNCOP_1:13
;
:: 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 A59, A60, FINSEQ_1:37, XREAL_1:31
.=
halt SCM+FSA
by FINSEQ_1:def 8
;
then A81:
s . (insloc ((mk + 1) + 1)) = halt SCM+FSA
by A67;
A82:
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 A83:
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
CurInstr (Computation s,n) = a := (intloc 0 )
by A1, A70;
:: thesis: Computation s,(n + 1) = Exec (a := (intloc 0 )),sthus Computation s,
(n + 1) =
Following (Computation s,n)
by AMI_1:14
.=
Exec (a := (intloc 0 )),
s
by A1, A70, A83
;
:: thesis: verum end; A84:
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 A85:
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 );
A86:
S1[
0 ]
by A1, AMI_1:13;
A87:
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 A88:
S1[
n]
;
:: thesis: S1[n + 1]
assume A89:
n + 1
<= (mk + 1) + 1
;
:: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
then A90:
n < (mk + 1) + 1
by NAT_1:13;
per cases
( n = 0 or n > 0 )
;
suppose A92:
n > 0
;
:: thesis: IC (Computation s,(n + 1)) = insloc (n + 1)
n + 0 <= n + 1
by XREAL_1:9;
then A93:
CurInstr (Computation s,n) =
s . (insloc n)
by A88, A89, AMI_1:54, XXREAL_0:2
.=
SubFrom a,
(intloc 0 )
by A77, A90, A92
;
Computation s,
(n + 1) =
Following (Computation s,n)
by AMI_1:14
.=
Exec (SubFrom a,(intloc 0 )),
(Computation s,n)
by A93
;
hence IC (Computation s,(n + 1)) =
Next (IC (Computation s,n))
by SCMFSA_2:91
.=
insloc (n + 1)
by A88, A89, NAT_1:13, NAT_1:39
;
:: thesis: verum end;
end;
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A86, A87);
hence
IC (Computation s,i) = insloc i
by A85;
:: thesis: verum
end; defpred S1[
Element of
NAT ]
means ( $1
<= (mk + 1) + 1 implies ( ( 1
<= $1 implies
(Computation s,$1) . a = ((- $1) + 1) + 1 ) & ( for
b being
Int-Location st
b <> a holds
(Computation s,$1) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Computation s,$1) . f = s . f ) ) );
A94:
S1[
0 ]
by AMI_1:13;
A95:
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 A96:
S1[
n]
;
:: thesis: S1[n + 1]
assume A97:
n + 1
<= (mk + 1) + 1
;
:: thesis: ( ( 1 <= n + 1 implies (Computation s,(n + 1)) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,(n + 1)) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,(n + 1)) . f = s . f ) )
per cases
( n = 0 or n > 0 )
;
suppose A100:
n > 0
;
:: thesis: ( ( 1 <= n + 1 implies (Computation s,(n + 1)) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Computation s,(n + 1)) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,(n + 1)) . f = s . f ) )then A101:
0 + 1
< n + 1
by XREAL_1:8;
A102:
n + 0 <= n + 1
by XREAL_1:9;
A103:
(
0 < n &
n < (mk + 1) + 1 )
by A97, A100, NAT_1:13;
A104:
CurInstr (Computation s,n) =
(Computation s,n) . (insloc n)
by A84, A97, A102, XXREAL_0:2
.=
s . (insloc n)
by AMI_1:54
.=
SubFrom a,
(intloc 0 )
by A77, A103
;
A105:
Computation s,
(n + 1) =
Following (Computation s,n)
by AMI_1:14
.=
Exec (SubFrom a,(intloc 0 )),
(Computation s,n)
by A104
;
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Computation s,(n + 1)) . b = s . b ) & ( for f being FinSeq-Location holds (Computation s,(n + 1)) . f = s . f ) )
assume
1
<= n + 1
;
:: thesis: (Computation s,(n + 1)) . a = ((- (n + 1)) + 1) + 1thus (Computation s,(n + 1)) . a =
(((- n) + 1) + 1) - ((Computation s,n) . (intloc 0 ))
by A96, A97, A101, A105, NAT_1:13, SCMFSA_2:91
.=
(((- n) + 1) + 1) - (s . (intloc 0 ))
by A4, A96, A97, A102, XXREAL_0:2
.=
((- (n + 1)) + 1) + 1
by A2
;
:: thesis: verum
end; let f be
FinSeq-Location ;
:: thesis: (Computation s,(n + 1)) . f = s . fthus (Computation s,(n + 1)) . f =
(Computation s,n) . f
by A105, SCMFSA_2:91
.=
s . f
by A96, A97, A102, XXREAL_0:2
;
:: thesis: verum end;
end; A107:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A94, A95);
A108:
CurInstr (Computation s,((mk + 1) + 1)) =
(Computation s,((mk + 1) + 1)) . (insloc ((mk + 1) + 1))
by A84
.=
halt SCM+FSA
by A81, AMI_1:54
;
hence
s is
halting
by AMI_1:def 20;
:: thesis: ( (Result s) . a = k & ( for b being Int-Location st b <> a holds
(Result s) . b = s . b ) & ( for f being FinSeq-Location holds (Result s) . f = s . f ) )then A109:
Computation s,
((mk + 1) + 1) = Result s
by A108, AMI_1:def 22;
A110:
((- ((mk + 1) + 1)) + 1) + 1
= k
;
0 + 1
<= mk + (1 + 1)
by XREAL_1:9;
hence
(
(Result s) . a = k & ( for
b being
Int-Location st
b <> a holds
(Result s) . b = s . b ) & ( for
f being
FinSeq-Location holds
(Result s) . f = s . f ) )
by A107, A109, A110;
:: thesis: verum end;