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