let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st a := k c= P & a <> intloc 0 holds
( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
let s be 0 -started State of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 implies for a being Int-Location
for k being Integer st a := k c= P & a <> intloc 0 holds
( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) )
assume A1: s . (intloc 0) = 1 ; :: thesis: for a being Int-Location
for k being Integer st a := k c= P & a <> intloc 0 holds
( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
A2: IC s = 0 by MEMSTR_0:def 11;
let a be Int-Location; :: thesis: for k being Integer st a := k c= P & a <> intloc 0 holds
( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
let k be Integer; :: thesis: ( a := k c= P & a <> intloc 0 implies ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) )
assume that
A3: a := k c= P and
A4: a <> intloc 0 ; :: thesis: ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
per cases ( k > 0 or k <= 0 ) ;
suppose A5: k > 0 ; :: thesis: ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
then consider k1 being Nat such that
A6: k1 + 1 = k and
A7: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) by Def1;
A8: len (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) = (len <%(a := (intloc 0))%>) + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:17
.= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:33
.= k by A6 ;
reconsider k = k as Element of NAT by A5, INT_1:3;
defpred S1[ Nat] means ( $1 <= k implies ( ( 1 <= $1 implies (Comput (P,s,$1)) . a = $1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) );
set f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA);
A9: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . 0 = (<%(a := (intloc 0))%> ^ ((k1 --> (AddTo (a,(intloc 0)))) ^ (Stop SCM+FSA))) . 0 by AFINSQ_1:27
.= a := (intloc 0) by AFINSQ_1:35 ;
A10: len ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) = (len (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))))) + (len (Stop SCM+FSA)) by AFINSQ_1:17
.= k + 1 by A8, AFINSQ_1:33 ;
A11: now :: thesis: for i being Nat st i <= k holds
i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA))
let i be Nat; :: thesis: ( i <= k implies i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) )
assume A12: i <= k ; :: thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA))
i < len ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) by A12, NAT_1:13, A10;
hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) by AFINSQ_1:86; :: thesis: verum
end;
A13: for i being Nat st i <= k holds
P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i by A3, A7, A11, GRFUNC_1:2;
then A14: P . 0 = a := (intloc 0) by A9;
A15: now :: thesis: for n being Nat st n = 0 holds
( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
let n be Nat; :: thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) )
assume n = 0 ; :: thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence A16: Comput (P,s,n) = s by EXTPRO_1:2; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A2, A14, PBOOLE:143; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)
thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((a := (intloc 0)),s) by A2, A14, A16, PBOOLE:143 ; :: thesis: verum
end;
A17: now :: thesis: for i being Nat st 1 <= i & i < k holds
((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = AddTo (a,(intloc 0))
let i be Nat; :: thesis: ( 1 <= i & i < k implies ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = AddTo (a,(intloc 0)) )
assume that
A18: 1 <= i and
A19: i < k ; :: thesis: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = AddTo (a,(intloc 0))
reconsider i1 = i - 1 as Element of NAT by A18, INT_1:5;
i - 1 < k - 1 by A19, XREAL_1:9;
then A20: i1 in Segm k1 by A6, NAT_1:44;
A21: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33;
A22: len (k1 --> (AddTo (a,(intloc 0)))) = k1 ;
i in dom (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) by A19, A8, AFINSQ_1:86;
hence ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) . i by AFINSQ_1:def 3
.= (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A18, A19, A21, A22, A6, AFINSQ_1:18
.= AddTo (a,(intloc 0)) by A20, FUNCOP_1:7 ;
:: thesis: verum
end;
A23: now :: thesis: for i being Nat st 0 < i & i < k holds
P . i = AddTo (a,(intloc 0))
let i be Nat; :: thesis: ( 0 < i & i < k implies P . i = AddTo (a,(intloc 0)) )
assume that
A24: 0 < i and
A25: i < k ; :: thesis: P . i = AddTo (a,(intloc 0))
A26: 0 + 1 <= i by A24, NAT_1:13;
thus P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i by A13, A25
.= AddTo (a,(intloc 0)) by A17, A26, A25 ; :: thesis: verum
end;
A27: for i being Nat st i <= k holds
IC (Comput (P,s,i)) = i
proof
defpred S2[ Nat] means ( $1 <= k implies IC (Comput (P,s,$1)) = $1 );
let i be Nat; :: thesis: ( i <= k implies IC (Comput (P,s,i)) = i )
assume A28: i <= k ; :: thesis: IC (Comput (P,s,i)) = i
A29: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A30: S2[n] ; :: thesis: S2[n + 1]
assume A31: n + 1 <= k ; :: thesis: IC (Comput (P,s,(n + 1))) = n + 1
then A32: n < k by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A33: n = 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = n + 1
hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A15
.= n + 1 by A2, A33, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose A34: n > 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = n + 1
n + 0 <= n + 1 by XREAL_1:7;
then A35: CurInstr (P,(Comput (P,s,n))) = P . n by A30, A31, PBOOLE:143, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A23, A32, A34 ;
Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((AddTo (a,(intloc 0))),(Comput (P,s,n))) by A35 ;
hence IC (Comput (P,s,(n + 1))) = n + 1 by A30, A31, NAT_1:13, SCMFSA_2:64; :: thesis: verum
end;
end;
end;
A36: S2[ 0 ] by A2, EXTPRO_1:2;
for i being Nat holds S2[i] from NAT_1:sch 2(A36, A29);
 hence IC (Comput (P,s,i)) = i by A28; :: thesis: verum
end;
A37: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A38: S1[n] ; :: thesis: S1[n + 1]
assume A39: n + 1 <= k ; :: thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
per cases ( n = 0 or n > 0 ) ;
suppose A40: n = 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput (P,s,(n + 1))) . a = n + 1
thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A15, A40
.= n + 1 by A1, A40, SCMFSA_2:63 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f
let b be Int-Location; :: thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b )
assume A41: b <> a ; :: thesis: (Comput (P,s,(n + 1))) . b = s . b
thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A15, A40
.= s . b by A41, SCMFSA_2:63 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput (P,s,(n + 1))) . f = s . f
thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A15, A40
.= s . f by SCMFSA_2:63 ; :: thesis: verum
end;
suppose A42: n > 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
A43: n < k by A39, NAT_1:13;
A44: P /. (IC (Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by PBOOLE:143;
A45: n + 0 <= n + 1 by XREAL_1:7;
then A46: CurInstr (P,(Comput (P,s,n))) = P . n by A27, A39, A44, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A23, A42, A43 ;
A47: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((AddTo (a,(intloc 0))),(Comput (P,s,n))) by A46 ;
A48: 0 + 1 <= n by A42, INT_1:7;
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput (P,s,(n + 1))) . a = n + 1
thus (Comput (P,s,(n + 1))) . a = n + ((Comput (P,s,n)) . (intloc 0)) by A38, A39, A48, A45, A47, SCMFSA_2:64, XXREAL_0:2
.= n + 1 by A1, A4, A38, A39, A45, XXREAL_0:2 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f
let b be Int-Location; :: thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b )
assume A49: b <> a ; :: thesis: (Comput (P,s,(n + 1))) . b = s . b
hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A47, SCMFSA_2:64
.= s . b by A38, A39, A45, A49, XXREAL_0:2 ;
:: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput (P,s,(n + 1))) . f = s . f
thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A47, SCMFSA_2:64
.= s . f by A38, A39, A45, XXREAL_0:2 ; :: thesis: verum
end;
end;
end;
len (Stop SCM+FSA) = 1 by AFINSQ_1:34;
then k < k + (len (Stop SCM+FSA)) by XREAL_1:29;
then A50: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA)) . k = (Stop SCM+FSA) . (k - k) by A8, AFINSQ_1:18
.= halt SCM+FSA ;
0 + 1 < k + 1 by A5, XREAL_1:6;
then A51: 1 <= k by NAT_1:13;
A52: S1[ 0 ] by EXTPRO_1:2;
A53: for i being Nat holds S1[i] from NAT_1:sch 2(A52, A37);
A54: P /. (IC (Comput (P,s,k))) = P . (IC (Comput (P,s,k))) by PBOOLE:143;
A55: CurInstr (P,(Comput (P,s,k))) = P . k by A27, A54
.= halt SCM+FSA by A50, A13 ;
hence P halts_on s by EXTPRO_1:29; :: thesis: ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
then Comput (P,s,k) = Result (P,s) by A55, EXTPRO_1:def 9;
hence ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) by A53, A51; :: thesis: verum
end;
suppose A56: k <= 0 ; :: thesis: ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
then reconsider mk = - k as Element of NAT by INT_1:3;
defpred S1[ Nat] means ( $1 <= (mk + 1) + 1 implies ( ( 1 <= $1 implies (Comput (P,s,$1)) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) );
consider k1 being Nat such that
A57: k1 + k = 1 and
A58: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA) by A56, Def1;
A59: len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:17
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:33
.= (mk + 1) + 1 by A57 ;
set f = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA);
A60: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . 0 = (<%(a := (intloc 0))%> ^ ((k1 --> (SubFrom (a,(intloc 0)))) ^ (Stop SCM+FSA))) . 0 by AFINSQ_1:27
.= a := (intloc 0) by AFINSQ_1:35 ;
A61: len ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) = (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) by AFINSQ_1:17
.= ((mk + 1) + 1) + 1 by A59, AFINSQ_1:33 ;
A62: now :: thesis: for i being Nat st i <= (mk + 1) + 1 holds
i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA))
let i be Nat; :: thesis: ( i <= (mk + 1) + 1 implies i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) )
assume A63: i <= (mk + 1) + 1 ; :: thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA))
i < ((mk + 1) + 1) + 1 by A63, NAT_1:13;
hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) by A61, AFINSQ_1:86; :: thesis: verum
end;
A64: for i being Nat st i <= (mk + 1) + 1 holds
P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i by A3, A58, GRFUNC_1:2, A62;
then A65: P . 0 = a := (intloc 0) by A60;
A66: now :: thesis: for n being Nat st n = 0 holds
( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
let n be Nat; :: thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) )
assume n = 0 ; :: thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence A67: Comput (P,s,n) = s by EXTPRO_1:2; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A2, A65, PBOOLE:143; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)
thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((a := (intloc 0)),s) by A2, A65, A67, PBOOLE:143 ; :: thesis: verum
end;
A68: now :: thesis: for i being Nat st 1 <= i & i < (mk + 1) + 1 holds
((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = SubFrom (a,(intloc 0))
A69: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33;
let i be Nat; :: thesis: ( 1 <= i & i < (mk + 1) + 1 implies ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = SubFrom (a,(intloc 0)) )
assume that
A70: 1 <= i and
A71: i < (mk + 1) + 1 ; :: thesis: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = SubFrom (a,(intloc 0))
reconsider i1 = i - 1 as Element of NAT by A70, INT_1:5;
i - 1 < (k1 + 1) - 1 by A71, A57, XREAL_1:9;
then A72: i1 in Segm k1 by NAT_1:44;
A73: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 ;
i in dom (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) by A71, A59, AFINSQ_1:86;
hence ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) . i by AFINSQ_1:def 3
.= (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A57, A70, A71, A69, A73, AFINSQ_1:18
.= SubFrom (a,(intloc 0)) by A72, FUNCOP_1:7 ;
:: thesis: verum
end;
A74: now :: thesis: for i being Nat st 0 < i & i < (mk + 1) + 1 holds
P . i = SubFrom (a,(intloc 0))
let i be Nat; :: thesis: ( 0 < i & i < (mk + 1) + 1 implies P . i = SubFrom (a,(intloc 0)) )
assume that
A75: 0 < i and
A76: i < (mk + 1) + 1 ; :: thesis: P . i = SubFrom (a,(intloc 0))
A77: 0 + 1 <= i by A75, NAT_1:13;
thus P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . i by A64, A76
.= SubFrom (a,(intloc 0)) by A68, A77, A76 ; :: thesis: verum
end;
A78: for i being Nat st i <= (mk + 1) + 1 holds
IC (Comput (P,s,i)) = i
proof
defpred S2[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (P,s,$1)) = $1 );
let i be Nat; :: thesis: ( i <= (mk + 1) + 1 implies IC (Comput (P,s,i)) = i )
assume A79: i <= (mk + 1) + 1 ; :: thesis: IC (Comput (P,s,i)) = i
A80: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A81: S2[n] ; :: thesis: S2[n + 1]
assume A82: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput (P,s,(n + 1))) = n + 1
then A83: n < (mk + 1) + 1 by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A84: n = 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = n + 1
hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A66
.= n + 1 by A2, A84, SCMFSA_2:63 ;
:: thesis: verum
end;
suppose A85: n > 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = n + 1
n + 0 <= n + 1 by XREAL_1:7;
then A86: CurInstr (P,(Comput (P,s,n))) = P . n by A81, A82, PBOOLE:143, XXREAL_0:2
.= SubFrom (a,(intloc 0)) by A74, A83, A85 ;
Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((SubFrom (a,(intloc 0))),(Comput (P,s,n))) by A86 ;
hence IC (Comput (P,s,(n + 1))) = n + 1 by A81, A82, NAT_1:13, SCMFSA_2:65; :: thesis: verum
end;
end;
end;
A87: S2[ 0 ] by A2, EXTPRO_1:2;
for i being Nat holds S2[i] from NAT_1:sch 2(A87, A80);
 hence IC (Comput (P,s,i)) = i by A79; :: thesis: verum
