:: Constant assignment macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 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, AMI_1, SCMFSA_2, RELAT_1, SCMFSA_7,
ARYTM_3, ARYTM_1, TARSKI, FUNCT_1, XXREAL_0, PARTFUN1, CAT_1, NAT_1,
CARD_1, FUNCOP_1, SCMFSA6A, ORDINAL4, AMI_3, FUNCT_4, INT_1, GRAPHSP,
FSM_1, CIRCUIT2, EXTPRO_1, SCMFSA6B, SF_MASTR, MSUALG_1, XBOOLE_0,
PRE_POLY, AMISTD_2, SCMFSA7B, AFINSQ_1, SCMFSA6C, COMPOS_1, AMISTD_1,
TURING_1, RELOC, VALUED_1, SCMPDS_4;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0,
COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2,
FUNCOP_1, XXREAL_0, ENUMSET1, NAT_D, PBOOLE, AFINSQ_2, AMISTD_4,
SCMFSA_7, COMPOS_2, SCMFSA6A, SF_MASTR, SCMFSA6B, INT_2, PRE_POLY,
SCMFSA_M;
constructors ENUMSET1, XXREAL_0, REAL_1, SCMFSA_7, SCMFSA6A, SF_MASTR,
SCMFSA6B, NAT_D, RELSET_1, PRE_POLY, DOMAIN_1, AFINSQ_2, PARTFUN3,
PBOOLE, AMISTD_1, AMISTD_2, AMI_3, MEMSTR_0, SCMFSA_M, FUNCT_7, COMPOS_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1,
INT_1, SCMFSA_2, SCMFSA6B, ORDINAL1, CARD_1, AFINSQ_1, COMPOS_1,
AFINSQ_2, EXTPRO_1, FUNCT_4, STRUCT_0, MEMSTR_0, SCMFSA10, COMPOS_0,
SCMFSA_M, COMPOS_2, SCMFSA6C, SCMFSA_4;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, SCMFSA6B, AMISTD_1;
equalities FUNCOP_1, SCMFSA6A, SCMFSA6B, COMPOS_1, SCMFSA_7, EXTPRO_1,
MEMSTR_0, SCMFSA_M, ORDINAL1, COMPOS_2;
expansions TARSKI, AMISTD_1;
theorems SCMFSA_7, NAT_1, GRFUNC_1, FUNCT_1, FUNCT_4, FUNCT_7, ENUMSET1,
SCMFSA_2, FUNCOP_1, INT_1, RELAT_1, TARSKI, SF_MASTR, XBOOLE_0, XBOOLE_1,
XREAL_1, XXREAL_0, AFINSQ_1, COMPOS_1, AFINSQ_2, CARD_1, EXTPRO_1,
PARTFUN1, MEMSTR_0, SCMFSA_M, ORDINAL1, AMISTD_1, COMPOS_0, VALUED_1;
schemes NAT_1, AFINSQ_1;
begin
reserve m for Nat;
reserve P for Instruction-Sequence of SCM+FSA;
set A = NAT;
theorem
for i being Instruction of SCM+FSA holds (i = halt SCM+FSA implies (
Directed Macro i). 0 = goto 2) & (i <> halt SCM+FSA implies (
Directed Macro i). 0 = i)
proof
A1: dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA;
let i be Instruction of SCM+FSA;
A2: (Macro i). 0 = i by COMPOS_1:58;
0 in { 0, 1} by TARSKI:def 2;
then
A3: 0 in dom Macro i by COMPOS_1:61;
A4: card Macro i = 2 by COMPOS_1:56;
hereby
A5: dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA;
assume
A6: i = halt SCM+FSA;
A7: i in dom (halt SCM+FSA .--> goto 2) by A6,TARSKI:def 1;
rng Macro i c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
hence
(Directed Macro i). 0 = (((id the InstructionsF of SCM+FSA) +* (
halt SCM+FSA, goto 2))*Macro i). 0 by A4,FUNCT_7:116
.= (((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto
2))*Macro i). 0 by A5,FUNCT_7:def 3
.= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto
2)).i by A3,A2,FUNCT_1:13
.= (halt SCM+FSA .--> goto 2).i by A7,FUNCT_4:13
.= goto 2 by A6,FUNCOP_1:72;
end;
assume i <> halt SCM+FSA;
then
A9: not i in dom (halt SCM+FSA .--> goto 2) by TARSKI:def 1;
rng Macro i c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
hence (Directed Macro i). 0 = (((id the InstructionsF of SCM+FSA) +* (
halt SCM+FSA, goto 2))* Macro i). 0 by A4,FUNCT_7:116
.= (((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto
2))* Macro i). 0 by A1,FUNCT_7:def 3
.= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2
)).i by A3,A2,FUNCT_1:13
.= (id the InstructionsF of SCM+FSA).i by A9,FUNCT_4:11
.= i;
end;
theorem
for i being Instruction of SCM+FSA holds (Directed Macro i). 1 = goto 2
proof
let i be Instruction of SCM+FSA;
A1: (Macro i). 1 = halt SCM+FSA by COMPOS_1:59;
1 in { 0, 1} by TARSKI:def 2;
then
A2: 1 in dom Macro i by COMPOS_1:61;
A3: halt SCM+FSA in dom (halt SCM+FSA .--> goto 2) by TARSKI:def 1;
A4: dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA;
card Macro i = 2 & rng Macro i c= the InstructionsF of SCM+FSA
by COMPOS_1:56,RELAT_1:def 19;
hence (Directed Macro i). 1 = (((id the InstructionsF of SCM+FSA) +* (
halt SCM+FSA,goto 2))* Macro i). 1 by FUNCT_7:116
.= (((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto
2))* Macro i). 1 by A4,FUNCT_7:def 3
.= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto 2
)). halt SCM+FSA by A2,A1,FUNCT_1:13
.= (halt SCM+FSA .--> goto 2).halt SCM+FSA by A3,FUNCT_4:13
.= goto 2 by FUNCOP_1:72;
end;
registration
let a be Int-Location, k be Integer;
cluster a := k -> initial non empty
NAT-defined (the InstructionsF of SCM+FSA)-valued;
coherence
proof
a := k = aSeq(a,k) ^ Stop SCM+FSA by SCMFSA_7:1;
hence thesis;
end;
end;
Lm1: for s being State of SCM+FSA st IC s = 0
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location, k being Integer
st a := k c= P
holds P halts_on s
proof
let s be State of SCM+FSA;
assume
A1: IC s = 0;
let P be Instruction-Sequence of SCM+FSA;
A2: dom P = NAT by PARTFUN1:def 2;
let a be Int-Location, k be Integer;
assume
A3: a := k c= P;
per cases;
suppose
A4: k > 0;
then consider k1 being Nat such that
A5: k1 + 1 = k and
A6: a := k = <% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) ^
Stop SCM+FSA by SCMFSA_7:def 1;
A7: 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:34
.= k by A5;
set f = <% a:=intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA;
A8: 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;
reconsider k as Element of NAT by A4,INT_1:3;
A9: len f = len (<% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0))) + len
Stop SCM+FSA by AFINSQ_1:17
.= k + 1 by A7,AFINSQ_1:34;
A10: now
let i be Element of NAT;
assume that
A11: i <= k;
i < k + 1 by A11,NAT_1:13;
hence i in dom f by A9,AFINSQ_1:86;
end;
A12: for i being Element of NAT st i <= k holds P.i = f.i
by A3,A6,A10,GRFUNC_1:2;
then
A13: P. 0 = a := intloc 0 by A8;
A14: now
let n be Element of NAT;
assume n = 0;
hence
A15: Comput(P,s,n) = s;
hence CurInstr(P,Comput(P,s,n)) = a:= intloc 0
by A1,A13,A2,PARTFUN1:def 6;
thus Comput(P,s,n+1) = Following(P,
Comput(P,s,n)) by EXTPRO_1:3
.= Exec(a:= intloc 0,s) by A15,A1,A13,A2,PARTFUN1:def 6;
end;
A16: now
let i be Element of NAT;
assume that
A17: 1 <= i and
A18: i < k;
reconsider i1 = i - 1 as Element of NAT by A17,INT_1:5;
i - 1 < k - 1 by A18,XREAL_1:9;
then
A19: i1 in Segm k1 by A5,NAT_1:44;
A20: len <%a:= intloc 0%> = 1 by AFINSQ_1:33;
A21: len(k1-->AddTo(a,intloc 0)) = k1;
i in dom (<%a:=intloc 0%>^(k1-->AddTo(a,intloc 0)))
by A18,A7,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 A17,A18,A20,A21,A5,AFINSQ_1:18
.= AddTo(a,intloc 0) by A19,FUNCOP_1:7;
end;
A22: now
let i be Nat;
assume that
A23: 0 < i and
A24: i < k;
A25: 0+1 <= i by A23,NAT_1:13;
A26: i in NAT by ORDINAL1:def 12;
hence P. i = f.(i) by A12,A24
.=AddTo(a,intloc 0) by A16,A25,A24,A26;
end;
A27: for i being Element of 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 Element of 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 A14
.= n+1 by A1,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,A2,PARTFUN1:def 6,XXREAL_0:2
.= AddTo(a,intloc 0) by A22,A32,A34;
A36: 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;
thus IC Comput(P,s,n+1)
= IC Comput(P,s,n)+1 by A36,SCMFSA_2:64
.= n+1 by A30,A31,NAT_1:13;
end;
end;
A37: P[0] by A1;
for i being Nat holds P[i] from NAT_1:sch 2(A37,A29);
hence thesis by A28;
end;
k < k + len Stop SCM+FSA by XREAL_1:29;
then
A38: f.(k) = (Stop SCM+FSA).(k - k) by A7,AFINSQ_1:18
.= halt SCM+FSA by AFINSQ_1:34;
CurInstr(P,Comput(P,s,k)) = P.IC Comput(P,s,k) by A2,PARTFUN1:def 6
.= P. k by A27
.= halt SCM+FSA by A38,A12;
hence thesis by EXTPRO_1:29;
end;
suppose
A39: k <= 0;
then reconsider mk = - k as Element of NAT by INT_1:3;
consider k1 being Nat such that
A40: k1 + k = 1 and
A41: a:=k = (<%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) ^
Stop SCM+FSA) by A39,SCMFSA_7:def 1;
A42: 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:34
.= mk+1+1 by A40;
set f = <%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA;
A43: 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;
A44: len f = len(<%a:=intloc 0%>^(k1-->SubFrom(a,intloc 0)))+len Stop
SCM+FSA by AFINSQ_1:17
.= mk+1+1 + 1 by A42,AFINSQ_1:34;
A45: now
let i be Nat;
assume that
0 <= i and
A46: i <= mk+1+1;
i < mk+1+1+1 by A46,NAT_1:13;
hence i in dom f by A44,AFINSQ_1:86;
end;
A47: for i being Nat st 0 <= i & i <= mk+1+1
holds P.i = f.i by A3,A41,A45,GRFUNC_1:2;
then
A48: P.0 = a := intloc 0 by A43;
A49: now
let n be Element of NAT;
assume n = 0;
hence
A50: Comput(P,s,n) = s;
hence CurInstr(P,Comput(P,s,n)) = a:= intloc 0
by A1,A48,A2,PARTFUN1:def 6;
thus Comput(P,s,n+1) = Following(P,
Comput(P,s,n)) by EXTPRO_1:3
.= Exec(a:= intloc 0,s) by A50,A1,A48,A2,PARTFUN1:def 6;
end;
A51: now
A52: len <%a:= intloc 0%> = 1 by AFINSQ_1:33;
let i be Nat;
assume that
A53: 1 <= i and
A54: i < mk+1+1;
reconsider i1 = i - 1 as Element of NAT by A53,INT_1:5;
i-1 < k1+1-1 by A54,A40,XREAL_1:9;
then
A55: i1 in Segm k1 by NAT_1:44;
A56: len(k1-->SubFrom(a,intloc 0)) = k1;
i in dom (<%a:=intloc 0%>^(k1-->SubFrom(a,intloc 0)))
by A54,A42,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 A40,A53,A54,A52,A56,AFINSQ_1:18
.= SubFrom(a,intloc 0) by A55,FUNCOP_1:7;
end;
A57: now
let i be Nat;
assume that
A58: 0 < i and
A59: i < mk+1+1;
A60: 0+1 <= i by A58,NAT_1:13;
thus P. i = f.(i) by A47,A59
.=SubFrom(a,intloc 0) by A51,A60,A59;
end;
A61: 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
A62: i <= mk+1+1;
A63: for n being Nat st P[n] holds P[n + 1]
proof
let n be Nat;
assume
A64: P[n];
assume
A65: n+1 <= mk+1+1;
then
A66: n < mk+1+1 by NAT_1:13;
per cases;
suppose
A67: n=0;
hence IC Comput(P,s,n+1)
= Exec(a:= intloc 0,s).IC SCM+FSA by A49
.= n+1 by A1,A67,SCMFSA_2:63;
end;
suppose
A68: n>0;
n + 0 <= n + 1 by XREAL_1:7;
then
A69: CurInstr(P,Comput(P,s,n)) = P. n
by A64,A65,A2,PARTFUN1:def 6,XXREAL_0:2
.= SubFrom(a,intloc 0) by A57,A66,A68;
A70: 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 A69;
thus IC Comput(P,s,n+1)
= IC Comput(P,s,n) + 1 by A70,SCMFSA_2:65
.= n+1 by A64,A65,NAT_1:13;
end;
end;
A71: P[0] by A1;
for i being Nat holds P[i] from NAT_1:sch 2(A71,A63);
hence thesis by A62;
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 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
A72: f.(mk+1+1) = halt SCM+FSA by A42,XREAL_1:29;
CurInstr(P,Comput(P,s,mk+1+1))
= P.IC Comput(P,s,mk+1+1) by A2,PARTFUN1:def 6
.= P. (mk+1+1) by A61
.= halt SCM+FSA by A72,A47;
hence thesis by EXTPRO_1:29;
end;
end;
registration
let a be Int-Location, k be Integer;
cluster a := k -> parahalting;
correctness
proof
A1: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
let s be 0-started State of SCM+FSA;
A2: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA
such that
A3: a := k c= P;
IC s = IC Start-At(0,SCM+FSA) by A2,A1,GRFUNC_1:2
.= 0;
hence P halts_on s by Lm1,A3;
end;
end;
theorem
for s being State of SCM+FSA for a being read-write Int-Location, k
being Integer holds IExec(a := k,P,s).a = k & (for b being read-write
Int-Location st b <> a holds IExec(a := k,P,s).b = s.b) & for f being
FinSeq-Location holds IExec(a := k,P,s).f = s.f
proof
let s be State of SCM+FSA;
let a be read-write Int-Location;
let k be Integer;
set s1 = s +* Initialize((intloc 0).-->1);
A1: s1.intloc 0 = (Initialize((intloc 0).-->1)).intloc 0
by FUNCT_4:13,SCMFSA_M:10
.= 1 by SCMFSA_M:12;
reconsider s1 as 0-started State of SCM+FSA;
A2: a := k c= P+*(a:=k) by FUNCT_4:25;
thus IExec(a := k,P,s).a = (Result(P+*(a:=k),s1)).a
.= k by A1,A2,SCMFSA_7:6;
hereby
let b be read-write Int-Location;
assume
A3: b <> a;
b <> intloc 0 & b <> IC SCM+FSA by SCMFSA_2:56;
then
A4: not b in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2;
thus IExec(a := k,P,s).b = (Result(P+*(a:=k),s1)).b
.= s1.b by A1,A2,A3,SCMFSA_7:6
.= s.b by A4,FUNCT_4:11;
end;
let f be FinSeq-Location;
f <> intloc 0 & f <> IC SCM+FSA by SCMFSA_2:57,58;
then
A5: not f in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2;
thus IExec(a := k,P,s).f = (Result(P+*(a:=k),s1)).f
.= s1.f by A1,A2,SCMFSA_7:6
.= s.f by A5,FUNCT_4:11;
end;
Lm2: for p1,p2,p3,p4 being XFinSequence
holds 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
.= p1 ^ (p2 ^ p3 ^ p4) by AFINSQ_1:27;
end;
Lm3:
for c0 being Element of NAT
for s being c0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location, k being Integer st
for c being Element of NAT st c < len aSeq(a,k)
holds aSeq(a,k).c = P. (c0 + c)
for i being Element of NAT st i <= len aSeq(a,k)
holds IC Comput(P,s,i) = c0 + i
proof
let c0 be Element of NAT;
let s be c0-started State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
A1: dom P = NAT by PARTFUN1:def 2;
A2: IC s = c0 by MEMSTR_0:def 12;
let a be Int-Location;
let k be Integer;
assume
A3: for c being Element of NAT st c < len aSeq(a,k)
holds aSeq(a,k).c = P. (c0 + c);
A4: for c being Element of NAT st c in dom aSeq(a,k)
holds aSeq(a,k).c = P.(c0 + c)
by A3,AFINSQ_1:66;
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,
SCMFSA_7:def 2;
defpred Q[Nat] means $1 <= k9 implies IC Comput(P,s,$1) =
(c0 + $1);
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:34
.= k9 by A6;
for i being Element of NAT st i <= len aSeq(a,k9)
holds IC Comput(P,s,i) = (c0 + i)
proof
A9: now
let i be Element of NAT;
assume that
A10: 1 <= i and
A11: i < k9;
reconsider i1 = i - 1 as Element of NAT by A10,INT_1:5;
i = i1 + 1;
then
i1 < k1 by A11,A6,XREAL_1:6;
then
A12: i1 in Segm k1 by NAT_1:44;
A13: 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 A10,A7,A13,A6,A11,AFINSQ_1:18
.= AddTo(a,intloc 0) by A12,FUNCOP_1:7;
end;
A14: for i being Element of NAT st i < k9 holds i in dom aSeq(a,k9)
by A8,AFINSQ_1:86;
A15: now
let i be Nat;
assume that
A16: 0 < i and
A17: i < k9;
A18: 0+1 <= i by A16,NAT_1:13;
A19: i in NAT by ORDINAL1:def 12;
hence P. (c0 + i) = aSeq(a,k9).(i) by A4,A14,A17
.=AddTo(a,intloc 0) by A9,A18,A17,A19;
end;
A20: P. (c0 + 0) = aSeq(a,k9).0 by A3,A5,A8
.= a:= intloc 0 by A7,AFINSQ_1:35;
A21: now
let n be Element of NAT;
assume n = 0;
hence
A22: Comput(P,s,n) = s;
thus CurInstr(P,Comput(P,s,n))
= P.IC Comput(P,s,n) by A1,PARTFUN1:def 6
.= a:= intloc 0 by A20,A22,MEMSTR_0:def 12;
thus Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3
.= Exec(a:= intloc 0,s) by A22,A2,A20,A1,PARTFUN1:def 6;
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 A21
.= c0 + 1 + n by A2,A26,SCMFSA_2:63
.= c0 + (n + 1);
end;
suppose
A27: n > 0;
A28: n < k9 by A25,NAT_1:13;
A29: n + 0 <= n + 1 by XREAL_1:7;
A30: CurInstr(P,Comput(P,s,n))
= P.(c0 + n) by A24,A25,A29,A1,PARTFUN1:def 6,XXREAL_0:2
.= AddTo(a,intloc 0) by A15,A27,A28;
A31: 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 A30;
thus IC Comput(P,s,n+1)
= IC Comput(P,s,n) + 1 by A31,SCMFSA_2:64
.= (c0 + n + 1) by A24,A25,A29,XXREAL_0:2
.= (c0 + (n + 1));
end;
end;
let i be Element of NAT;
assume
A32: i <= len aSeq(a,k9);
A33: Q[0] by A2;
for i being Nat holds Q[i] from NAT_1:sch 2(A33,A23);
hence thesis by A8,A32;
end;
hence thesis;
end;
suppose
A34: 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);
consider k1 being Nat such that
A35: k1 + k = 1 and
A36: aSeq(a,k) = <%a:=intloc 0%> ^ (k1 --> SubFrom(a,intloc 0)) by A34,
SCMFSA_7:def 2;
A37: len aSeq(a,k) = len <% a:=intloc 0 %> + len (k1-->SubFrom(a,intloc 0)
) by A36,AFINSQ_1:17
.= 1 + len (k1-->SubFrom(a,intloc 0)) by AFINSQ_1:34
.= mk+1+1 by A35;
for i being Element of NAT st i <= len aSeq(a,k) holds IC Comput(
P,s,i) = (c0 + i)
proof
A38: now
let i be Element of NAT;
assume that
A39: 1 <= i and
A40: i < mk+1+1;
A41: i - 1 < mk+1+1 - 1 by A40,XREAL_1:9;
reconsider i1 = i - 1 as Element of NAT by A39,INT_1:5;
A42: i1 in Segm k1 by A35,A41,NAT_1:44;
A43: 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 A36,A39,A43,A35,A40,AFINSQ_1:18
.= SubFrom(a,intloc 0) by A42,FUNCOP_1:7;
end;
A44: for i being Element of NAT st i < mk+1+1 holds i in dom aSeq(a,k)
by A37,AFINSQ_1:86;
A45: now
let i be Nat;
assume that
A46: 0 < i and
A47: i < mk+1+1;
A48: 0+1 <= i by A46,NAT_1:13;
A49: i in NAT by ORDINAL1:def 12;
hence P. (c0 + i) = aSeq(a,k).(i) by A4,A44,A47
.=SubFrom(a,intloc 0) by A38,A48,A47,A49;
end;
A50: P. (c0 + 0) = aSeq(a,k).0 by A3,A37
.= a:= intloc 0 by A36,AFINSQ_1:35;
A51: for n being Element of 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 Element of NAT;
assume n = 0;
hence
A52: Comput(P,s,n) = s;
thus CurInstr(P,Comput(P,s,n))
= P.IC Comput(P,s,n) by A1,PARTFUN1:def 6
.= a:= intloc 0 by A50,A52,MEMSTR_0:def 12;
thus Comput(P,s,n+1) = Following(P,Comput(P,s,n)) by EXTPRO_1:3
.= Exec(a:= intloc 0,s) by A52,A2,A50,A1,PARTFUN1:def 6;
end;
A53: for n being Nat st Q[n] holds Q[n + 1]
proof
let n be Nat;
assume
A54: Q[n];
assume
A55: n + 1 <= mk+1+1;
per cases;
suppose
A56: n = 0;
hence IC Comput(P,s,n+1)
= Exec(a:= intloc 0,s).IC SCM+FSA by A51
.= (c0 + n)+1 by A2,A56,SCMFSA_2:63
.= c0 + (n + 1);
end;
suppose
A57: n > 0;
A58: n < mk+1+1 by A55,NAT_1:13;
A59: n + 0 <= n + 1 by XREAL_1:7;
A60: CurInstr(P,Comput(P,s,n))
= P. (c0 + n) by A54,A55,A59,A1,PARTFUN1:def 6,XXREAL_0:2
.= SubFrom(a,intloc 0) by A45,A57,A58;
A61: 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 A60;
thus IC Comput(P,s,n+1)
= IC Comput(P,s,n)+1 by A61,SCMFSA_2:65
.= c0 + n + 1 by A54,A55,A59,XXREAL_0:2
.= c0 + (n + 1);
end;
end;
let i be Element of NAT;
assume
A62: i <= len aSeq(a,k);
A63: Q[0] by A2;
for i being Nat holds Q[i] from NAT_1:sch 2(A63,A53);
hence thesis by A37,A62;
end;
hence thesis;
end;
end;
Lm4: for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location,
k being Integer st aSeq(a,k) c= P
for i being Element of NAT st i <= len aSeq(a,k)
holds IC Comput(P,s,i) = i
proof
let s be 0-started State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let a be Int-Location;
let k be Integer;
assume
A1: aSeq(a,k) c= P;
A2: for c being Element of NAT st c < len aSeq(a,k)
holds P.(0+c) = ( aSeq(a,k)). c by A1,AFINSQ_1:86,GRFUNC_1:2;
let i be Element of NAT;
assume i <= len aSeq(a,k);
then IC Comput(P,s,i) = (0+i) by A2,Lm3;
hence thesis;
end;
Lm5: for s being 0-started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for f being
FinSeq-Location, p being FinSequence of INT st f := p c= P
holds P halts_on s
proof
set a2 = intloc 2;
set a1 = intloc 1;
let s be 0-started State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
A1: dom P = NAT by PARTFUN1:def 2;
set D = the InstructionsF of SCM+FSA;
let f be FinSeq-Location;
let p be FinSequence of INT;
set q = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %> ^ aSeq(f,p) ^ Stop
SCM+FSA;
set q0 = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %>;
assume
A2: f := p c= P;
set q = aSeq(a1,len p)^<% f:=<0,...,0>a1 %>^aSeq(f,p)^Stop SCM+FSA;
A3: for i,k being Element of NAT st i < len q
holds P. i = q.(i) by A2,AFINSQ_1:86,GRFUNC_1:2;
consider pp being XFinSequence of D^omega such that
A4: len pp = len p & for k being Nat st k < len pp
ex i being Integer st i = p.(k+1) &
pp.k = (aSeq(a1,k+1) ^ aSeq(a2,i) ^ <% (f,a1):= a2 %>) and
A5: aSeq(f,p) = FlattenSeq pp by SCMFSA_7:def 3;
len q = len (q0 ^ FlattenSeq pp) + 1 by A5,AFINSQ_1:75;
then
A6: 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 Element of NAT st i <= len (q0 ^ FlattenSeq pp0)
holds IC Comput(P,s,i) = i);
A7: for r being XFinSequence, x being object st P[r] holds P[r ^ <% x %>]
proof
let r be XFinSequence;
let x be object;
assume
A8: 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
A9: r1 in dom (r ^ <% x %>) by AFINSQ_1:86;
assume
A10: r ^ <% x %> c= pp;
then
A11: dom (r ^ <% x %>) c= dom pp by GRFUNC_1:2;
then r1 < len pp by A9,AFINSQ_1:86;
then consider pr1 being Integer such that
pr1 = p.(r1+1) and
A12: pp.r1 = aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %> by A4;
r c= r ^ <% x %> by AFINSQ_1:74;
then consider pp0 being XFinSequence of D^omega such that
A13: pp0 = r and
A14: for i being Element of NAT st i <= len (q0 ^ FlattenSeq pp0)
holds IC Comput(P,s,i) = i by A8,A10,XBOOLE_1:1;
set c2 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1));
set c1 = len (q0 ^ FlattenSeq pp0);
IC Comput(P,s,c1) = c1 by A14;
then reconsider s1 = Comput(P,s,c1) as
c1-started State of SCM+FSA by MEMSTR_0:def 12;
A15: x = (r ^ <% x %>).r1 by AFINSQ_1:36
.= pp.r1 by A10,A9,GRFUNC_1:2;
then x in D^omega by A9,A11,FUNCT_1:102;
then reconsider pp1 = pp0 ^ <% x %> as XFinSequence of D^omega;
take pp1;
thus pp1 = r ^ <% x %> by A13;
reconsider x as Element of D^omega by A9,A11,A15,FUNCT_1:102;
A16: FlattenSeq pp1 = FlattenSeq pp0 ^ FlattenSeq <% x %> by AFINSQ_2:75
.= FlattenSeq pp0 ^ x by AFINSQ_2:73;
set s2 = Comput(P,s,c2);
A17: x = aSeq(a1,r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1):=a2 %>)
by A12,A15,AFINSQ_1:27;
then
A18: len q0 + len FlattenSeq pp1 = len q0 + len (FlattenSeq pp0 ^ aSeq(a1,
r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1):=a2 %>)) by A16,AFINSQ_1:27
.= len (q0 ^ (FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1)
:=a2 %>))) by AFINSQ_1:17
.= len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ (aSeq(a2,pr1) ^ <% (f,a1)
:=a2 %>)) by Lm2
.= c2 + len (aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by AFINSQ_1:17
.= c2 + (len aSeq(a2,pr1) + len <% (f,a1):=a2 %>) by AFINSQ_1:17
.= c2 + (len aSeq(a2,pr1) + 1) by AFINSQ_1:34
.= c2 + len aSeq(a2,pr1) + 1;
then
A19: len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(a2,pr1) + 1 by AFINSQ_1:17;
then
A20: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(a2,pr1) by NAT_1:13;
A21: FlattenSeq pp1 c= FlattenSeq pp by A10,A13,AFINSQ_2:82;
A22: 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 A21,A16;
then q0 ^ (FlattenSeq pp0 ^ p) c= q0 ^ FlattenSeq pp by AFINSQ_2:81;
then
A23: q0 ^ FlattenSeq pp0 ^ p c= q0 ^ FlattenSeq pp by AFINSQ_1:27;
q0 ^ FlattenSeq pp c= q by A5,AFINSQ_1:74;
hence q0 ^ FlattenSeq pp0 ^ p c= q by A23;
end;
A24: for c being Element of NAT st c < len aSeq(a1,r1+1)
holds aSeq(a1,r1+1).c = P.(c1 + c)
proof
let c be Element of NAT;
assume c < len aSeq(a1,r1+1);
then
A25: c in dom aSeq(a1,r1+1) by AFINSQ_1:66;
then
A26: c1 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)) by AFINSQ_1:23;
A27: q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) c= q by A17,A22,AFINSQ_1:74;
then
A28: dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)) c= dom q by GRFUNC_1:2;
thus aSeq(a1,r1+1).c = (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1)).(c1 + c)
by A25,AFINSQ_1:def 3
.= q.(c1 + c) by A27,A26,GRFUNC_1:2
.= P. (c1 + c) by A2,A28,A26,GRFUNC_1:2;
end;
set c3 = len (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1));
A29: c2 = c1 + len aSeq(a1,r1+1) by AFINSQ_1:17;
A30: q0 ^ FlattenSeq pp1 = q0 ^ FlattenSeq pp0 ^ x by A16,AFINSQ_1:27;
then len (q0 ^ FlattenSeq pp1) <= len q by A22,NAT_1:43;
then
A31: c2 + len aSeq(a2,pr1) < len q by A19,NAT_1:13;
A32: c3 = c2 + len aSeq(a2,pr1) by AFINSQ_1:17;
A33: Comput(P,s,c2) = Comput(P,s1, len aSeq(a1,r1+1)) by A29,EXTPRO_1:4;
IC Comput(P,s,c2) = c2 by A29,A33,A24,Lm3;
then reconsider s2 as c2-started State of SCM+FSA by MEMSTR_0:def 12;
A34: for c being Element of NAT st c < len aSeq(a2,pr1)
holds aSeq(a2,pr1).c = P.(c2+ c)
proof
let c be Element of NAT;
assume c < len aSeq(a2,pr1);
then
A35: c in dom aSeq(a2,pr1) by AFINSQ_1:66;
then
A36: c2 + c in dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)) by
AFINSQ_1:23;
q0 ^ FlattenSeq pp0 ^ (aSeq(a1,r1+1) ^ aSeq(a2,pr1)) c= q by A12,A15,A22,
AFINSQ_1:74;
then
A37: q0 ^FlattenSeq pp0^aSeq(a1,r1+1) ^ aSeq(a2,pr1) c= q by AFINSQ_1:27;
then
A38: dom (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)) c= dom q by
GRFUNC_1:2;
thus aSeq(a2,pr1).c
= (q0 ^ FlattenSeq pp0 ^ aSeq(a1,r1+1) ^ aSeq(a2,pr1)).(c2 + c)
by A35,AFINSQ_1:def 3
.= q.(c2 + c) by A36,A37,GRFUNC_1:2
.= P. (c2 + c) by A2,A38,A36,GRFUNC_1:2;
end;
A39: now
let i be Element of NAT;
assume i <= len aSeq(a2,pr1);
hence c2 + i = IC Comput(P,s2,i) by A34,Lm3
.= IC Comput(P,s,c2+i) by EXTPRO_1:4;
end;
A40: now
let i be Element of NAT;
assume i <= len aSeq(a1,r1+1);
hence c1 + i = IC Comput(P,s1,i) by A24,Lm3
.= IC Comput(P,s,c1 + i) by EXTPRO_1:4;
end;
A41: for i being Element of NAT st i < len (q0 ^ FlattenSeq pp1) holds IC
Comput(P,s,i) = i
proof
let i be Element of NAT;
assume
A42: i < len (q0 ^ FlattenSeq pp1);
A43: now
A44: i < len q0 + len FlattenSeq pp1 by A42,AFINSQ_1:17;
assume
A45: not i <= c1;
assume not (c1 + 1 <= i & i <= c2);
hence c2 + 1 <= i & i <= c2 + len aSeq(a2,pr1) by A18,A45,A44,NAT_1:13;
end;
per cases by A43;
suppose
i <= len (q0 ^ FlattenSeq pp0);
hence thesis by A14;
end;
suppose
A46: 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 A46,XREAL_1:9;
hence i = IC Comput(P,s,c1+ii) by A29,A40
.= IC Comput(P,s,i);
thus thesis;
end;
suppose
A47: c2 + 1 <= i & i <= c2 + len aSeq(a2,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(a2,pr1) - c2 by A47,XREAL_1:9;
hence i = IC Comput(P,s,c2+ii)by A39
.= IC Comput(P,s,i);
end;
end;
q0 ^ FlattenSeq pp0 ^ x c= q by A22;
then consider rq being XFinSequence of D such that
A48: (q0 ^ FlattenSeq pp0 ^ x)^rq = q by AFINSQ_2:80;
len (q0 ^ FlattenSeq pp1) = c2 + len aSeq(a2,pr1) + 1 by A18,AFINSQ_1:17;
then
A49: len (q0 ^ FlattenSeq pp1) > c2 + len aSeq(a2,pr1) by NAT_1:13;
then
A50: c3 in dom(q0 ^ FlattenSeq pp0 ^ x)
by A30,A32,AFINSQ_1:66;
dom<% (f,a1):=a2 %> = 1 by AFINSQ_1:33;
then
A51: 0 in dom<% (f,a1):=a2 %> by CARD_1:49,TARSKI:def 1;
len<% (f,a1):=a2 %> = 1 by AFINSQ_1:34;
then len(aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>)
= len (aSeq(a1,r1+1) ^ aSeq(a2,pr1)) + 1 by AFINSQ_1:17;
then len (aSeq(a1,r1+1) ^ aSeq(a2,pr1))
< len(aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by XREAL_1:29;
then
A52: len (aSeq(a1,r1+1) ^ aSeq(a2,pr1))
in dom(aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>) by AFINSQ_1:66;
A53: c3 = c1 + len aSeq(a1,r1+1) + len aSeq(a2,pr1) by A29,AFINSQ_1:17;
A54: (P)/.IC Comput(P,s,c3) = P.IC Comput(P,s,c3) by A1,PARTFUN1:def 6;
CurInstr(P,Comput(P,s,c3))
= P. c3 by A32,A41,A54,A49
.= q.(c3 ) by A3,A32,A31
.= (q0 ^ FlattenSeq pp0 ^ x).
(c1 + (len aSeq(a1,r1+1) + (len aSeq(a2,pr1))))
by A53,A50,A48,AFINSQ_1:def 3
.= (q0 ^ FlattenSeq pp0 ^ x).
(c1 + len(aSeq(a1,r1+1) ^ aSeq(a2,pr1))) by AFINSQ_1:17;
then
A55: CurInstr(P,Comput(P,s,c3))
= (aSeq(a1,r1+1) ^ aSeq(a2,pr1) ^ <% (f,a1):=a2 %>).
(len (aSeq(a1,r1+1) ^ aSeq(a2,pr1))+0)
by A52,A12,A15,AFINSQ_1:def 3
.= <% (f,a1):=a2 %>.0 by A51,AFINSQ_1:def 3
.= (f,a1):=a2;
Comput(P,s,c3+1) =
Following(P,Comput(P,s,
c3))
by EXTPRO_1:3
.= Exec((f,a1):=a2, Comput(P,s,c3)) by A55;
then
A56: IC Comput(P,s,len (q0 ^ FlattenSeq pp1)) = Exec((f,a1):=a2,
Comput(P,s,c3)).IC SCM+FSA by A19,AFINSQ_1:17
.= IC Comput(P,s,c3)+1 by SCMFSA_2:73
.= c3+1 by A32,A41,A20;
thus for i being Element of NAT st i <= len (q0 ^ FlattenSeq pp1) holds IC
Comput(P,s,i) = i
proof
let i be Element of NAT;
assume
A57: i <= len (q0 ^ FlattenSeq pp1);
per cases by A57,XXREAL_0:1;
suppose
i < len (q0 ^ FlattenSeq pp1);
hence thesis by A41;
end;
suppose
i = len (q0 ^ FlattenSeq pp1);
hence thesis by A32,A19,A56;
end;
end;
end;
set k = len aSeq(a1,len p);
A58: len q0 = k + 1 by AFINSQ_1:75;
q = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %> ^ (aSeq(f,p) ^ Stop
SCM+FSA) by AFINSQ_1:27
.= aSeq(a1,len p) ^ (<% f :=<0,...,0> a1 %> ^ (aSeq(f,p) ^ Stop
SCM+FSA)) by AFINSQ_1:27;
then
A59: aSeq(a1,len p) c= f:=p by AFINSQ_1:74;
A60: P[{}]
proof
assume {} c= pp;
take <%>(D^omega);
thus <%>(D^omega) = {};
A61: q = aSeq(a1,len p) ^ <% f :=<0,...,0> a1 %> ^ (aSeq(f,p) ^ Stop
SCM+FSA ) by AFINSQ_1:27;
then len q = len q0 + len ((aSeq(f,p) ^ Stop SCM+FSA)) by AFINSQ_1:17;
then len q0 <= len q by NAT_1:11;
then
A62: k < len q by A58,NAT_1:13;
A63: now
let i be Element of NAT;
assume i < len q0;
then i <= len aSeq(a1,len p) by A58,NAT_1:13;
hence IC Comput(P,s,i) = i by A2,A59,Lm4,XBOOLE_1:1;
end;
A64: k < len q0 by A58,NAT_1:13;
then
A65: k in dom q0 by AFINSQ_1:66;
A66: IC Comput(P,s,k) = k by A63,A64;
then
A67: CurInstr(P,Comput(P,s,k))
= P. k by A1,PARTFUN1:def 6
.= q.k by A3,A62
.= q0.k by A61,A65,AFINSQ_1:def 3
.= f:=<0,...,0>a1 by AFINSQ_1:36;
A68: Comput(P,s,len q0) = Following(P,Comput(P,s,k)) by A58,EXTPRO_1:3
.= Exec(f:=<0,...,0>a1, Comput(P,s,k)) by A67;
A69: IC Comput(P,s,len q0)
= IC Comput(P,s,k)+1 by A68,SCMFSA_2:75
.= len q0 by A58,A66;
A70: now
let i be Element of 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 A63,A69;
end;
q0 ^ FlattenSeq <%>(D^omega) = q0 ^ <%>D by AFINSQ_2:74
.= q0 ^ {}
.= q0;
hence thesis by A70;
end;
for r being XFinSequence holds P[r] from AFINSQ_1:sch 3(A60,A7);
then ex pp0 being XFinSequence of D^omega st pp0 = pp &
for i being Element of NAT
st i <= len (q0 ^ FlattenSeq pp0) holds IC Comput(P,s,i) = i;
then IC Comput(P,s,len (q0 ^ FlattenSeq pp)) = len (q0 ^
FlattenSeq pp);
then CurInstr(P,
Comput(P,s,len (q0 ^ FlattenSeq pp)))
= P. len (q0 ^ FlattenSeq pp) by A1,PARTFUN1:def 6
.= q.len (q0 ^ FlattenSeq pp) by A3,A6
.= halt SCM+FSA by A5,AFINSQ_1:36;
hence thesis by EXTPRO_1:29;
end;
registration
let f be FinSeq-Location, p be FinSequence of INT;
cluster f := p -> initial non empty
NAT-defined (the InstructionsF of SCM+FSA)-valued;
coherence;
end;
registration
let f be FinSeq-Location, p be FinSequence of INT;
cluster f := p -> parahalting;
correctness
by Lm5;
end;
theorem
for s being State of SCM+FSA, f being FinSeq-Location, p being
FinSequence of INT holds IExec(f := p,P,s).f = p &
(for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2
holds IExec(f := p,P,s).a = s.a) &
for g being FinSeq-Location st g <> f holds IExec(f := p,P,s).g = s.g
proof
let s be State of SCM+FSA;
let f be FinSeq-Location;
let p be FinSequence of INT;
A1: (s+*Initialize((intloc 0).-->1)).intloc 0
= (Initialize((intloc 0).-->1)).intloc 0 by FUNCT_4:13,SCMFSA_M:10
.= 1 by SCMFSA_M:12;
reconsider s1 = s+*Initialize((intloc 0).-->1)
as 0-started State of SCM+FSA;
A2: (f := p) c= P+*(f:=p) by FUNCT_4:25;
thus IExec(f := p,P,s).f = (Result(P+*(f := p),s1)).f
.= p by A1,A2,SCMFSA_7:7;
hereby
let a be read-write Int-Location;
a <> intloc 0 & a <> IC SCM+FSA by SCMFSA_2:56;
then
A3: not a in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2;
assume
A4: a <> intloc 1 & a <> intloc 2;
thus IExec(f := p,P,s).a
= (Result(P+*(f:=p),s+* Initialize((intloc 0).-->1))).a
.= s1.a by A1,A2,A4,SCMFSA_7:7
.= s.a by A3,FUNCT_4:11;
end;
let g be FinSeq-Location;
assume
A5: g <> f;
g <> intloc 0 & g <> IC SCM+FSA by SCMFSA_2:57,58;
then
A6: not g in dom Initialize((intloc 0).-->1) by SCMFSA_M:11,TARSKI:def 2;
thus IExec(f := p,P,s).g
= (Result(P+*(f:=p),s+*Initialize((intloc 0).-->1))).g
.= s1.g by A1,A2,A5,SCMFSA_7:7
.= s.g by A6,FUNCT_4:11;
end;
definition
let i be Instruction of SCM+FSA;
let a be Int-Location;
pred i refers a means
not for b being Int-Location, l being Nat
for f being FinSeq-Location holds b := a <> i &
AddTo(b,a) <> i & SubFrom(b,a) <> i & MultBy(b,a) <> i & Divide(b,a) <> i &
Divide(a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b :=(f,a) <> i &
(f,b) := a <> i & (f,a):= b <> i & f :=<0,...,0> a <> i;
end;
definition
let I be preProgram of SCM+FSA;
let a be Int-Location;
pred I refers a means
ex i being Instruction of SCM+FSA st i in rng I & i refers a;
end;
definition
let i be Instruction of SCM+FSA;
let a be Int-Location;
pred i destroys a means
not for b being Int-Location for f being
FinSeq-Location holds a := b <> i & AddTo(a,b) <> i & SubFrom(a,b) <> i &
MultBy(a,b) <> i & Divide(a,b) <> i & Divide(b,a) <> i & a :=(f,b) <> i &
a :=len f <> i;
end;
definition
let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function;
let a be Int-Location;
pred I destroys a means
ex i being Instruction of SCM+FSA st i in rng I & i destroys a;
end;
definition
let I be NAT-defined (the InstructionsF of SCM+FSA)-valued Function;
attr I is good means
I does not destroy intloc 0;
end;
theorem
for a being Int-Location holds halt SCM+FSA does not destroy a;
theorem Th6:
for a,b,c being Int-Location holds a <> b implies
b := c does not destroy a
proof
let a,b,c be Int-Location;
assume
A1: a <> b;
now
let e be Int-Location;
let l be Element of NAT;
let f be FinSeq-Location;
thus a := e <> b := c by A1,SF_MASTR:1;
A2: InsCode (b := c) = 1 by SCMFSA_2:18;
hence AddTo(a,e) <> b := c by SCMFSA_2:19;
thus SubFrom(a,e) <> b := c by A2,SCMFSA_2:20;
thus MultBy(a,e) <> b := c by A2,SCMFSA_2:21;
thus Divide(a,e) <> b := c & Divide(e,a) <> b := c by A2,SCMFSA_2:22;
thus a :=(f,e) <> b := c by A2,SCMFSA_2:26;
thus a :=len f <> b := c by A2,SCMFSA_2:28;
end;
hence thesis;
end;
theorem Th7:
for a,b,c being Int-Location holds a <> b implies
AddTo(b,c) does not destroy a
proof
let a,b,c be Int-Location;
assume
A1: a <> b;
now
let e be Int-Location;
let l be Element of NAT;
let f be FinSeq-Location;
A2: InsCode AddTo(b,c) = 2 by SCMFSA_2:19;
hence a := e <> AddTo(b,c) by SCMFSA_2:18;
thus AddTo(a,e) <> AddTo(b,c) by A1,SF_MASTR:2;
thus SubFrom(a,e) <> AddTo(b,c) by A2,SCMFSA_2:20;
thus MultBy(a,e) <> AddTo(b,c) by A2,SCMFSA_2:21;
thus Divide(a,e) <> AddTo(b,c) & Divide(e,a) <> AddTo(b,c) by A2,
SCMFSA_2:22;
thus a :=(f,e) <> AddTo(b,c) by A2,SCMFSA_2:26;
thus a :=len f <> AddTo(b,c) by A2,SCMFSA_2:28;
end;
hence thesis;
end;
theorem Th8:
for a,b,c being Int-Location holds a <> b implies
SubFrom(b,c) does not destroy a
proof
let a,b,c be Int-Location;
assume
A1: a <> b;
now
let e be Int-Location;
let l be Element of NAT;
let f be FinSeq-Location;
A2: InsCode SubFrom(b,c) = 3 by SCMFSA_2:20;
hence a := e <> SubFrom(b,c) by SCMFSA_2:18;
thus AddTo(a,e) <> SubFrom(b,c) by A2,SCMFSA_2:19;
thus SubFrom(a,e) <> SubFrom(b,c) by A1,SF_MASTR:3;
thus MultBy(a,e) <> SubFrom(b,c) by A2,SCMFSA_2:21;
thus Divide(a,e) <> SubFrom(b,c) & Divide(e,a) <> SubFrom(b,c) by A2,
SCMFSA_2:22;
thus a :=(f,e) <> SubFrom(b,c) by A2,SCMFSA_2:26;
thus a :=len f <> SubFrom(b,c) by A2,SCMFSA_2:28;
end;
hence thesis;
end;
theorem
for a,b,c being Int-Location holds a <> b implies
MultBy(b,c) does not destroy a
proof
let a,b,c be Int-Location;
assume
A1: a <> b;
now
let e be Int-Location;
let l be Element of NAT;
let f be FinSeq-Location;
A2: InsCode MultBy(b,c) = 4 by SCMFSA_2:21;
hence a := e <> MultBy(b,c) by SCMFSA_2:18;
thus AddTo(a,e) <> MultBy(b,c) by A2,SCMFSA_2:19;
thus SubFrom(a,e) <> MultBy(b,c) by A2,SCMFSA_2:20;
thus MultBy(a,e) <> MultBy(b,c) by A1,SF_MASTR:4;
thus Divide(a,e) <> MultBy(b,c) & Divide(e,a) <> MultBy(b,c) by A2,
SCMFSA_2:22;
thus a :=(f,e) <> MultBy(b,c) by A2,SCMFSA_2:26;
thus a :=len f <> MultBy(b,c) by A2,SCMFSA_2:28;
end;
hence thesis;
end;
theorem
for a,b,c being Int-Location holds a <> b & a <> c implies
Divide(b,c) does not destroy a
proof
let a,b,c be Int-Location;
assume
A1: a <> b & a <> c;
now
let e be Int-Location;
let l be Element of NAT;
let h be FinSeq-Location;
A2: InsCode Divide(b,c) = 5 by SCMFSA_2:22;
hence a := e <> Divide(b,c) by SCMFSA_2:18;
thus AddTo(a,e) <> Divide(b,c) by A2,SCMFSA_2:19;
thus SubFrom(a,e) <> Divide(b,c) by A2,SCMFSA_2:20;
thus MultBy(a,e) <> Divide(b,c) by A2,SCMFSA_2:21;
thus Divide(e,a) <> Divide(b,c) & Divide(a,e) <> Divide(b,c) by A1,
SF_MASTR:5;
thus a := (h,e) <> Divide(b,c) by A2,SCMFSA_2:26;
thus a :=len h <> Divide(b,c) by A2,SCMFSA_2:28;
end;
hence thesis;
end;
theorem
for a being Int-Location, l being Nat
holds goto l does not destroy a;
theorem
for a,b being Int-Location, l being Nat
holds b =0_goto l does not destroy a;
theorem
for a,b being Int-Location, l being Nat
holds b >0_goto l does not destroy a;
theorem
for a,b,c being Int-Location, f being FinSeq-Location holds a <> b
implies b := (f,c) does not destroy a
proof
let a,b,c be Int-Location;
let f be FinSeq-Location;
assume
A1: a <> b;
now
let e be Int-Location;
let l be Element of NAT;
let h be FinSeq-Location;
A2: InsCode (b := (f,c)) = 9 by SCMFSA_2:26;
hence a := e <> b := (f,c) by SCMFSA_2:18;
thus AddTo(a,e) <> b := (f,c) by A2,SCMFSA_2:19;
thus SubFrom(a,e) <> b := (f,c) by A2,SCMFSA_2:20;
thus MultBy(a,e) <> b := (f,c) by A2,SCMFSA_2:21;
thus Divide(a,e) <> b := (f,c) & Divide(e,a) <> b := (f,c) by A2,
SCMFSA_2:22;
thus a := (h,e) <> b := (f,c) by A1,SF_MASTR:9;
thus a :=len h <> b := (f,c) by A2,SCMFSA_2:28;
end;
hence thesis;
end;
theorem
for a,b,c being Int-Location, f being FinSeq-Location holds
(f,c):= b does not destroy a
proof
let a,b,c be Int-Location;
let f be FinSeq-Location;
now
let e be Int-Location;
let h be FinSeq-Location;
A1: InsCode ((f,c) := b) = 10 by SCMFSA_2:27;
hence a := e <> (f,c) := b by SCMFSA_2:18;
thus AddTo(a,e) <> (f,c) := b by A1,SCMFSA_2:19;
thus SubFrom(a,e) <> (f,c) := b by A1,SCMFSA_2:20;
thus MultBy(a,e) <> (f,c) := b by A1,SCMFSA_2:21;
thus Divide(e,a) <> (f,c) := b & Divide(a,e) <> (f,c) := b by A1,
SCMFSA_2:22;
thus a := (h,e) <> (f,c) := b by A1,SCMFSA_2:26;
thus a :=len h <> (f,c) := b by A1,SCMFSA_2:28;
end;
hence thesis;
end;
theorem
for a,b being Int-Location, f being FinSeq-Location holds a <> b
implies b :=len f does not destroy a
proof
let a,b be Int-Location;
let f be FinSeq-Location;
assume
A1: a <> b;
now
let c be Int-Location;
let g be FinSeq-Location;
A2: InsCode (b :=len f) = 11 by SCMFSA_2:28;
hence a := c <> b :=len f by SCMFSA_2:18;
thus AddTo(a,c) <> b :=len f by A2,SCMFSA_2:19;
thus SubFrom(a,c) <> b :=len f by A2,SCMFSA_2:20;
thus MultBy(a,c) <> b :=len f by A2,SCMFSA_2:21;
thus Divide(a,c) <> b :=len f & Divide(c,a) <> b :=len f by A2,SCMFSA_2:22;
thus a :=(g,c) <> b :=len f by A2,SCMFSA_2:26;
thus a :=len g <> b :=len f by A1,SF_MASTR:11;
end;
hence thesis;
end;
theorem
for a,b being Int-Location, f being FinSeq-Location holds
f:=<0,...,0> b does not destroy a
proof
let a,b be Int-Location;
let f be FinSeq-Location;
now
let e be Int-Location;
let h be FinSeq-Location;
A1: InsCode (f :=<0,...,0> b) = 12 by SCMFSA_2:29;
hence a := e <> f :=<0,...,0> b by SCMFSA_2:18;
thus AddTo(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:19;
thus SubFrom(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:20;
thus MultBy(a,e) <> f :=<0,...,0> b by A1,SCMFSA_2:21;
thus Divide(a,e) <> f :=<0,...,0> b & Divide(e,a) <> f :=<0,...,0> b by A1,
SCMFSA_2:22;
thus a :=(h,e) <> f :=<0,...,0> b by A1,SCMFSA_2:26;
thus a :=len h <> f :=<0,...,0> b by A1,SCMFSA_2:28;
end;
hence thesis;
end;
::$CD
definition
let I be Program of SCM+FSA;
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
pred I is_halting_on s,P means
P +* I halts_on Initialize s;
end;
::$CT
theorem
for I being Program of SCM+FSA
holds I is parahalting iff
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
holds I is_halting_on s,P
proof
set SAt = Start-At(0,SCM+FSA);
let I be Program of SCM+FSA;
thus I is parahalting implies
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
holds I is_halting_on s,P
by FUNCT_4:25;
assume
A1: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
holds I is_halting_on s,P;
let s be 0-started State of SCM+FSA;
A2: Start-At(0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA such that
A3: I c= P;
A4: P = P+*I by A3,FUNCT_4:98;
A5: Initialize s = s by A2,FUNCT_4:98;
I is_halting_on s,P by A1;
hence P halts_on s by A4,A5;
end;
theorem Th19:
for i being Instruction of SCM+FSA, a being Int-Location, s
being State of SCM+FSA st i does not destroy a holds Exec(i,s).a = s.a
proof
let i be Instruction of SCM+FSA;
let a be Int-Location;
let s be State of SCM+FSA;
assume
A1: i does not destroy a;
InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16;
then per cases;
suppose
InsCode i = 0;
then i = halt SCM+FSA by SCMFSA_2:95;
hence thesis by EXTPRO_1:def 3;
end;
suppose
InsCode i = 1;
then consider da,db being Int-Location such that
A2: i = da := db by SCMFSA_2:30;
da <> a by A1,A2;
hence thesis by A2,SCMFSA_2:63;
end;
suppose
InsCode i = 2;
then consider da, db being Int-Location such that
A3: i = AddTo(da,db) by SCMFSA_2:31;
da <> a by A1,A3;
hence thesis by A3,SCMFSA_2:64;
end;
suppose
InsCode i = 3;
then consider da, db being Int-Location such that
A4: i = SubFrom(da, db) by SCMFSA_2:32;
da <> a by A1,A4;
hence thesis by A4,SCMFSA_2:65;
end;
suppose
InsCode i = 4;
then consider da, db being Int-Location such that
A5: i = MultBy(da,db) by SCMFSA_2:33;
da <> a by A1,A5;
hence thesis by A5,SCMFSA_2:66;
end;
suppose
InsCode i = 5;
then consider da, db being Int-Location such that
A6: i = Divide(da, db) by SCMFSA_2:34;
da <> a & db <> a by A1,A6;
hence thesis by A6,SCMFSA_2:67;
end;
suppose
InsCode i = 6;
then ex loc being Nat st i = goto loc by SCMFSA_2:35;
hence thesis by SCMFSA_2:69;
end;
suppose
InsCode i = 7;
then
ex loc being Nat, da being Int-Location st
i = da=0_goto loc by SCMFSA_2:36;
hence thesis by SCMFSA_2:70;
end;
suppose
InsCode i = 8;
then
ex loc being Nat, da being Int-Location st
i = da>0_goto loc by SCMFSA_2:37;
hence thesis by SCMFSA_2:71;
end;
suppose
InsCode i = 9;
then consider db, da being Int-Location, g being FinSeq-Location such that
A7: i = da := (g,db) by SCMFSA_2:38;
da <> a by A1,A7;
hence thesis by A7,SCMFSA_2:72;
end;
suppose
InsCode i = 10;
then ex db, da being Int-Location, g being FinSeq-Location st i = (g,db):=
da by SCMFSA_2:39;
hence thesis by SCMFSA_2:73;
end;
suppose
InsCode i = 11;
then consider da being Int-Location, g being FinSeq-Location such that
A8: i = da :=len g by SCMFSA_2:40;
da <> a by A1,A8;
hence thesis by A8,SCMFSA_2:74;
end;
suppose
InsCode i = 12;
then
ex da being Int-Location, g being FinSeq-Location st i = g :=<0,...,0>
da by SCMFSA_2:41;
hence thesis by SCMFSA_2:75;
end;
end;
theorem Th20:
for s being State of SCM+FSA,
P being Instruction-Sequence of SCM+FSA,
I being really-closed Program of SCM+FSA, a being Int-Location
st I does not destroy a :::& I is_closed_on s,P
for k being Nat holds Comput(P +* I,Initialize s,k).a = s.a
proof
let s be State of SCM+FSA;
let P be Instruction-Sequence of SCM+FSA;
let I be really-closed Program of SCM+FSA;
let a be Int-Location;
assume
A1: I does not destroy a;
defpred P[Nat] means
Comput(P+*I,Initialize s,$1).a = s.a;
A2: I c= P+*I by FUNCT_4:25;
::: assume
:::A3: I is_closed_on s,P;
A3: now
let k be Nat;
assume
A4: P[k];
set l = IC Comput(P+*I,Initialize s,k);
IC Initialize s = 0 by MEMSTR_0:47;
then IC Initialize s in dom I by AFINSQ_1:65;
then
A5: l in dom I by A2,AMISTD_1:21;
then (P+*I).l = I.l by A2,GRFUNC_1:2;
then (P+*I).l in rng I by A5,FUNCT_1:def 3;
then
A6: (P+*I).l does not destroy a by A1;
A7: dom(P+*I) = NAT by PARTFUN1:def 2;
Comput(P+*I,(Initialize s),k + 1).a =
(Following(P+*I,Comput(P+*I,(Initialize s),k))).a
by EXTPRO_1:3
.=(Exec((P+*I).
IC Comput(P+*I,Initialize s,k),
Comput(P+*I,Initialize s,k))).a
by A7,PARTFUN1:def 6
.= Comput(P+*I,s+* Start-At(0,SCM+FSA),k).a by A6,Th19
.= s.a by A4;
hence P[k+1];
end;
A8: not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
Comput(P+*I,Initialize s,0).a = (Initialize s).a
.= s.a by A8,FUNCT_4:11;
then
A9: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A9, A3);
end;
registration
cluster Stop SCM+FSA -> parahalting good;
coherence
proof
thus Stop SCM+FSA is parahalting;
let i be Instruction of SCM+FSA;
A6: rng Stop SCM+FSA = {halt SCM+FSA} by AFINSQ_1:33;
assume i in rng Stop SCM+FSA;
then i = halt SCM+FSA by A6,TARSKI:def 1;
hence i does not destroy intloc 0;
end;
end;
registration
cluster parahalting good halt-ending unique-halt for Program of SCM+FSA;
existence
proof
take Stop SCM+FSA;
thus thesis;
end;
end;
registration
cluster really-closed good -> keeping_0 for Program of SCM+FSA;
correctness
proof
let I be Program of SCM+FSA;
assume
A1: I is really-closed good;
let s be 0-started State of SCM+FSA;
A2: Initialize s = s by MEMSTR_0:44;
let P such that
A3: I c= P;
let k be Nat;
:::A5: I is_closed_on s,P by A1,Th18;
P +* I = P by A3,FUNCT_4:98;
hence Comput(P,s,k).intloc 0 = s.intloc 0 by A1,A2,Th20;
end;
end;
theorem Th21:
for a being Int-Location, k being Integer holds rng aSeq(a,k) c=
{a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)}
proof
let a be Int-Location;
let k be Integer;
let x be object;
assume
A1: x in rng aSeq(a,k);
per cases;
suppose
A2: k > 0 & k = 0 + 1;
then
ex k1 being Nat st k1 + 1 = k & aSeq(a,k) = <% a := intloc
0 %> ^ (k1 --> AddTo(a,intloc 0)) by SCMFSA_7:def 2;
then aSeq(a,k) = <% a := intloc 0 %> ^ {} by A2
.= <% a := intloc 0 %>;
then rng aSeq(a,k) = {a := intloc 0} by AFINSQ_1:33;
then x = a := intloc 0 by A1,TARSKI:def 1;
hence x in {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by
ENUMSET1:def 1;
end;
suppose
A3: k > 0 & k <> 1;
then consider k1 being Nat such that
A4: k1 + 1 = k and
A5: aSeq(a,k) = <% a := intloc 0 %> ^ (k1 --> AddTo(a,intloc 0)) by
SCMFSA_7:def 2;
A6: k1 <> 0 by A3,A4;
rng aSeq(a,k) = rng <% a := intloc 0 %> \/ rng (k1 --> AddTo(a,
intloc 0)) by A5,AFINSQ_1:26
.= {a := intloc 0} \/ rng ( k1 --> AddTo(a,intloc 0)) by AFINSQ_1:33
.= {a := intloc 0} \/ {AddTo(a,intloc 0)} by A6,FUNCOP_1:8;
then x in {a := intloc 0} or x in {AddTo(a,intloc 0)} by A1,
XBOOLE_0:def 3;
then x = a := intloc 0 or x = AddTo(a,intloc 0) by TARSKI:def 1;
hence x in {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by
ENUMSET1:def 1;
end;
suppose
A7: not k > 0;
then consider k1 being Nat such that
A8: k1 + k = 1 and
A9: aSeq(a,k) = <% a := intloc 0 %> ^ (k1 --> SubFrom(a,intloc 0))
by SCMFSA_7:def 2;
A10: k1 <> 0 by A7,A8;
rng aSeq(a,k) = rng <% a := intloc 0 %> \/ rng (k1 --> SubFrom(a,
intloc 0)) by A9,AFINSQ_1:26
.= {a := intloc 0} \/ rng ( k1 --> SubFrom(a,intloc 0)) by AFINSQ_1:33
.= {a := intloc 0} \/ {SubFrom(a,intloc 0)} by A10,FUNCOP_1:8;
then x in {a := intloc 0} or x in {SubFrom(a,intloc 0)} by A1,
XBOOLE_0:def 3;
then x = a := intloc 0 or x = SubFrom(a,intloc 0) by TARSKI:def 1;
hence x in {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)} by
ENUMSET1:def 1;
end;
end;
theorem Th22:
for a being Int-Location, k being Integer holds rng (a := k) c=
{halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0)}
proof
let a be Int-Location;
let k be Integer;
let x be object;
A1: rng aSeq(a,k) c= {a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0 )
} by Th21;
A2: rng (a := k) = rng (aSeq(a,k) ^ Stop SCM+FSA) by SCMFSA_7:1
.= rng aSeq(a,k) \/ rng Stop SCM+FSA by AFINSQ_1:26
.= rng aSeq(a,k) \/ {halt SCM+FSA} by AFINSQ_1:33;
assume x in rng (a := k);
then x in rng aSeq(a,k) or x in {halt SCM+FSA} by A2,XBOOLE_0:def 3;
then
x = a := intloc 0 or x = AddTo(a,intloc 0) or x = SubFrom(a,intloc 0)
or x = halt SCM+FSA by A1,ENUMSET1:def 1,TARSKI:def 1;
hence
x in {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),SubFrom(a,intloc 0
)} by ENUMSET1:def 2;
end;
registration
let a be read-write Int-Location, k be Integer;
cluster a := k -> good;
correctness
proof
now
let i be Instruction of SCM+FSA;
A1: rng (a := k) c= {halt SCM+FSA,a := intloc 0,AddTo(a,intloc 0),
SubFrom(a,intloc 0)} by Th22;
assume
A2: i in rng (a := k);
per cases by A2,A1,ENUMSET1:def 2;
suppose
i = halt SCM+FSA;
hence i does not destroy intloc 0;
end;
suppose
i = a := intloc 0;
hence i does not destroy intloc 0 by Th6;
end;
suppose
i = AddTo(a,intloc 0);
hence i does not destroy intloc 0 by Th7;
end;
suppose
i = SubFrom(a,intloc 0);
hence i does not destroy intloc 0 by Th8;
end;
end;
then a := k does not destroy intloc 0;
hence thesis;
end;
end;
reserve n for Nat;
registration
let a be read-write Int-Location, k be Integer;
cluster a := k -> really-closed;
correctness
proof
per cases;
suppose k > 0;
then consider k1 being Nat such that
k1 + 1 = k and
A1: a := k = <% a:= intloc 0 %> ^ (k1 --> AddTo(a,intloc 0))
^ Stop SCM+FSA by SCMFSA_7:def 1;
defpred P[Nat] means <% a:= intloc 0 %>
^ ($1 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA
is really-closed;
<% a:= intloc 0 %> ^ (0 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA
= <% a:= intloc 0 %> ^ {} ^ Stop SCM+FSA
.= <% a:= intloc 0 %> ^ Stop SCM+FSA
.= Macro(a:= intloc 0);
then <% a:= intloc 0 %> ^ (0 --> AddTo(a,intloc 0)) ^ Stop SCM+FSA
is really-closed;
then
A2: P[0];
A3: for n st P[n] holds P[n+1]
proof let n;
assume
A4: P[n];
set p1 = n --> AddTo(a,intloc 0);
now
per cases;
suppose n is empty;
then p1 is empty;
then <% a:= intloc 0 %> ^ p1 = <% a:= intloc 0 %>;
hence <% a:= intloc 0 %> ^ p1 is halt-free;
end;
suppose
A5: n is non empty;
then p1 is non empty;
then reconsider pp=p1 as Program of SCM+FSA;
rng pp = {AddTo(a,intloc 0)} by A5,FUNCOP_1:8;
then not halt SCM+FSA in rng pp by TARSKI:def 1;
then pp is halt-free by COMPOS_1:def 11;
hence <% a:= intloc 0 %> ^ p1 is halt-free;
end;
end;
then reconsider p = <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0))
as halt-free Program of SCM+FSA;
set m = <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^ Stop SCM+FSA;
m = stop p;
then reconsider m as really-closed MacroInstruction of SCM+FSA by A4;
A7: CutLastLoc m = <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0))
by AFINSQ_2:83;
A8: card CutLastLoc m = card m -' 1 by VALUED_1:65;
<% a:= intloc 0 %> ^ (Segm(n+1) --> AddTo(a,intloc 0)) ^ Stop SCM+FSA
= <% a:= intloc 0 %> ^ ((Segm n --> AddTo(a,intloc 0)) ^
<%AddTo(a,intloc 0)%>) ^ Stop SCM+FSA by AFINSQ_1:87
.= <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^
<%AddTo(a,intloc 0)%> ^ Stop SCM+FSA by AFINSQ_1:27
.= <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^
(<%AddTo(a,intloc 0)%> ^ Stop SCM+FSA) by AFINSQ_1:27
.= <% a:= intloc 0 %> ^ (n --> AddTo(a,intloc 0)) ^
Macro AddTo(a,intloc 0)
.= CutLastLoc m +* Shift(Macro AddTo(a,intloc 0),card m -' 1)
by A7,A8,AFINSQ_1:77
.= CutLastLoc m +*
Shift(Macro IncAddr(AddTo(a,intloc 0),card m -' 1),card m -' 1)
by COMPOS_0:4
.= CutLastLoc m +*
Shift(IncAddr(Macro AddTo(a,intloc 0),card m -' 1),card m -' 1)
by COMPOS_1:74
.= CutLastLoc m +* Reloc(Macro AddTo(a,intloc 0),card m -' 1)
.= m ';' Macro AddTo(a,intloc 0)
.= m ';' AddTo(a,intloc 0);
then <% a:= intloc 0 %>
^ ((n+1) --> AddTo(a,intloc 0)) ^ Stop SCM+FSA
is really-closed;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis by A1;
end;
suppose k <= 0;
then consider k1 being Nat such that
k1 + k = 1 and
A9: a := k = <% a:= intloc 0 %> ^ ( k1 --> SubFrom(a,intloc 0) ) ^
Stop SCM+FSA by SCMFSA_7:def 1;
defpred P[Nat] means <% a:= intloc 0 %>
^ ($1 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA
is really-closed;
<% a:= intloc 0 %> ^ (0 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA
= <% a:= intloc 0 %> ^ {} ^ Stop SCM+FSA
.= <% a:= intloc 0 %> ^ Stop SCM+FSA
.= Macro(a:= intloc 0);
then <% a:= intloc 0 %> ^ (0 --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA
is really-closed;
then
A10: P[0];
A11: for n st P[n] holds P[n+1]
proof let n;
assume
A12: P[n];
set p1 = n --> SubFrom(a,intloc 0);
now
per cases;
suppose n is empty;
then p1 is empty;
then <% a:= intloc 0 %> ^ p1 = <% a:= intloc 0 %>;
hence <% a:= intloc 0 %> ^ p1 is halt-free;
end;
suppose
A13: n is non empty;
then p1 is non empty;
then reconsider pp=p1 as Program of SCM+FSA;
rng pp = {SubFrom(a,intloc 0)} by A13,FUNCOP_1:8;
then not halt SCM+FSA in rng pp by TARSKI:def 1;
then pp is halt-free by COMPOS_1:def 11;
hence <% a:= intloc 0 %> ^ p1 is halt-free;
end;
end;
then reconsider p = <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0))
as halt-free Program of SCM+FSA;
set m = <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA;
m = stop p;
then reconsider m as really-closed MacroInstruction of SCM+FSA by A12;
A15: CutLastLoc m = <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0))
by AFINSQ_2:83;
A16: card CutLastLoc m = card m -' 1 by VALUED_1:65;
<% a:= intloc 0 %> ^ (Segm(n+1) --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA
= <% a:= intloc 0 %> ^ ((Segm n --> SubFrom(a,intloc 0)) ^
<%SubFrom(a,intloc 0)%>) ^ Stop SCM+FSA by AFINSQ_1:87
.= <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^
<%SubFrom(a,intloc 0)%> ^ Stop SCM+FSA by AFINSQ_1:27
.= <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^
(<%SubFrom(a,intloc 0)%> ^ Stop SCM+FSA) by AFINSQ_1:27
.= <% a:= intloc 0 %> ^ (n --> SubFrom(a,intloc 0)) ^
Macro SubFrom(a,intloc 0)
.= CutLastLoc m +* Shift(Macro SubFrom(a,intloc 0),card m -' 1)
by A15,A16,AFINSQ_1:77
.= CutLastLoc m +*
Shift(Macro IncAddr(SubFrom(a,intloc 0),card m -' 1),card m -' 1)
by COMPOS_0:4
.= CutLastLoc m +*
Shift(IncAddr(Macro SubFrom(a,intloc 0),card m -' 1),card m -' 1)
by COMPOS_1:74
.= CutLastLoc m +* Reloc(Macro SubFrom(a,intloc 0),card m -' 1)
.= m ';' Macro SubFrom(a,intloc 0)
.= m ';' SubFrom(a,intloc 0);
then <% a:= intloc 0 %>
^ ((n+1) --> SubFrom(a,intloc 0)) ^ Stop SCM+FSA
is really-closed;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A10,A11);
hence thesis by A9;
end;
end;
end;
registration
let a be read-write Int-Location, k be Integer;
cluster a := k -> keeping_0;
correctness;
end;