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