:: Some Multi-instructions defined by sequence of instructions of SCM+FSA
:: by Noriko Asamoto
::
:: Received April 24, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FINSEQ_1, ARYTM_3, ORDINAL4, ARYTM_1, AMI_1,
SCMFSA_2, RELAT_1, FUNCT_1, PARTFUN1, TARSKI, XXREAL_0, NAT_1, CARD_1,
XBOOLE_0, INT_1, GRAPHSP, FINSEQ_2, AMI_3, PRE_POLY, FSM_1, CIRCUIT2,
MSUALG_1, COMPLEX1, FUNCT_4, SCMFSA_7, EXTPRO_1, AFINSQ_1, FUNCOP_1,
PBOOLE, FINSET_1, AMISTD_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0,
NAT_1, INT_2, NAT_D, INT_1, RELAT_1, PARTFUN1, FINSET_1, FINSEQ_1,
AFINSQ_1, FINSEQ_2, FUNCT_1, FUNCOP_1, FUNCT_7, PBOOLE, XXREAL_0,
MEMSTR_0, COMPOS_1, EXTPRO_1, SCMFSA_2, AFINSQ_2;
constructors REAL_1, AMI_3, SCMFSA_2, NAT_D, RELSET_1, PRE_POLY, AFINSQ_2,
FUNCT_7;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1,
FINSEQ_1, FUNCT_7, SCMFSA_2, FINSEQ_2, AFINSQ_1, FUNCOP_1, MEMSTR_0,
PBOOLE, AMI_3, COMPOS_0, COMPOS_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities EXTPRO_1, FINSEQ_1, SCMFSA_2, AFINSQ_1, FUNCOP_1, MEMSTR_0,
ORDINAL1, COMPOS_1;
theorems FUNCT_1, SCMFSA_2, INT_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
RELAT_1, CARD_1, TARSKI, GRFUNC_1, ABSVALUE, FUNCT_7, XBOOLE_1, XREAL_1,
XXREAL_0, FUNCOP_1, AMI_3, AFINSQ_1, AFINSQ_2, EXTPRO_1, PBOOLE,
MEMSTR_0;
schemes NAT_1, STIRL2_1, AFINSQ_1;
begin
reserve m for Nat;
reserve P for (the InstructionsF of SCM+FSA)-valued ManySortedSet of NAT;
Lm1: for p1,p2,p3,p4 being XFinSequence
holds p1 ^ p2 ^ p3 ^ p4 = p1 ^ p2 ^ (p3
^ p4) & p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3 ^ p4) & p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2
^ (p3 ^ p4)) & p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3) ^ p4
proof
let p1,p2,p3,p4 be XFinSequence;
thus p1 ^ p2 ^ p3 ^ p4 = p1 ^ p2 ^ (p3 ^ p4) by AFINSQ_1:27;
thus p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ p3) ^ p4 by AFINSQ_1:27
.= p1 ^ (p2 ^ p3 ^ p4) by AFINSQ_1:27;
hence p1 ^ p2 ^ p3 ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) by AFINSQ_1:27;
thus thesis by AFINSQ_1:27;
end;
Lm2: for p1,p2,p3,p4,p5 being XFinSequence
holds p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^
p2 ^ p3 ^ (p4 ^ p5) & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ (p3 ^ p4 ^ p5) & p1 ^
p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ (p3 ^ (p4 ^ p5)) & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^
(p2 ^ p3 ^ p4 ^ p5) & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ p3 ^ (p4 ^ p5)) & p1
^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ (p3 ^ p4 ^ p5)) & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1
^ (p2 ^ (p3 ^ (p4 ^ p5))) & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ (p3 ^ p4) ^ p5 &
p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ p3 ^ p4) ^ p5 & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1
^ (p2 ^ (p3 ^ p4)) ^ p5 & p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ (p3 ^ p4) ^ p5)
proof
let p1,p2,p3,p4,p5 be XFinSequence;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ p3 ^ (p4 ^ p5) by AFINSQ_1:27;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ (p3 ^ p4 ^ p5) by Lm1;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ (p3 ^ (p4 ^ p5)) by Lm1;
thus
A1: p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ p3 ^ p4) ^ p5 by Lm1
.= p1 ^ (p2 ^ p3 ^ p4 ^ p5) by AFINSQ_1:27;
hence p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ p3 ^ (p4 ^ p5)) by AFINSQ_1:27;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ (p3 ^ p4 ^ p5)) by A1,Lm1;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) by A1,Lm1;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ p2 ^ (p3 ^ p4) ^ p5 by Lm1;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ p3 ^ p4) ^ p5 by Lm1;
thus p1 ^ p2 ^ p3 ^ p4 ^ p5 = p1 ^ (p2 ^ (p3 ^ p4)) ^ p5 by Lm1;
thus thesis by A1,Lm1;
end;
deffunc U(Nat) = $1-'1;
definition
let a be Int-Location;
let k be Integer;
func a := k -> (the InstructionsF of SCM+FSA)-valued NAT-defined
finite Function
means
:Def1:
ex k1 being Nat st
k1 + 1 = k & it = <% a:= intloc 0 %> ^ ( k1 --> AddTo(a,intloc 0) )
^ Stop SCM+FSA if k > 0
otherwise ex k1 being Nat st k1 + k
= 1 & it = <% a:= intloc 0 %> ^ ( k1 --> SubFrom(a,intloc 0) ) ^
Stop SCM+FSA;
existence
proof
thus k > 0 implies
ex f being (the InstructionsF of SCM+FSA)-valued NAT-defined
finite Function
st
ex k1 being Nat st k1 + 1 = k &
f = <% a:= intloc 0 %> ^ ( k1 --> AddTo(a,intloc 0) ) ^ Stop SCM+FSA
proof
assume k > 0;
then 0 + 1 <= k by INT_1:7;
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
set xx = <% a:= intloc 0 %> ^ ( k1 --> AddTo(a,intloc 0) ) ^ Stop
SCM+FSA;
reconsider xx as (the InstructionsF of SCM+FSA)-valued NAT-defined
finite Function;
take xx,k1;
thus k1 + 1 = k;
thus thesis;
end;
assume k <= 0;
then reconsider k1 = 1 - k as Element of NAT by INT_1:5;
set xx = <% a:= intloc 0 %> ^ ( k1 --> SubFrom(a,intloc 0) ) ^ Stop
SCM+FSA;
reconsider xx as (the InstructionsF of SCM+FSA)-valued NAT-defined
finite Function;
take xx,k1;
thus k1 + k = 1;
thus thesis;
end;
uniqueness;
correctness;
end;
definition
let a be Int-Location;
let k be Integer;
func aSeq(a,k) -> XFinSequence of the InstructionsF of SCM+FSA means
:Def2:
ex k1 being Nat st k1 + 1 = k &
it = <% a:= intloc 0 %> ^ (k1 --> AddTo (a,intloc 0)) if k > 0
otherwise ex k1 being Nat st k1 + k = 1 & it
= <% a:= intloc 0 %> ^ (k1 --> SubFrom(a,intloc 0));
existence
proof
thus k > 0 implies
ex s being XFinSequence of the InstructionsF of SCM+FSA,
k1 being Nat
st k1 + 1 = k & s = <% a:= intloc 0 %> ^ ( k1 -->
AddTo(a,intloc 0))
proof
assume k > 0;
then 0 + 1 <= k by INT_1:7;
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
take <% a:= intloc 0 %> ^ ( k1 --> AddTo(a,intloc 0)),k1;
thus k1 + 1 = k;
thus thesis;
end;
assume k <= 0;
then reconsider k1 = 1 - k as Element of NAT by INT_1:5;
take <% a:= intloc 0 %> ^ ( k1 --> SubFrom(a,intloc 0) ), k1;
thus k1 + k = 1;
thus thesis;
end;
uniqueness;
correctness;
end;
theorem
for a being Int-Location, k being Integer holds a:=k = aSeq(a,k)
^ Stop SCM+FSA
proof
let a be Int-Location, k be Integer;
per cases;
suppose
k > 0;
then
ex k1 being Nat st k1 + 1 = k & a:=k = <% a:=intloc 0
%> ^ (k1-->AddTo(a,intloc 0)) ^ Stop SCM+FSA by Def1;
hence thesis by Def2;
end;
suppose
A1: k <= 0;
then
ex k1 being Nat st k1 + k = 1 & a:=k = <% a:=intloc 0
%> ^ (k1-->SubFrom(a,intloc 0)) ^ Stop SCM+FSA by Def1;
hence thesis by A1,Def2;
end;
end;
definition
let f be FinSeq-Location;
let p be FinSequence of INT;
func aSeq(f,p) -> XFinSequence of the InstructionsF of SCM+FSA means
:Def3:
ex pp being XFinSequence of (the InstructionsF of SCM+FSA)^omega
st len pp = len p &
(for k being Nat st k < len pp
ex i being Integer st i = p.(k+1) &
pp.k = (aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^
<% (f,intloc 1):=intloc 2 %>))
& it = FlattenSeq pp;
existence
proof
defpred P[Integer,set] means ex i being Integer
st (i = p.($1+1) & $2 = (aSeq(intloc 1,$1+1) ^ aSeq(intloc 2,i) ^
<% (f,intloc 1):=intloc 2 %>));
set D = (the InstructionsF of SCM+FSA)^omega;
A1: for k being Nat st k in Segm len p ex d being Element of D st P[k,d]
proof
let k be Nat;
assume k in Segm len p;
then k < len p by NAT_1:44;
then 1 <= k+1 & k+1 <= len p by NAT_1:12,13;
then k+1 in dom p by FINSEQ_3:25;
then p.(k+1) in INT by FINSEQ_2:11;
then reconsider i = p.(k+1) as Integer;
reconsider d = aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^
<% (f,intloc 1):=intloc 2 %> as Element of D by AFINSQ_1:def 7;
take d;
thus thesis;
end;
consider pp being XFinSequence of D such that
A2: dom pp = Segm len p and
A3: for k being Nat st
k in Segm len p holds P[k,pp.k] from STIRL2_1:sch 5(A1);
reconsider tt = FlattenSeq pp as
XFinSequence of the InstructionsF of SCM+FSA by AFINSQ_1:def 7;
take tt,pp;
thus len pp = len p by A2;
thus for k be Nat st k < len pp
ex i being Integer st i = p.(k+1) &
(aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^ <% (f,intloc 1):=intloc 2 %>
) = pp.k by A2,A3,NAT_1:44;
thus thesis;
end;
uniqueness
proof
reconsider i = len p as Nat;
let s1,s2 be XFinSequence of the InstructionsF of SCM+FSA such that
A4: ex pp being XFinSequence of (the InstructionsF of SCM+FSA)^omega st len
pp = len p & (for k being Nat st k < len pp
ex i being Integer st i = p.(k+1) &
pp.k = (aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^ <% (f,
intloc 1):=intloc 2 %>)) & s1 = FlattenSeq pp and
A5: ex pp being XFinSequence of (the InstructionsF of SCM+FSA)^omega st len
pp = len p & (for k being Nat st k < len pp
ex i being Integer st i = p.(k+1) &
pp.k = (aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^ <% (f,
intloc 1):=intloc 2 %>)) & s2 = FlattenSeq pp;
consider pp1 being XFinSequence of (the InstructionsF of SCM+FSA)^omega
such that
A6: len pp1 = len p and
A7: for k being Nat st k < len pp1
ex i being Integer st i = p.(k+1) &
pp1.k = (aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^ <% (f
,intloc 1):=intloc 2 %>) and
A8: s1 = FlattenSeq pp1 by A4;
consider pp2 being XFinSequence of (the InstructionsF of SCM+FSA)^omega
such that
A9: len pp2 = len p and
A10: for k being Nat st k < len pp2 holds
ex i being Integer st i = p.(k+1) &
pp2.k = (aSeq(intloc 1,k+1) ^ aSeq(intloc 2,i) ^ <% (f
,intloc 1):=intloc 2 %>) and
A11: s2 = FlattenSeq pp2 by A5;
for k being Nat st k < len pp1 holds pp1.k = pp2.k
proof
let k be Nat;
assume
A12: k < len pp1;
(ex i1 being Integer st i1 = p.(k+1) &
pp1.k = (aSeq(intloc 1, k+1) ^ aSeq(intloc 2,i1) ^
<% (f,intloc 1):= intloc 2 %>) )&
ex i2 being Integer st i2
= p.(k+1) & pp2.k = (aSeq(intloc 1, k+1) ^ aSeq(intloc 2,i2) ^
<% (f,intloc 1):=
intloc 2 %>) by A7,A10,A12,A6,A9;
hence pp1.k = pp2.k;
end;
hence thesis by A8,A11,A6,A9,AFINSQ_1:9;
end;
correctness;
end;
definition
let f be FinSeq-Location;
let p be FinSequence of INT;
func f := p -> (the InstructionsF of SCM+FSA)-valued NAT-defined
finite Function equals
aSeq(intloc 1,len p) ^ <% f:=<0,...,0>intloc 1 %> ^
aSeq(f,p) ^ Stop SCM+FSA;
correctness;
end;
theorem
for a being Int-Location holds a:=1 = <% a:= intloc 0 %> ^ Stop SCM+FSA
proof
let a be Int-Location;
A1: 0 + 1 = 1;
<% a:= intloc 0 %> ^ Stop SCM+FSA
= <% a:= intloc 0 %> ^ {} ^ Stop SCM+FSA
.= <% a:= intloc 0 %> ^ ( 0 --> AddTo(a,intloc 0) ) ^ Stop SCM+FSA;
hence thesis by Def1,A1;
end;
theorem
for a being Int-Location holds a:=0 = <% a:= intloc 0 %>^<%
SubFrom(a,intloc 0)%>^Stop SCM+FSA
proof
let a be Int-Location;
1 + 0 = 1 & <% a:= intloc 0 %>^<%
SubFrom(a,intloc 0)%>^Stop SCM+FSA
= <% a:= intloc 0 %> ^ ( 1 --> SubFrom(a,intloc 0) ) ^
Stop SCM+FSA by CARD_1:49;
hence thesis by Def1;
end;
theorem Th4:
for c0 being Nat
for s being c0-started State of SCM+FSA st s.intloc 0 = 1
for a being Int-Location, k being Integer st a <> intloc 0 &
(for c being Nat st c in dom aSeq(a,k)
holds aSeq(a,k).c = P.(c0 + c))
holds
(for i being Nat st i <= len aSeq(a,k)
holds IC Comput(P,s,i) = c0 + i &
(for b being Int-Location st b <> a
holds Comput(P,s,i).b = s.b) &
(for f being FinSeq-Location holds Comput(P,s,i).f = s.f)) &
Comput(P,s,len aSeq(a,k)).a = k
proof
let c0 be Nat;
let s be c0-started State of SCM+FSA;
assume
A1: s.intloc 0 = 1;
A2: IC s = c0 by MEMSTR_0:def 11;
let a be Int-Location;
let k be Integer;
assume that
A3: a <> intloc 0 and
A4: for c being Nat st c in dom aSeq(a,k)
holds aSeq(a,k).c = P.(c0 + c);
per cases;
suppose
A5: k > 0;
then reconsider k9= k as Element of NAT by INT_1:3;
consider k1 being Nat such that
A6: k1 + 1 = k9 and
A7: aSeq(a,k9) = <%a:=intloc 0%> ^ (k1 --> AddTo(a,intloc 0)) by A5,Def2;
defpred Q[Nat] means $1 <= k9 implies IC Comput(P,s,$1) =
(c0 + $1) & (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);
A8: len aSeq(a,k9) = len <%a:=intloc 0%> + len (k1-->AddTo(a,intloc 0))
by A7,AFINSQ_1:17
.= 1 + len(k1-->AddTo(a,intloc 0)) by AFINSQ_1:33
.= k9 by A6;
A9: for i being Nat st i <= len aSeq(a,k9)
holds IC Comput(P,s,i) = (c0 + i) &
(1 <= i implies Comput(P,s,i).a = i) &
(for b being Int-Location st b <> a
holds Comput(P,s,i).b = s.b) &
for f being
FinSeq-Location holds Comput(P,s,i).f = s.f
proof
A10: for i being Nat st i < k9 holds i in dom aSeq(a,k9)
by A8,AFINSQ_1:86;
A11: P.(c0 + 0) = aSeq(a,k9).0 by A5,A4,A10
.= a:= intloc 0 by A7,AFINSQ_1:35;
A12: now
let n be Nat;
assume n = 0;
hence
A13: Comput(P,s,n) = s by EXTPRO_1:2;
hence CurInstr(P,Comput(P,s,n)) =
a:= intloc 0 by A2,A11,PBOOLE:143;
thus Comput(P,s,n+1) = Following(P,
Comput(P,s,n)) by EXTPRO_1:3
.= Exec(a:= intloc 0,s) by A2,A11,A13,PBOOLE:143;
end;
A14: now
let i be Nat;
assume that
A15: 1 <= i and
A16: i < k9;
reconsider i1 = i - 1 as Element of NAT by A15,INT_1:5;
i = i1 + 1;
then
i1 < k1 by A16,A6,XREAL_1:6;
then
A17: i1 in Segm k1 by NAT_1:44;
A18: len (k1 --> AddTo(a,intloc 0)) = k1;
len <% a:= intloc 0 %> = 1 by AFINSQ_1:33;
hence aSeq(a,k9).i = (k1 --> AddTo(a,intloc 0)).(i - 1)
by A15,A7,A18,A6,A16,AFINSQ_1:18
.= AddTo(a,intloc 0) by A17,FUNCOP_1:7;
end;
A19: now
let i be Nat;
assume that
A20: 0 < i and
A21: i < k9;
A22: 0+1 <= i by A20,NAT_1:13;
thus P. (c0 + i) = aSeq(a,k9).(i) by A4,A10,A21
.=AddTo(a,intloc 0) by A14,A22,A21;
end;
A23: for n being Nat st Q[n] holds Q[n + 1]
proof
let n be Nat;
assume
A24: Q[n];
assume
A25: n + 1 <= k9;
per cases;
suppose
A26: n = 0;
hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A12
.= c0 + (n + 1) by A2,A26,SCMFSA_2:63;
hereby
assume 1 <= n + 1;
thus Comput(P,s,n+1).a = Exec(a:= intloc 0,s).a by A12,A26
.= n + 1 by A1,A26,SCMFSA_2:63;
end;
hereby
let b be Int-Location;
assume
A27: b <> a;
thus Comput(P,s,n+1).b = Exec(a:= intloc 0,s).b by A12,A26
.= s.b by A27,SCMFSA_2:63;
end;
let f be FinSeq-Location;
thus Comput(P,s,n+1).f = Exec(a:= intloc 0,s).f by A12,A26
.= s.f by SCMFSA_2:63;
end;
suppose
A28: n > 0;
A29: n < k9 by A25,NAT_1:13;
A30: n + 0 <= n + 1 by XREAL_1:7;
then
A31: CurInstr(P,Comput(P,s,n)) =
P. (c0 + n) by A24,A25,PBOOLE:143,XXREAL_0:2
.= AddTo(a,intloc 0) by A19,A28,A29;
A32: 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 A31;
hence IC Comput(P,s,n+1) = IC Comput(P,s,n)+1 by SCMFSA_2:64
.= c0 + (n + 1) by A24,A25,A30,XXREAL_0:2;
A33: 0 + 1 <= n by A28,INT_1:7;
hereby
assume 1 <= n + 1;
thus Comput(P,s,n+1).a = n + Comput(P,s,n
).intloc 0 by A24,A25,A33,A30,A32,SCMFSA_2:64,XXREAL_0:2
.= n + 1 by A1,A3,A24,A25,A30,XXREAL_0:2;
end;
hereby
let b be Int-Location;
assume
A34: b <> a;
hence Comput(P,s,n+1).b = Comput(P,s,n).b
by A32,SCMFSA_2:64
.= s.b by A24,A25,A30,A34,XXREAL_0:2;
end;
let f be FinSeq-Location;
thus ( Comput(P,s,n+1)).f = Comput(P,s,n).f
by A32,SCMFSA_2:64
.= s.f by A24,A25,A30,XXREAL_0:2;
end;
end;
A35: Q[0] by A2,EXTPRO_1:2;
A36: for i being Nat holds Q[i] from NAT_1:sch 2(A35,A23);
let i be Nat;
assume i <= len aSeq(a,k9);
hence thesis by A8,A36;
end;
hence
for i being Nat st i <= len aSeq(a,k) holds IC Comput(
P,s,i) = (c0 + i) & (for b being Int-Location st b <> a holds
Comput(P,s,i).b = s.b) & for f being FinSeq-Location holds Comput(
P,s,i).f = s.f;
1 <= len aSeq(a,k) by A6,A8,NAT_1:11;
hence thesis by A8,A9;
end;
suppose
A37: k <= 0;
then reconsider mk = - k as Element of NAT by INT_1:3;
defpred Q[Nat] means $1 <= mk+1+1 implies IC Comput(P,s,$1)
= (c0 + $1) & (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
A38: k1 + k = 1 and
A39: aSeq(a,k) = <%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) by A37,Def2;
A40: len aSeq(a,k) = len <% a:=intloc 0 %> + len (k1-->SubFrom(a,intloc 0)
) by A39,AFINSQ_1:17
.= 1 + len (k1-->SubFrom(a,intloc 0)) by AFINSQ_1:33
.= mk+1+1 by A38;
A41: for i being Nat st i <= len aSeq(a,k) holds IC Comput(
P,s,i) = (c0 + i) & (1 <= i implies Comput(P,s,i).a
= -i+1+1) & (for b
being Int-Location st b <> a holds Comput(P,s,i).b = s.b) &
for f being
FinSeq-Location holds Comput(P,s,i).f = s.f
proof
A42: for i being Nat st i < mk+1+1 holds i in dom aSeq(a,k)
by A40,AFINSQ_1:86;
A43: P.(c0 + 0) = aSeq(a,k).0 by A4,A42
.= a:= intloc 0 by A39,AFINSQ_1:35;
A44: 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)
proof
let n be Nat;
assume n = 0;
hence
A45: Comput(P,s,n) = s by EXTPRO_1:2;
hence CurInstr(P,Comput(P,s,n))
= a:= intloc 0 by A2,A43,PBOOLE:143;
thus Comput(P,s,n+1) = Following(P,
Comput(P,s,n)) by EXTPRO_1:3
.= Exec(a:= intloc 0,s) by A2,A43,A45,PBOOLE:143;
end;
A46: now
let i be Nat;
assume that
A47: 1 <= i and
A48: i < mk+1+1;
A49: i - 1 < mk+1+1 - 1 by A48,XREAL_1:9;
reconsider i1 = i - 1 as Element of NAT by A47,INT_1:5;
A50: i1 in Segm k1 by A38,A49,NAT_1:44;
A51: len(k1 --> SubFrom(a,intloc 0)) = k1;
len <% a:= intloc 0 %> = 1 by AFINSQ_1:33;
hence aSeq(a,k).i = (k1-->SubFrom(a,intloc 0)).(i - 1)
by A39,A47,A51,A38,A48,AFINSQ_1:18
.= SubFrom(a,intloc 0) by A50,FUNCOP_1:7;
end;
A52: now
let i be Nat;
assume that
A53: 0 < i and
A54: i < mk+1+1;
A55: 0+1 <= i by A53,NAT_1:13;
thus P. (c0 + i) = aSeq(a,k).(i) by A4,A42,A54
.=SubFrom(a,intloc 0) by A46,A55,A54;
end;
A56: for n being Nat st Q[n] holds Q[n + 1]
proof
let n be Nat;
assume
A57: Q[n];
assume
A58: n + 1 <= mk+1+1;
per cases;
suppose
A59: n = 0;
hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A44
.= c0 + (n + 1) by A2,A59,SCMFSA_2:63;
hereby
assume 1 <= n + 1;
thus Comput(P,s,n+1).a = Exec(a:= intloc 0,s).a by A44,A59
.= -(n + 1)+1+1 by A1,A59,SCMFSA_2:63;
end;
hereby
let b be Int-Location;
assume
A60: b <> a;
thus Comput(P,s,n+1).b = Exec(a:= intloc 0,s).b by A44,A59
.= s.b by A60,SCMFSA_2:63;
end;
let f be FinSeq-Location;
thus Comput(P,s,n+1).f = Exec(a:= intloc 0,s).f by A44,A59
.= s.f by SCMFSA_2:63;
end;
suppose
A61: n > 0;
A62: n < mk+1+1 by A58,NAT_1:13;
A63: n + 0 <= n + 1 by XREAL_1:7;
then
A64: CurInstr(P,Comput(P
,s,n))
= P. (c0 + n) by A57,A58,PBOOLE:143,XXREAL_0:2
.= SubFrom(a,intloc 0) by A52,A61,A62;
A65: 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 A64;
hence IC Comput(P,s,n+1) = IC Comput(P
,s,n)+1 by SCMFSA_2:65
.= c0 + (n + 1) by A57,A58,A63,XXREAL_0:2;
A66: 0 + 1 < n + 1 by A61,XREAL_1:6;
hereby
assume 1 <= n + 1;
thus Comput(P,s,n+1).a
= -n+1+1 - Comput(P,s,n).intloc 0
by A57,A58,A66,A65,NAT_1:13,SCMFSA_2:65
.= -n+1+1 - s.intloc 0 by A3,A57,A58,A63,XXREAL_0:2
.= -(n+1)+1+1 by A1;
end;
hereby
let b be Int-Location;
assume
A67: b <> a;
hence Comput(P,s,n+1).b = Comput(P,s,n).b
by A65,SCMFSA_2:65
.= s.b by A57,A58,A63,A67,XXREAL_0:2;
end;
let f be FinSeq-Location;
thus ( Comput(P,s,n+1)).f = Comput(P,s,n).f
by A65,SCMFSA_2:65
.= s.f by A57,A58,A63,XXREAL_0:2;
end;
end;
A68: Q[0] by A2,EXTPRO_1:2;
A69: for i being Nat holds Q[i] from NAT_1:sch 2(A68,A56);
let i be Nat;
assume i <= len aSeq(a,k);
hence thesis by A40,A69;
end;
hence
for i being Nat st i <= len aSeq(a,k) holds IC Comput(
P,s,i) = (c0 + i) & (for b being Int-Location st b <> a holds
Comput(P,s,i).b = s.b) & for f being FinSeq-Location holds Comput(
P,s,i).f = s.f;
1 <= len aSeq(a,k) by A40,NAT_1:11;
hence Comput(P,s,len aSeq(a,k)).a = -(-k+(1+1))+1+1 by A40,A41
.= k;
end;
end;
theorem Th5:
for s being 0-started State of SCM+FSA st s.intloc 0 = 1
for a being Int-Location
for k being Integer st aSeq(a,k) c= P & a<>intloc 0
holds
(for i being Nat st i <= len aSeq(a,k)
holds IC Comput(P,s,i) = i &
(for b being Int-Location st b <> a
holds Comput(P,s,i).b = s.b) &
(for f being FinSeq-Location holds Comput(P,s,i).f = s.f)) &
Comput(P,s,len aSeq(a,k)).a = k
proof
let s be 0-started State of SCM+FSA;
assume
A1: s.intloc 0 = 1;
let a be Int-Location;
let k be Integer;
assume that
A2: aSeq(a,k) c= P and
A3: a <> intloc 0;
A4: for c being Nat st c in dom aSeq(a,k)
holds aSeq(a,k).c = P.(0 + c) by A2,GRFUNC_1:2;
hereby
let i be Nat;
assume
A5: i <= len aSeq(a,k);
then IC Comput(P,s,i) = (0 + i) by A1,A3,A4,Th4;
hence IC Comput(P,s,i) = i & (for b being Int-Location st b
<> a
holds Comput(P,s,i).b = s.b) & for f being FinSeq-Location holds
Comput(P,s,i).f = s.f by A1,A3,A4,A5,Th4;
end;
thus thesis by A1,A3,A4,Th4;
end;
:: Users' guide
theorem
for s being 0-started State of SCM+FSA st s.intloc 0 = 1 for a
being Int-Location, 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
proof
let s be 0-started State of SCM+FSA;
assume that
A1: s.intloc 0 = 1;
A2: IC s = 0 by MEMSTR_0:def 11;
let a be Int-Location, k be Integer;
assume that
A3: a:=k c= P and
A4: a <> intloc 0;
per cases;
suppose
A5: k > 0;
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 as Element of NAT by A5,INT_1:3;
defpred Q[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: f.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 f = 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
let i be Nat;
assume that
A12: i <= k;
i < len f by A12,NAT_1:13,A10;
hence i in dom f by AFINSQ_1:86;
end;
A13: for i being Nat st i <= k holds P. i = ( f). i by A3,A7,A11,GRFUNC_1:2;
then
A14: P.0 = a:= intloc 0 by A9;
A15: now
let n be Nat;
assume n = 0;
hence
A16: Comput(P,s,n) = s by EXTPRO_1:2;
hence CurInstr(P,Comput(P,s,n))
= a:= intloc 0 by A2,A14,PBOOLE:143;
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;
end;
A17: now
let i be Nat;
assume that
A18: 1 <= i and
A19: i < k;
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 f.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;
end;
A23: now
let i be Nat;
assume that
A24: 0 < i and
A25: i < k;
A26: 0+1 <= i by A24,NAT_1:13;
thus P. i = f.(i) by A13,A25
.=AddTo(a,intloc 0) by A17,A26,A25;
end;
A27: for i being Nat st i <= k holds IC Comput(P,s,i) =
i
proof
defpred P[Nat] means $1 <= k implies IC Comput(P,s,$1) =
$1;
let i be Nat;
assume
A28: i <= k;
A29: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume
A30: P[n];
assume
A31: n+1 <= k;
then
A32: n < k by NAT_1:13;
per cases;
suppose
A33: n=0;
hence IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC
SCM+FSA by A15
.= n+1 by A2,A33,SCMFSA_2:63;
end;
suppose
A34: n>0;
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;
end;
end;
A36: P[0] by A2,EXTPRO_1:2;
for i being Nat holds P[i] from NAT_1:sch 2(A36,A29);
hence thesis by A28;
end;
A37: for n being Nat st Q[n] holds Q[n + 1]
proof
let n be Nat;
assume
A38: Q[n];
assume
A39: n + 1 <= k;
per cases;
suppose
A40: n = 0;
hereby
assume 1 <= 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;
end;
hereby
let b be Int-Location;
assume
A41: b <> a;
thus Comput(P,s,n+1).b = Exec(a:= intloc 0,s).b by A15,A40
.= s.b by A41,SCMFSA_2:63;
end;
let f be FinSeq-Location;
thus Comput(P,s,n+1).f = Exec(a:= intloc 0,s).f by A15,A40
.= s.f by SCMFSA_2:63;
end;
suppose
A42: n > 0;
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
assume 1 <= 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;
end;
hereby
let b be Int-Location;
assume
A49: b <> a;
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;
end;
let f be FinSeq-Location;
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;
end;
end;
len Stop SCM+FSA = 1 by AFINSQ_1:34;
then k < k + len Stop SCM+FSA by XREAL_1:29;
then
A50: f.(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: Q[0] by EXTPRO_1:2;
A53: for i being Nat holds Q[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;
then Comput(P,s,k) = Result(P,s)
by A55,EXTPRO_1:def 9;
hence thesis by A53,A51;
end;
suppose
A56: k <= 0;
then reconsider mk = - k as Element of NAT by INT_1:3;
defpred Q[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: f.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 f = 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
let i be Nat;
assume that
A63: i <= mk+1+1;
i < mk+1+1+1 by A63,NAT_1:13;
hence i in dom f by A61,AFINSQ_1:86;
end;
A64: for i being Nat st i <= mk+1+1 holds P.i = f.i by A3,A58,GRFUNC_1:2,A62;
then
A65: P.0 = a:= intloc 0 by A60;
A66: now
let n be Nat;
assume n = 0;
hence
A67: Comput(P,s,n) = s by EXTPRO_1:2;
hence CurInstr(P,Comput(P,s,n))
= a:= intloc 0 by A2,A65,PBOOLE:143;
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;
end;
A68: now
A69: len <%a:= intloc 0%> = 1 by AFINSQ_1:33;
let i be Nat;
assume that
A70: 1 <= i and
A71: i < mk+1+1;
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 f.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;
end;
A74: now
let i be Nat;
assume that
A75: 0 < i and
A76: i < mk+1+1;
A77: 0+1 <= i by A75,NAT_1:13;
thus P. i = f.(i) by A64,A76
.=SubFrom(a,intloc 0) by A68,A77,A76;
end;
A78: for i being Nat st i <= mk+1+1 holds IC Comput(P,s
,i)
= i
proof
defpred P[Nat] means $1<=mk+1+1 implies IC Comput(P,s,$1)=
$1;
let i be Nat;
assume
A79: i <= mk+1+1;
A80: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume
A81: P[n];
assume
A82: n+1 <= mk+1+1;
then
A83: n < mk+1+1 by NAT_1:13;
per cases;
suppose
A84: n=0;
hence
IC Comput(P,s,n+1) = Exec(a:= intloc 0,s).IC SCM+FSA by A66
.= n+1 by A2,A84,SCMFSA_2:63;
end;
suppose
A85: n>0;
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;
end;
end;
A87: P[0] by A2,EXTPRO_1:2;
for i being Nat holds P[i] from NAT_1:sch 2(A87,A80);
hence thesis by A79;
end;
A88: for n being Nat st Q[n] holds Q[n + 1]
proof
let n be Nat;
assume
A89: Q[n];
assume
A90: n + 1 <= mk+1+1;
per cases;
suppose
A91: n = 0;
hereby
assume 1 <= n + 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;
end;
hereby
let b be Int-Location;
assume
A92: b <> a;
thus Comput(P,s,n+1).b = Exec(a:= intloc 0,s).b by A66,A91
.= s.b by A92,SCMFSA_2:63;
end;
let f be FinSeq-Location;
thus Comput(P,s,n+1).f = Exec(a:= intloc 0,s).f by A66,A91
.= s.f by SCMFSA_2:63;
end;
suppose
A93: n > 0;
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
assume 1 <= n + 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;
end;
hereby
let b be Int-Location;
assume
A100: b <> a;
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;
end;
let f be FinSeq-Location;
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;
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
f.(mk+1+1)=(Stop SCM+FSA).(mk+1+1-
len (<%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0))))
by AFINSQ_1:18;
then
A102: f.(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;
then
A105: Comput(P,s,mk+1+1) = Result(P,s) by A104,EXTPRO_1:def 9;
A106: Q[0] by EXTPRO_1:2;
A107: for i being Nat holds Q[i] from NAT_1:sch 2(A106,A88);
-(mk+1+1)+1+1 = k & 0 + 1 <= mk+(1+1) by XREAL_1:7;
hence thesis by A107,A105;
end;
end;
theorem
for s being 0-started State of SCM+FSA st s.intloc 0 = 1 for f
being FinSeq-Location, p being FinSequence of INT st f:=p c= P
holds P halts_on s &
(Result(P,s)).f = p &
(for b being Int-Location st b <> intloc 1 & b <> intloc 2
holds (Result(P,s)).b = s.b) &
for g being FinSeq-Location st g <> f
holds (Result(P,s)).g = s.g
proof
set D = the InstructionsF of SCM+FSA;
set V = intloc 2;
set I = intloc 1;
set O = intloc 0;
A1: I <> O by AMI_3:10;
A2: I <> V by AMI_3:10;
let s be 0-started State of SCM+FSA such that
A3: s.O = 1;
let f be FinSeq-Location, p be FinSequence of INT such that
A4: f:=p c= P;
set q = aSeq(I,len p)^<% f:=<0,...,0>I %>^aSeq(f,p)^Stop SCM+FSA;
A5: for i,k being Nat st i < len q holds P.i= q.i
by A4,GRFUNC_1:2,AFINSQ_1:86;
set q0 = aSeq(I,len p) ^ <% f:=<0,...,0>I %>;
consider pp being XFinSequence of D^omega such that
A6: len pp = len p and
A7: for k being Nat st k < len pp
ex i being Integer st i = p.(k+1) &
pp.k = (aSeq(I,k+1) ^ aSeq(V,i) ^ <% (f,I):=V %>) and
A8: aSeq(f,p) = FlattenSeq pp by Def3;
len Stop SCM+FSA = 1 by AFINSQ_1:34;
then len q = len (q0 ^ FlattenSeq pp) + 1 by A8,AFINSQ_1:17;
then
A9: len (q0 ^ FlattenSeq pp) < len q by NAT_1:13;
defpred P[XFinSequence] means $1 c= pp implies
(ex pp0 being XFinSequence of D^omega st
(pp0 = $1 &
(for i being Nat st i <= len (q0 ^ FlattenSeq pp0)
holds IC Comput(P,s,i) = i) &
((Comput(P,s,len (q0^ FlattenSeq pp0)).f) | len pp0
= p | len pp0) &
len (Comput(P,s,len(q0 ^FlattenSeq pp0)).f) = len p &
(for b being Int-Location st b <> I & b <> V
holds Comput(P,s,len (q0 ^ FlattenSeq pp0)).b = s.b) &
(for g being FinSeq-Location st g <> f
holds Comput(P,s,len (q0 ^ FlattenSeq pp0)).g = s.g)));
A10: V <> O by AMI_3:10;
A11: for r being XFinSequence, x being object st P[r] holds P[r ^ <% x %>]
proof
let r be XFinSequence, x be object;
assume
A12: P[r];
set r1 = len r;
len<% x %> =1 by AFINSQ_1:34;
then len (r ^ <% x %>) = r1+1 by AFINSQ_1:17;
then r1 < len (r ^ <% x %>) by XREAL_1:29;
then
A13: r1 in dom (r ^ <% x %>) by AFINSQ_1:86;
assume
A14: r ^ <% x %> c= pp;
then
A15: dom (r ^ <% x %>) c= dom pp by GRFUNC_1:2;
then
A16: r1 < len pp by A13,AFINSQ_1:86;
then consider pr1 being Integer such that
A17: pr1 = p.(r1+1) and
A18: pp.r1 = aSeq(I,r1+1) ^ aSeq(V,pr1) ^ <% (f,I):=V %> by A7;
1 <= r1+1 & r1+1 <= len pp by A16,NAT_1:11,13;
then
A19: r1+1 in Seg len pp;
r c= r ^ <% x %> by AFINSQ_1:74;
then consider pp0 being XFinSequence of D^omega such that
A20: pp0 = r and
A21: for i being Nat st i <= len (q0 ^ FlattenSeq pp0)
holds IC Comput(P,s,i) = i and
A22: (Comput(P,s,len (q0 ^ FlattenSeq pp0)).f) | len pp0 = p |
len pp0 and
A23: len (Comput(P,s,len (q0 ^ FlattenSeq pp0)).f) = len p and
A24: for b being Int-Location st b <> I & b <> V holds Comput(P,s,
len (q0 ^ FlattenSeq pp0)).b = s.b and
A25: for h being FinSeq-Location st h <> f holds Comput(P,s,len (
q0 ^ FlattenSeq pp0)).h = s.h by A12,A14,XBOOLE_1:1;
A26: x = (r ^ <% x %>).r1 by AFINSQ_1:36
.= pp.r1 by A14,A13,GRFUNC_1:2;
then x in D^omega by A13,A15,FUNCT_1:102;
then reconsider pp1 = pp0 ^ <% x %> as XFinSequence of D^omega;
take pp1;
thus pp1 = r ^ <% x %> by A20;
reconsider x as Element of D^omega by A13,A15,A26,FUNCT_1:102;
A27: FlattenSeq pp1 = FlattenSeq pp0 ^ FlattenSeq <% x %> by AFINSQ_2:75
.= FlattenSeq pp0 ^ x by AFINSQ_2:73;
A28: Seg len p = dom p by FINSEQ_1:def 3;
len pp1 <= len p by A6,A14,A20,NAT_1:43;
then
A29: Seg len pp1 c= Seg len p by FINSEQ_1:5;
then
A30: dom (p | Seg len pp1) = Seg len pp1 by A28,RELAT_1:62;
set c2 = len (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1));
set c1 = len (q0 ^ FlattenSeq pp0);
set s1 = Comput(P,s,c1);
set s2 = Comput(P,s,c2);
A31: x = aSeq(I,r1+1) ^ (aSeq(V,pr1) ^ <% (f,I):=V %>) by A18,A26,AFINSQ_1:27;
then
A32: len q0 + len FlattenSeq pp1 = len q0 + len (FlattenSeq pp0 ^ aSeq(I,
r1+1) ^ (aSeq(V,pr1) ^ <% (f,I):=V %>)) by A27,AFINSQ_1:27
.= len (q0 ^ (FlattenSeq pp0 ^ aSeq(I,r1+1) ^
(aSeq(V,pr1) ^ <% (f,I):=V%>))) by AFINSQ_1:17
.= len (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1) ^
(aSeq(V,pr1) ^ <% (f,I):=V%>)) by Lm2
.= c2 + len (aSeq(V,pr1) ^ <% (f,I):=V %>) by AFINSQ_1:17
.= c2 + (len aSeq(V,pr1) + len <% (f,I):=V %>) by AFINSQ_1:17
.= c2 + (len aSeq(V,pr1) + 1) by AFINSQ_1:33
.= c2 + len aSeq(V,pr1) + 1;
then
A33: len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(V,pr1) + 1 by AFINSQ_1:17;
A34: FlattenSeq pp1 c= FlattenSeq pp by A14,A20,AFINSQ_2:82;
A35: now
let p be XFinSequence;
assume p c= x;
then FlattenSeq pp0 ^ p c= FlattenSeq pp0 ^ x by AFINSQ_2:81;
then FlattenSeq pp0 ^ p c= FlattenSeq pp by A34,A27,XBOOLE_1:1;
then q0 ^ (FlattenSeq pp0 ^ p) c= q0 ^ FlattenSeq pp by AFINSQ_2:81;
then
A36: q0 ^ FlattenSeq pp0 ^ p c= q0 ^ FlattenSeq pp by AFINSQ_1:27;
q0 ^ FlattenSeq pp c= q by A8,AFINSQ_1:74;
hence q0 ^ FlattenSeq pp0 ^ p c= q by A36,XBOOLE_1:1;
end;
IC s1 = c1 by A21;
then reconsider s1 as c1-started State of SCM+FSA by MEMSTR_0:def 12;
A37: s1.O = 1 by A1,A10,A3,A24;
A38: for c being Nat st c in dom aSeq(I,r1+1)
holds aSeq(I,r1+1).c = P.(c1 + c)
proof
let c be Nat;
assume
A39: c in dom aSeq(I,r1+1);
then
A40: c1 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1)) by AFINSQ_1:23;
A41: q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1) c= q by A31,A35,AFINSQ_1:74;
then
A42: dom (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1)) c= dom q by GRFUNC_1:2;
thus aSeq(I,r1+1).c = (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1)).(c1 + c)
by A39,AFINSQ_1:def 3
.= q.(c1 + c) by A41,A40,GRFUNC_1:2
.= P. (c1 + c) by A4,A42,A40,GRFUNC_1:2;
end;
then
A43: Comput(P,s1,len aSeq(I,r1+1)).I = r1+1 by Th4,A37,A1;
A44: q0 ^ FlattenSeq pp1 = q0 ^ FlattenSeq pp0 ^ x by A27,AFINSQ_1:27;
then len (q0 ^ FlattenSeq pp1) <= len q by A35,NAT_1:43;
then
A45: c2 + len aSeq(V,pr1) < len q by A33,NAT_1:13;
A46: now
let i be Nat;
assume i <= len aSeq(I,r1+1);
hence (c1 + i) = IC Comput(P,s1,i) by A38,Th4,A37,A1
.= IC Comput(P,s,c1+i) by EXTPRO_1:4;
end;
set c3 = len (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1) ^ aSeq(V,pr1));
A47: c3 = c2 + len aSeq(V,pr1) by AFINSQ_1:17;
A48: c2 = c1 + len aSeq(I,r1+1) by AFINSQ_1:17;
then
A49: s2 = Comput(P,Comput(P
,s,c1),len aSeq(I,r1+1)) by EXTPRO_1:4;
IC s2 = c2 by A48,A49,A38,Th4,A37,A1;
then reconsider s2 as c2-started State of SCM+FSA by MEMSTR_0:def 12;
A50: s2.O = 1 by A49,A38,Th4,A37,A1;
A51: for c being Nat st c in dom aSeq(V,pr1)
holds aSeq(V,pr1).c = P.(c2 + c)
proof
let c be Nat;
assume
A52: c in dom aSeq(V,pr1);
then
A53: c2 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1) ^ aSeq(V,pr1)) by
AFINSQ_1:23;
q0 ^ FlattenSeq pp0 ^ (aSeq(I,r1+1) ^ aSeq(V,pr1)) c= q by A18,A26,A35,
AFINSQ_1:74;
then
A54: q0 ^FlattenSeq pp0^aSeq(I,r1+1) ^ aSeq(V,pr1) c= q by AFINSQ_1:27;
then
A55: dom (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1) ^ aSeq(V,pr1)) c= dom q by
GRFUNC_1:2;
thus aSeq(V,pr1).c
= (q0 ^ FlattenSeq pp0 ^ aSeq(I,r1+1) ^ aSeq(V,pr1)).(c2 + c)
by A52,AFINSQ_1:def 3
.= q.(c2 + c) by A53,A54,GRFUNC_1:2
.= P. (c2 + c) by A4,A55,A53,GRFUNC_1:2;
end;
then
A56: Comput(P,s2,len aSeq(V,pr1)).V = pr1 by Th4,A50,A10;
A57: Comput(P,s,c3).f = Comput(P,s,c2 + len aSeq(V,
pr1)).f by AFINSQ_1:17
.= Comput(P,s2,len aSeq(V,pr1)).f by EXTPRO_1:4
.= s2.f by A51,Th4,A50,A10
.= s1.f by A49,A38,Th4,A37,A1;
A58: now
let i be Nat;
assume i <= len aSeq(V,pr1);
hence (c2 + i) = IC Comput(P,s2,i)
by A51,Th4,A50,A10
.= IC Comput(P,s,c2+i) by EXTPRO_1:4;
end;
A59: for i being Nat st i < len (q0 ^ FlattenSeq pp1) holds IC
Comput(P,s,i) = i
proof
let i be Nat;
assume
A60: i < len (q0 ^ FlattenSeq pp1);
A61: now
A62: i < len q0 + len FlattenSeq pp1 by A60,AFINSQ_1:17;
assume
A63: not i <= c1;
assume not (c1 + 1 <= i & i <= c2);
hence c2 + 1 <= i & i <= c2 + len aSeq(V,pr1) by A32,A63,A62,NAT_1:13;
end;
per cases by A61;
suppose
i <= len (q0 ^ FlattenSeq pp0);
hence thesis by A21;
end;
suppose
A64: c1 + 1 <= i & i <= c2;
then c1 + 1 - c1 <= i - c1 by XREAL_1:9;
then reconsider ii = i - c1 as Element of NAT by INT_1:3;
i - c1 <= c2 - c1 by A64,XREAL_1:9;
hence i = IC Comput(P,s,c1+ii) by A48,A46
.= IC Comput(P,s,i);
end;
suppose
A65: c2 + 1 <= i & i <= c2 + len aSeq(V,pr1);
then c2 + 1 - c2 <= i - c2 by XREAL_1:9;
then reconsider ii = i - c2 as Element of NAT by INT_1:3;
i - c2 <= c2 + len aSeq(V,pr1) - c2 by A65,XREAL_1:9;
hence i = IC Comput(P,s,c2+ii) by A58
.= IC Comput(P,s,i);
end;
end;
A66: c3 = c1 + len aSeq(I,r1+1) + len aSeq(V,pr1) by A48,AFINSQ_1:17;
A67: P/.IC Comput(P,s,c3) = P.IC Comput(P,s,c3) by PBOOLE:143;
q0 ^ FlattenSeq pp0 ^ x c= q by A35;
then consider rq being XFinSequence of D such that
A68: (q0 ^ FlattenSeq pp0 ^ x)^rq = q by AFINSQ_2:80;
A69: len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(V,pr1) + 1 by A32,AFINSQ_1:17;
then
A70: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(V,pr1) by NAT_1:13;
then
A71: c3 in dom(q0 ^ FlattenSeq pp0 ^ x)
by A44,A47,AFINSQ_1:66;
A72: 0 in dom<% (f,I):=V %> by TARSKI:def 1;
len<% (f,I):=V %> = 1 by AFINSQ_1:34;
then len(aSeq(I,r1+1) ^ aSeq(V,pr1) ^ <% (f,I):=V %>)
= len (aSeq(I,r1+1) ^ aSeq(V,pr1)) + 1 by AFINSQ_1:17;
then len (aSeq(I,r1+1) ^ aSeq(V,pr1))
< len(aSeq(I,r1+1) ^ aSeq(V,pr1) ^ <% (f,I):=V %>) by XREAL_1:29;
then
A73: len (aSeq(I,r1+1) ^ aSeq(V,pr1))
in dom(aSeq(I,r1+1) ^ aSeq(V,pr1) ^ <% (f,I):=V %>) by AFINSQ_1:66;
CurInstr(P,Comput(P,s,c3))
= P. c3 by A47,A59,A67,A70
.= q.(c3 ) by A5,A47,A45
.= (q0 ^ FlattenSeq pp0 ^ x).
(c1 + (len aSeq(I,r1+1) + (len aSeq(V,pr1))))
by A66,A71,A68,AFINSQ_1:def 3
.= (q0 ^ FlattenSeq pp0 ^ x).
(c1 + len(aSeq(I,r1+1) ^ aSeq(V,pr1))) by AFINSQ_1:17;
then
A74: CurInstr(P,
Comput(P,s,c3))
= (aSeq(I,r1+1) ^ aSeq(V,pr1) ^ <% (f,I):=V %>).
(len (aSeq(I,r1+1) ^ aSeq(V,pr1))+0) by A73,A18,A26,AFINSQ_1:def 3
.= <% (f,I):=V %>.0 by A72,AFINSQ_1:def 3
.= (f,I):=V;
A75: Comput(P,s,c3+1) = Following(P,Comput(P,s,c3)) by EXTPRO_1:3
.= Exec((f,I):=V, Comput(P,s,c3)) by A74;
then
A76: IC Comput(P,s,len (q0 ^ FlattenSeq pp1))
= IC Comput(P,s,c3)+1 by A47,A33,SCMFSA_2:73
.= len (q0 ^ FlattenSeq pp1) by A47,A69,A59,A70;
thus for i being Nat st i <= len (q0 ^ FlattenSeq pp1) holds IC
Comput(P,s,i) = i
proof
let i be Nat;
assume
A77: i <= len (q0 ^ FlattenSeq pp1);
per cases by A77,XXREAL_0:1;
suppose
i < len (q0 ^ FlattenSeq pp1);
hence thesis by A59;
end;
suppose
i = len (q0 ^ FlattenSeq pp1);
hence thesis by A76;
end;
end;
A78: Comput(P,s,c3).V
= Comput(P,s,c2 + len aSeq(V,pr1)).V by AFINSQ_1:17
.= p.(r1+1) by A17,A56,EXTPRO_1:4;
consider ki being Nat such that
A79: ki = |. Comput(P,s,c3).I.| and
A80: Exec((f,I):=V, Comput(P,s,c3)).f
= Comput(P,s,c3).f +*(ki,Comput(P,s,c3).V)
by SCMFSA_2:73;
A81: ki = |. Comput(P,s,c2 + len aSeq(V,pr1)).I .| by A79,AFINSQ_1:17
.= |. Comput(P,s2,len aSeq(V,pr1)).I .| by EXTPRO_1:4
.= |. s2.I .| by A2,A51,Th4,A50,A10
.= r1+1 by A49,A43,ABSVALUE:def 1;
A82: dom (s1.f) = Seg len p by A23,FINSEQ_1:def 3;
for i being Nat st i in Seg len pp1
holds ((Comput(P,s,len (q0 ^ FlattenSeq pp1)).f)
| Seg len pp1).i
= (p | Seg len pp1).i
proof
let i be Nat;
assume
A83: i in Seg len pp1;
then
A84: i <= len pp1 by FINSEQ_1:1;
len<% x %> = 1 by AFINSQ_1:34;
then
A85: len pp1 = len pp0 + 1 by AFINSQ_1:17;
per cases;
suppose
A86: i = len pp1;
thus
((Comput(P,s,len (q0 ^ FlattenSeq pp1))).f |
Seg len pp1).i =
(s1.f +*(r1+1,p.(r1+1))).i
by A47,A69,A75,A80,A81,A78,A57,A86,A85,FINSEQ_1:4,FUNCT_1:49
.= p.i by A20,A6,A82,A86,A19,A85,FUNCT_7:31
.= (p | Seg len pp1).i by A86,A85,FINSEQ_1:4,FUNCT_1:49;
end;
suppose
A87: i <> len pp1;
then i < len pp0 + 1 by A85,A84,XXREAL_0:1;
then
A88: i <= len pp0 by NAT_1:13;
1 <= i by A83,FINSEQ_1:1;
then
A89: i in Seg len pp0 by A88;
((Comput(P,s,len (q0 ^ FlattenSeq pp1))).f |
Seg len pp1).i =
(s1.f +*(r1+1,p.(r1+1))).i
by A47,A69,A75,A80,A81,A78,A57,A83,FUNCT_1:49
.= s1.f.i by A85,A20,A87,FUNCT_7:32;
hence
((Comput(P,s,len (q0 ^ FlattenSeq pp1))).f |
Seg len pp1).i =
(p | Seg len pp0).i by A22,A89,FUNCT_1:49
.= p.i by A89,FUNCT_1:49
.= (p | Seg len pp1).i by A83,FUNCT_1:49;
end;
end;
then
A90: for i being object st i in Seg len pp1
holds ((Comput(P,s,len (q0 ^FlattenSeq pp1)).f) | Seg len pp1).i
= (p | Seg len pp1).i;
A91: dom (s1.f +*(r1+1,p.(r1+1))) = dom (s1.f) by FUNCT_7:30;
dom (Comput(P,s,len (q0 ^ FlattenSeq pp1)).f)
= dom (s1.f +*(r1+1,p.(r1+1)))
by A33,A75,A80,A81,A78,A57,AFINSQ_1:17
.= Seg len p
by A23,A91,FINSEQ_1:def 3;
then dom ((Comput(P,s,len (q0 ^ FlattenSeq pp1)).f)
| Seg len pp1 ) =
Seg len pp1 by A29,RELAT_1:62;
hence (Comput(P,s,len (q0 ^ FlattenSeq pp1)).f) | len pp1
= p | len pp1 by A30,A90,FUNCT_1:2;
len (s1.f +*(r1+1,p.(r1+1))) = len (s1.f) by A91,FINSEQ_3:29;
hence len (Comput(P,s,len (q0^FlattenSeq pp1)).f)
= len p by A23,A33,A75,A80,A81,A78,A57,AFINSQ_1:17;
hereby
let b be Int-Location;
assume that
A92: b <> I and
A93: b <> V;
thus Comput(P,s,len (q0 ^ FlattenSeq pp1)).b = Comput(
P,s,c2 + len
aSeq(V,pr1)).b by A47,A33,A75,SCMFSA_2:73
.= Comput(P,s2,len aSeq(V,pr1)).b by EXTPRO_1:4
.= s2.b by A51,A93,Th4,A50,A10
.= s1.b by A49,A38,A92,Th4,A37,A1
.= s.b by A24,A92,A93;
end;
hereby
let h be FinSeq-Location;
assume
A94: h <> f;
hence
Comput(P,s,len (q0 ^ FlattenSeq pp1)).h = Comput(P,s,c2 + len
aSeq(V,pr1)).h by A47,A33,A75,SCMFSA_2:73
.= Comput(P,s2,len aSeq(V,pr1)).h by EXTPRO_1:4
.= s2.h by A51,Th4,A50,A10
.= s1.h by A49,A38,Th4,A37,A1
.= s.h by A25,A94;
end;
end;
set k = len aSeq(I,len p);
len<% f:=<0,...,0>I %> = 1 by AFINSQ_1:34;
then
A95: len q0 = k + 1 by AFINSQ_1:17;
A96: q = aSeq(I,len p)^<% f:=<0,...,0>I %>^(aSeq(f,p)^Stop SCM+FSA) by
AFINSQ_1:27;
then q = aSeq(I,len p)^(<% f:=<0,...,0>I %>^(aSeq(f,p)^Stop SCM+FSA))
by AFINSQ_1:27;
then aSeq(I,len p) c= f:=p by AFINSQ_1:74;
then
A97: aSeq(I,len p) c= P by A4,XBOOLE_1:1;
then
A98: Comput(P,s,len aSeq(I,len p)).I = len p by A1,A3,Th5;
A99: P[{}]
proof
A100: now
let i be Nat such that
A101: i < len q0;
i < len q0 implies i <= len aSeq(I,len p) by A95,NAT_1:13;
hence IC Comput(P,s,i) = i by A1,A3,A97,A101,Th5;
end;
assume {} c= pp;
reconsider sD = <%>(D^omega) as XFinSequence of D^omega;
take sD;
A102: q0 ^ FlattenSeq <%>(D^omega) = q0 ^ <%>D by AFINSQ_2:74
.= q0 ^ {}
.= q0;
A103: k < len q0 by A95,NAT_1:13;
then
A104: IC Comput(P,s,k) = k by A100;
A105: P/.IC Comput(P,s,k) = P.IC Comput(P,s,k) by PBOOLE:143;
len q = len q0 + len ((aSeq(f,p) ^ Stop SCM+FSA)) by A96,AFINSQ_1:17;
then len q0 <= len q by NAT_1:11;
then
A106: k < len q by A95,NAT_1:13;
A107: q = aSeq(I,len p)^<% f:=<0,...,0>I %>^(aSeq(f,p)^Stop SCM+FSA)
by AFINSQ_1:27;
A108: k in dom q0 by A103,AFINSQ_1:66;
A109: CurInstr(P,Comput(P,s,k))
= q.k by A5,A104,A105,A106
.= q0.k by A107,A108,AFINSQ_1:def 3
.= f:=<0,...,0>I by AFINSQ_1:36;
thus sD = {};
A110: Comput(P,s,len q0) =
Following(P,Comput(P,s,k))
by A95,EXTPRO_1:3
.= Exec(f:=<0,...,0>I, Comput(P,s,k)) by A109;
then
A111: IC Comput(P,s,len q0) = len q0 by A95,A104,SCMFSA_2:75;
now
let i be Nat;
assume i <= len q0;
then i < len q0 or i = len q0 by XXREAL_0:1;
hence IC Comput(P,s,i) = i by A100,A111;
end;
hence for i being Nat st i <= len (q0 ^ FlattenSeq sD)
holds IC Comput(P,s,i) = i by A102;
consider ki being Nat such that
A112: ki = |. Comput(P,s,k).I.| and
A113: Exec(f:=<0,...,0>I, Comput(P,s,k)).f = ki |-> 0 by SCMFSA_2:75;
(Comput(P,s,len (q0 ^ FlattenSeq sD)).f) | 0 = p | len sD;
hence
(Comput(P,s,len (q0 ^ FlattenSeq sD)).f)|len sD = p
| len sD;
ki = len p by A98,A112,ABSVALUE:def 1;
hence len (Comput(P,s,len (q0 ^ FlattenSeq sD)).f) = len p
by A102,A110,A113,CARD_1:def 7;
now
let b be Int-Location such that
A114: b <> I and
b <> V;
thus Comput(P,s,len q0).b = Comput(P,s,k).b by A110,SCMFSA_2:75
.= s.b by A1,A3,A97,A114,Th5;
end;
hence
for b being Int-Location st b <> I & b <> V holds Comput(P,s,
len (
q0 ^ FlattenSeq sD)).b = s.b by A102;
now
let g be FinSeq-Location;
assume g <> f;
hence Comput(P,s,len q0).g = Comput(P,s,k).g
by A110,SCMFSA_2:75
.= s.g by A1,A3,A97,Th5;
end;
hence thesis by A102;
end;
for r being XFinSequence holds P[r] from AFINSQ_1:sch 3(A99,A11);
then consider pp0 being XFinSequence of D^omega such that
A115: pp0 = pp and
A116: for i being Nat st i <= len (q0 ^ FlattenSeq pp0) holds
IC Comput(P,s,i) = i and
A117: (Comput(P,s,len (q0 ^ FlattenSeq pp0)).f) | len pp0
= p | len pp0 and
A118: len (Comput(P,s,len (q0 ^ FlattenSeq pp0)).f) = len p and
A119: ( for b being Int-Location st b <> I & b <> V holds Comput(P
,s,
len (q0 ^ FlattenSeq pp0)).b = s.b)& for g being FinSeq-Location st g <> f
holds Comput(P,s,len (q0 ^ FlattenSeq pp0)).g = s.g;
A120: P/.IC Comput(P,s,len (q0 ^ FlattenSeq pp))
= P.IC Comput(P,s,len (q0 ^ FlattenSeq pp)) by PBOOLE:143;
IC Comput(P,s,len (q0 ^ FlattenSeq pp))
= len (q0 ^ FlattenSeq pp) by A115,A116;
then
A121: CurInstr(P,
Comput(P,s,len (q0 ^ FlattenSeq pp)))
= q.len (q0 ^ FlattenSeq pp) by A5,A9,A120
.= halt SCM+FSA by A8,AFINSQ_1:36;
hence P halts_on s by EXTPRO_1:29;
then
A122: Comput(P,s,len (q0^FlattenSeq pp))
= Result(P,s) by A121,EXTPRO_1:def 9;
A123: Seg len pp0 = dom p by A6,A115,FINSEQ_1:def 3;
(Comput(P,s,len (q0 ^ FlattenSeq pp0)).f)
= (Comput(P,s,len (q0 ^ FlattenSeq pp0)).f) | len pp0
by A6,A115,A118,FINSEQ_3:113;
hence (Result(P,s)).f = p by A123,A115,A122,A117;
thus thesis by A115,A119,A122;
end;