end;
A88: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A89: S1[n] ; :: thesis: S1[n + 1]
assume A90: n + 1 <= (mk + 1) + 1 ; :: thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
per cases ( n = 0 or n > 0 ) ;
suppose A91: n = 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1
thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A66, A91
.= ((- (n + 1)) + 1) + 1 by A1, A91, SCMFSA_2:63 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f
let b be Int-Location; :: thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b )
assume A92: b <> a ; :: thesis: (Comput (P,s,(n + 1))) . b = s . b
thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A66, A91
.= s . b by A92, SCMFSA_2:63 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput (P,s,(n + 1))) . f = s . f
thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A66, A91
.= s . f by SCMFSA_2:63 ; :: thesis: verum
end;
suppose A93: n > 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
A94: n < (mk + 1) + 1 by A90, NAT_1:13;
A95: P /. (IC (Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by PBOOLE:143;
A96: n + 0 <= n + 1 by XREAL_1:7;
then A97: CurInstr (P,(Comput (P,s,n))) = P . n by A78, A90, A95, XXREAL_0:2
.= SubFrom (a,(intloc 0)) by A74, A93, A94 ;
A98: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((SubFrom (a,(intloc 0))),(Comput (P,s,n))) by A97 ;
A99: 0 + 1 < n + 1 by A93, XREAL_1:6;
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1
thus (Comput (P,s,(n + 1))) . a = (((- n) + 1) + 1) - ((Comput (P,s,n)) . (intloc 0)) by A89, A90, A99, A98, NAT_1:13, SCMFSA_2:65
.= (((- n) + 1) + 1) - (s . (intloc 0)) by A4, A89, A90, A96, XXREAL_0:2
.= ((- (n + 1)) + 1) + 1 by A1 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f
let b be Int-Location; :: thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b )
assume A100: b <> a ; :: thesis: (Comput (P,s,(n + 1))) . b = s . b
hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A98, SCMFSA_2:65
.= s . b by A89, A90, A96, A100, XXREAL_0:2 ;
:: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput (P,s,(n + 1))) . f = s . f
thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A98, SCMFSA_2:65
.= s . f by A89, A90, A96, XXREAL_0:2 ; :: thesis: verum
end;
end;
end;
A101: len (Stop SCM+FSA) = 1 by AFINSQ_1:34;
( len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) <= (mk + 1) + 1 & (mk + 1) + 1 < (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))))) + (len (Stop SCM+FSA)) implies ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . ((mk + 1) + 1) = (Stop SCM+FSA) . (((mk + 1) + 1) - (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))))) ) by AFINSQ_1:18;
then A102: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ (Stop SCM+FSA)) . ((mk + 1) + 1) = halt SCM+FSA by A59, XREAL_1:29, A101;
A103: P /. (IC (Comput (P,s,((mk + 1) + 1)))) = P . (IC (Comput (P,s,((mk + 1) + 1)))) by PBOOLE:143;
A104: CurInstr (P,(Comput (P,s,((mk + 1) + 1)))) = P . ((mk + 1) + 1) by A78, A103
.= halt SCM+FSA by A102, A64 ;
hence P halts_on s by EXTPRO_1:29; :: thesis: ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )
then A105: Comput (P,s,((mk + 1) + 1)) = Result (P,s) by A104, EXTPRO_1:def 9;
A106: S1[ 0 ] by EXTPRO_1:2;
A107: for i being Nat holds S1[i] from NAT_1:sch 2(A106, A88);
 ( ((- ((mk + 1) + 1)) + 1) + 1 = k & 0 + 1 <= mk + (1 + 1) ) by XREAL_1:7;
hence ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) by A107, A105; :: thesis: verum
end;
end;