:: While Macro Instructions of SCM+FSA
:: by Jing-Chao Chen
::
:: Received December 10, 1997
:: Copyright (c) 1997-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, AMI_1, SCMFSA_2, CARD_1, SCMFSA8B, SCMFSA8A, AMISTD_2,
ARYTM_3, SUBSET_1, FUNCT_4, AMI_3, RELAT_1, TARSKI, XBOOLE_0, NAT_1,
SCMFSA6A, FUNCT_1, XXREAL_0, VALUED_1, CARD_3, ARYTM_1, FSM_1, SF_MASTR,
SCMFSA7B, CIRCUIT2, GRAPHSP, SCMFSA6B, SCMFSA_9, PBOOLE, PARTFUN1,
EXTPRO_1, RELOC, SCMFSA6C, COMPOS_1, MEMSTR_0, AMISTD_1, TURING_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, AFINSQ_1, FUNCOP_1, FUNCT_4, CARD_3,
FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, VALUED_1,
PBOOLE, NAT_1, NAT_D, AMISTD_1, AMISTD_2, SCMFSA_2, SCMFSA6A, SF_MASTR,
SCMFSA6B, SCMFSA7B, SCMFSA8A, SCMFSA8B, XXREAL_0, SCMFSA_M, SCMFSA_X;
constructors XXREAL_0, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA8A, FUNCT_4,
SCMFSA8B, AMISTD_2, RELSET_1, PRE_POLY, PBOOLE, SCMFSA7B, DOMAIN_1,
AMISTD_1, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X, COMPOS_2, NAT_D;
registrations RELSET_1, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SCMFSA6B,
SCMFSA7B, SCMFSA8A, ORDINAL1, VALUED_1, FUNCT_4, VALUED_0, AFINSQ_1,
FUNCOP_1, COMPOS_1, EXTPRO_1, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities SCMFSA6A, COMPOS_1, EXTPRO_1, MEMSTR_0, CARD_3, SF_MASTR, SCMFSA_X,
SCMFSA8B, COMPOS_2;
expansions EXTPRO_1, MEMSTR_0;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_4, SCMFSA_2, SCMFSA6A, GRFUNC_1,
SCMFSA7B, SCMFSA8A, XBOOLE_0, XBOOLE_1, XREAL_1, ORDINAL1, XXREAL_0,
VALUED_1, FUNCOP_1, PBOOLE, AFINSQ_1, PARTFUN1, RELAT_1, COMPOS_1,
EXTPRO_1, MEMSTR_0, CARD_3, SCMFSA_M, FUNCT_7, SCMFSA_X, AMISTD_1,
SCMFSA8C, COMPOS_2;
schemes NAT_1, FUNCT_7;
begin
reserve P,Q for Instruction-Sequence of SCM+FSA;
set SA0= Start-At(0,SCM+FSA);
:: WHILE Statement
reserve m, n for Nat;
::$CD 3
::$CT 17
theorem Th1:
for s being State of SCM+FSA, I being MacroInstruction of SCM+FSA, a
being read-write Int-Location st s.a <> 0
holds while=0(a,I) is_halting_on s,P
proof
let s be State of SCM+FSA;
let I be MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
assume
A1: s.a <> 0;
set i = a =0_goto 3;
set s1 = Initialize s,
P1 = P +* while=0(a,I);
A2: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
A3: IC s1 = IC Start-At(0,SCM+FSA) by A2,FUNCT_4:13
.= 0 by FUNCOP_1:72;
set loc5= card I + 4;
set s5 = Comput(P1,s1,3);
set s4 = Comput(P1,s1,2);
set s2 = Comput(P1,s1,1);
A4: 1 in dom while=0(a,I) by SCMFSA_X:5;
not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
then
A5: s1.a = s.a by FUNCT_4:11;
A6: P1/.IC s1 = P1.IC s1 by PBOOLE:143;
0 in dom while=0(a,I) by AFINSQ_1:65;
then P1. 0 = (while=0(a,I)). 0 by FUNCT_4:13
.= i by SCMFSA_X:10;
then
A7: CurInstr(P1,s1) = i by A3,A6;
A8: Comput(P1,s1,0+1) = Following(P1,Comput(P1,s1,0)) by EXTPRO_1:3
.= Exec(i,s1) by A7;
A9: IC Comput(P1,s1,1) = 0 + 1 by A1,A3,A8,A5,SCMFSA_2:70;
A10: (P1)/.IC Comput(P1,s1,1) = P1.IC Comput(P1,s1,1) by PBOOLE:143;
P1. 1 = (while=0(a,I)). 1 by A4,FUNCT_4:13
.= goto 2 by SCMFSA_X:10;
then
A11: CurInstr(P1,Comput(P1,s1,1)) = goto 2 by A9,A10;
A12: Comput(P1,s1,1+1) = Following(P1,s2) by EXTPRO_1:3
.= Exec(goto 2,s2) by A11;
A13: IC s4 = 2 by A12,SCMFSA_2:69;
A14: 2 in dom while=0(a,I) by SCMFSA_X:5;
A15: loc5 in dom while=0(a,I) by SCMFSA_X:6;
A16: P1/.IC s4 = P1.IC s4 by PBOOLE:143;
P1.2 = (while=0(a,I)).2 by A14,FUNCT_4:13
.= goto loc5 by SCMFSA_X:12;
then
A17: CurInstr(P1,s4) = goto loc5 by A13,A16;
A18: Comput(P1,s1,2+1) = Following(P1,s4) by EXTPRO_1:3
.= Exec(goto loc5,s4) by A17;
A19: IC s5 = loc5 by A18,SCMFSA_2:69;
A20: P1/.IC s5 = P1.IC s5 by PBOOLE:143;
P1.loc5 = (while=0(a,I)).loc5 by A15,FUNCT_4:13
.= halt SCM+FSA by SCMFSA_X:11;
then
CurInstr(P1,s5) = halt SCM+FSA by A19,A20;
then P1 halts_on s1 by EXTPRO_1:29;
hence while=0(a,I) is_halting_on s,P by SCMFSA7B:def 7;
thus thesis;
end;
theorem Th2:
for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA,
s being State of SCM+FSA,k being Nat
st I is_halting_on s,P
& k < LifeSpan(P +* I,Initialize s) &
IC Comput(P +* while=0(a,I),(Initialize s),1+k)
= IC Comput(P +* I, (Initialize s),k) + 3 &
DataPart Comput(P +* while=0(a,I),(Initialize s),1+k)
= DataPart Comput(P +* I,(Initialize s),k)
holds IC Comput(P +* while=0(a,I),(Initialize s),1+k+1) = IC
Comput(P +* I, (Initialize s),k+1) + 3 &
DataPart Comput(P +* while=0(a,I),(Initialize s),1+k+1) =
DataPart Comput(P +* I, (Initialize s),k+1)
proof
::: set J3= Goto 0 ";" Stop SCM+FSA;
set J = Stop SCM+FSA;
let a be Int-Location;
set D = Int-Locations \/ FinSeq-Locations;
let I be really-closed MacroInstruction of SCM+FSA;
let s be State of SCM+FSA;
let k be Nat;
set s1 = Initialize s,
P1 = P +* while=0(a,I);
set sI = Initialize s,
PI = P +* I;
A1: I c= PI by FUNCT_4:25;
set sK1= Comput(P1, s1,1+k);
set sK2= Comput(PI, sI,k);
set l3=IC Comput(PI, sI,k);
set I1= I ';' goto 0;
set i = a =0_goto 3;
reconsider n = l3 as Element of NAT;
set Mi= i ";" Goto (card I1 + 1);
set J2= I1 ";" Stop SCM+FSA;
A2: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
A3: I c= PI by FUNCT_4:25;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom I by AFINSQ_1:65;
then
A4: n in dom I by AMISTD_1:21,A3;
then n < card I by AFINSQ_1:66;
then
A5: n+3 < card I+ 5 by XREAL_1:8;
A6: PI/.IC sK2 = PI.IC sK2 by PBOOLE:143;
A7: CurInstr(PI,sK2) = I. n by A4,A1,GRFUNC_1:2,A6;
assume I is_halting_on s,P;
then
A8: PI halts_on sI by SCMFSA7B:def 7;
assume k < LifeSpan(PI,sI);
then
I. n <> halt SCM+FSA by A7,A8,EXTPRO_1:def 15;
then
A9: n <> LastLoc I by COMPOS_1:def 14;
n <= LastLoc I by A4,VALUED_1:32;
then
A10: n < LastLoc I by A9,XXREAL_0:1;
then
A11: n in dom CutLastLoc I by COMPOS_2:26;
dom I c= dom I1 by COMPOS_1:21;
then
A12: n in dom I1 by A4;
dom I1 = dom CutLastLoc I \/ dom Reloc(Macro goto 0, card I -' 1)
by FUNCT_4:def 1;
then
A13: dom CutLastLoc I c= dom I1 by XBOOLE_1:7;
A14: dom CutLastLoc I misses dom Reloc(Macro goto 0, card I -' 1)
by COMPOS_1:18;
A15: n in dom I1 by A11,A13;
dom I c= dom I1 by COMPOS_1:21;
then LastLoc I <= LastLoc I1 by VALUED_1:68;
then n < LastLoc I1 by A10,XXREAL_0:2;
then
A16: I1.n <> halt SCM+FSA by A15,COMPOS_1:def 15;
dom I1 c= dom J2 by SCMFSA6A:17;
then
A17: n in dom J2 by A12;
then n + 3 in { il+3 where il is Nat: il in dom J2};
then
A18: n+3 in dom Shift(J2,3) by VALUED_1:def 12;
then
A19: Shift(J2,3)/.(n+3) =Shift(J2,3).( n +3) by PARTFUN1:def 6
.=J2. n by A17,VALUED_1:def 12
.= I1.n by A16,A15,SCMFSA6A:15
.=(CutLastLoc I). n by A11,FUNCT_4:16,A14
.=I.n by A10,COMPOS_2:27;
card while=0(a,I) = card I + 5 by SCMFSA_X:3;
then
A20: n+3 in dom while=0(a,I) by A5,AFINSQ_1:66;
I. n in rng I by A4,FUNCT_1:def 3;
then reconsider j = I. n as Instruction of SCM+FSA by A2;
A21: card Mi = card Macro i + card Goto (card I1 + 1) by SCMFSA6A:21
.= card Macro i + 1 by SCMFSA8A:15
.= 2 + 1 by COMPOS_1:56
.= 3;
then n+3 >= card Mi by NAT_1:11;
then
A22: not n+3 in dom Mi by AFINSQ_1:66;
A23: Comput(PI, sI,k+1) = Following(PI,sK2) by EXTPRO_1:3
.= Exec(j,sK2) by A7;
assume
A24: IC Comput(P1, s1,1+k)=l3 + 3;
:::B3: n < LastLoc I by B4,XXREAL_0:1;
n + 3 < LastLoc I + 3 by A10,XREAL_1:6;
then
A25: n + 3 <> card I - 1 + 3 by AFINSQ_1:91;
dom while=0(a,I) = dom if=0(a,I1) by FUNCT_7:30;
then
A26: n+3 in dom if=0(a,I1) by A20;
A27: if=0(a,I1) = Mi ";" J2 by SCMFSA6A:25;
then
dom if=0(a,I1) = dom Mi \/ dom Reloc(J2, 3) by SCMFSA6A:39,A21;
then
A28: (n+3) in dom Reloc(J2, 3) by A26,A22,XBOOLE_0:def 3;
A29: (P1)/.IC sK1 = P1.IC sK1 by PBOOLE:143;
A30: Reloc(J2,3) = IncAddr(Shift(J2,3),3) by COMPOS_1:34;
P1. (n+3) = (while=0(a,I)). (n+3) by A20,FUNCT_4:13
.= (Mi ";" J2). (n+3) by A27,FUNCT_7:32,A25
.= (Reloc(J2,3)).(n+3) by A28,SCMFSA6A:40,A21
.= IncAddr(j,3) by A18,A19,A30,COMPOS_1:def 21;
then
A31: CurInstr(P1,sK1) =IncAddr(j,3) by A24,A29;
assume
A32: DataPart sK1 = DataPart sK2;
Comput(P1, s1,1+k+1) = Following(P1,sK1) by EXTPRO_1:3
.= Exec(IncAddr(j,3),sK1) by A31;
hence thesis by A24,A32,A23,SCMFSA6A:8;
end;
:: Twierdzeinie zmienia znaczenie, jezeli w oryginale mowilo
:: ze znajdziemy sie w miejscu "przed powrotem" i wykonujemy Next
:: to w tym miejscu jest teraz powrot i wykonujemy goto 0
theorem Th3:
for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA,
s being State of SCM+FSA st I is_halting_on s,P &
IC Comput(P +* while=0(a,I), Initialize s,1 + LifeSpan(P +* I,Initialize s) )
= IC Comput(P +* I,Initialize s,LifeSpan(P +* I,Initialize s) ) + 3
holds CurInstr(P +* while=0(a,I),
Comput(P +* while=0(a,I),Initialize s,
(1 + LifeSpan(P +* I,Initialize s)))) = goto 0
proof
set J3= Goto 0 ";" Stop SCM+FSA;
set J = Stop SCM+FSA;
let a be Int-Location;
let I be really-closed MacroInstruction of SCM+FSA;
let s be State of SCM+FSA;
set s1 = Initialize s,
P1 = P +* while=0(a,I);
set sI = Initialize s,
PI = P +* I;
A1: I c= PI by FUNCT_4:25;
set life=LifeSpan(P +* I,Initialize s);
set sK1= Comput(P1, s1,1+life);
set sK2= Comput(PI, sI,life);
set I1= I ';' goto 0;
set i = a =0_goto 3;
reconsider n = IC sK2 as Element of NAT;
set Mi= i ";" Goto (card I1 + 1);
set J2= I1 ";" Stop SCM+FSA;
A2: I c= PI by FUNCT_4:25;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom I by AFINSQ_1:65;
then
A3: n in dom I by AMISTD_1:21,A2;
then n < card I by AFINSQ_1:66;
then
A4: n+3 < card I+ 5 by XREAL_1:8;
assume I is_halting_on s,P;
then
A5: PI halts_on sI by SCMFSA7B:def 7;
A6: (PI)/.IC sK2 = PI.IC sK2 by PBOOLE:143;
A7: (P1)/.IC sK1 = P1.IC sK1 by PBOOLE:143;
assume
A8: IC sK1 = IC sK2 + 3;
CurInstr(PI,sK2) = I. n by A3,A1,GRFUNC_1:2,A6;
then
A9: I.IC sK2 = halt SCM+FSA by A5,EXTPRO_1:def 15;
IC sK2 = LastLoc I by A3,A9,COMPOS_1:def 15
.= card I - 1 by AFINSQ_1:91;
then
A10: IC sK2 + 3 = card I + 2;
card while=0(a,I) = card I + 5 by SCMFSA_X:3;
then
A11: n+3 in dom while=0(a,I) by A4,AFINSQ_1:66;
A12: n+3 in dom if=0(a,I1) by A11,FUNCT_7:30;
P1. (n+3) = (while=0(a,I)). (n+3) by FUNCT_4:13,A11
.= (while=0(a,I)).(card I + 2) by A10
.= goto 0 by FUNCT_7:31,A10,A12;
hence thesis by A8,A7;
end;
reserve f for FinSeq-Location,
c for Int-Location;
::$CT
theorem Th4:
for s being State of SCM+FSA,
I being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location
st I is_halting_on s,P & s.a =0
holds IC Comput(P +* while=0(a,I), Initialize s,
(LifeSpan(P +* I,Initialize s) + 2)) = 0 &
for k being Nat st k
<= LifeSpan(P +* I,Initialize s) + 2
holds IC Comput(P +* while=0(a,I),
(Initialize s),k) in dom while=0(a,I)
proof
set D = Int-Locations \/ FinSeq-Locations;
let s be State of SCM+FSA;
let I be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set sI = Initialize s,
PI = P +* I;
set s1 = Initialize s,
P1 = P +* while=0(a,I);
defpred P[Nat] means $1 <= LifeSpan(PI,sI) implies IC Comput(
P1, s1
,1+$1) = IC Comput(PI, sI,$1)+ 3 & DataPart Comput(P1, s1,1+$1) = DataPart
Comput(PI, sI,$1);
assume
A1: I is_halting_on s,P;
A2: now
let k be Nat;
assume
A3: P[k];
now
A4: k + 0 < k + 1 by XREAL_1:6;
assume k + 1 <= LifeSpan(PI,sI);
then k < LifeSpan(PI,sI) by A4,XXREAL_0:2;
hence IC Comput(P1, s1,1+k+1) = IC Comput(PI,sI,k+1) + 3 &
DataPart Comput(P1, s1,1+k+1) = DataPart Comput(PI, sI,k+1)
by A1,A3,Th2;
end;
hence P[k + 1];
end;
reconsider l=LifeSpan(PI,sI) as Element of NAT by ORDINAL1:def 12;
set loc4= (card I + 3);
set i = a =0_goto 3;
set s2 = Comput(P1,s1,1);
IC SCM+FSA in dom (Start-At(0,SCM+FSA)) by MEMSTR_0:15;
then
A5: IC s1 = IC(Start-At(0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72;
not a in dom (Start-At(0,SCM+FSA)) by SCMFSA_2:102;
then
A6: s1.a = s.a by FUNCT_4:11;
assume
A7: s.a = 0;
A8: 0 in dom while=0(a,I) by AFINSQ_1:65;
A9: (P1)/.IC s1 = P1.IC s1 by PBOOLE:143;
P1. 0 = while=0(a,I). 0 by A8,FUNCT_4:13
.= i by SCMFSA_X:10;
then
A10: CurInstr(P1,s1) = i by A5,A9;
A11: Comput(P1,s1,0+1) = Following(P1,Comput(P1,s1,0)) by EXTPRO_1:3
.= Exec(i,s1) by A10;
then ( for c holds s2.c = s1.c)& for f holds s2.f = s1.f by SCMFSA_2:70;
then
A12: DataPart s2 = DataPart sI by SCMFSA_M:2;
A13: IC s2 = 3 by A7,A11,A6,SCMFSA_2:70;
A14: P[ 0]
proof
assume 0 <= LifeSpan(PI,sI);
A15: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
IC Comput(PI, sI,0)
= IC Start-At(0,SCM+FSA) by A15,FUNCT_4:13
.= 0 by FUNCOP_1:72;
hence thesis by A13,A12;
end;
A16: for k being Nat holds P[k] from NAT_1:sch 2(A14,A2);
set s4= Comput(P1, s1,1+LifeSpan(PI,sI)+1);
set s3= Comput(P1, s1,1+LifeSpan(PI,sI));
set s2= Comput(P1, s1,1+LifeSpan(PI,sI));
P[l] by A16;
then
A17: CurInstr(P1,s2) = goto 0 by A1,Th3;
A18: CurInstr(P1,s3) = goto 0 by A17;
A19: s4 = Following(P1,s3) by EXTPRO_1:3
.= Exec(goto 0,s3) by A18;
A20: IC s4 = 0 by A19,SCMFSA_2:69;
hence IC Comput(P1, s1,LifeSpan(PI,sI)+2) = 0;
A21: now
let k be Nat;
assume
A22: k <= LifeSpan(PI,sI)+2;
assume k<>0;
then consider n being Nat such that
A23: k = n+ 1 by NAT_1:6;
k<=LifeSpan(PI,sI)+1 or k >= LifeSpan(PI,sI)+1+1 by NAT_1:13;
then
A24: k <=LifeSpan(PI,sI)+1 or k = LifeSpan(PI,sI)+2 by A22,XXREAL_0:1;
reconsider n as Element of NAT by ORDINAL1:def 12;
per cases by A24;
suppose
k<=LifeSpan(PI,sI)+1;
then n <= LifeSpan(PI,sI) by A23,XREAL_1:6;
then
A25: IC Comput(P1,s1,1+n) = IC Comput(PI, sI,n) + 3
by A16;
reconsider m = IC Comput(PI, sI,n) as Element of NAT;
A26: I c= PI by FUNCT_4:25;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom I by AFINSQ_1:65;
then m in dom I by AMISTD_1:21,A26;
then m < card I by AFINSQ_1:66;
then
A27: m+3 < card I+ 5 by XREAL_1:8;
card while=0(a,I) = card I + 5 by SCMFSA_X:3;
hence IC Comput(P1,s1,k) in dom while=0(a,I) by A23,A25,A27,AFINSQ_1:66;
end;
suppose
k >= LifeSpan(PI,sI)+2;
then k = LifeSpan(PI,sI)+2 by A22,XXREAL_0:1;
hence IC Comput(P1,s1,k) in dom while=0(a,I) by A20,AFINSQ_1:65;
end;
end;
now
let k be Nat;
assume
A28: k <= LifeSpan(PI,sI)+2;
per cases;
suppose
k = 0;
hence IC Comput(P1,s1,k) in dom while=0(a,I) by A8,A5;
end;
suppose
k <>0;
hence IC Comput(P1,s1,k) in dom while=0(a,I) by A21,A28;
end;
end;
hence thesis;
end;
reserve s for State of SCM+FSA,
I for MacroInstruction of SCM+FSA,
a for read-write Int-Location;
definition
let s,I,a,P;
deffunc U(Nat,State of SCM+FSA) =
Comput(P +* while=0(a,I), Initialize $2,
LifeSpan(P +* while=0(a,I) +* I,Initialize $2) + 2);
deffunc V(Nat,State of SCM+FSA) = down U($1,$2);
func StepWhile=0(a,I,P,s) ->
sequence of product the_Values_of SCM+FSA means
:Def1:
it.0 = s &
for i being Nat holds
it.(i+1)= Comput(P +* while=0(a,I), Initialize(it.i),
LifeSpan(P +* while=0(a,I) +* I, Initialize(it.i)) + 2);
existence
proof
reconsider ss=s as
Element of product the_Values_of SCM+FSA by CARD_3:107;
consider f being sequence of product the_Values_of SCM+FSA
such that
A1: f.0 = ss and
A2: for i being Nat holds f.(i+1)= V(i,f.i) from NAT_1:sch 12;
take f;
thus f.0 = s by A1;
let i be Nat;
f.(i+1)= V(i,f.i) by A2;
hence thesis;
end;
uniqueness
proof
let F1,F2 be sequence of product the_Values_of SCM+FSA such that
A3: F1.0 = s and
A4: for i being Nat holds F1.(i+1)= U(i,F1.i) and
A5: F2.0 = s and
A6: for i being Nat holds F2.(i+1)= U(i,F2.i);
reconsider s as Element of product the_Values_of SCM+FSA by CARD_3:107;
A7: F1.0 = s by A3;
A8: for i being Nat holds F1.(i+1)= V(i,F1.i) by A4;
A9: F2.0 = s by A5;
A10: for i being Nat holds F2.(i+1)= V(i,F2.i) by A6;
thus F1 = F2 from NAT_1:sch 16(A7,A8,A9,A10);
end;
end;
reserve i,k,m,n for Nat;
theorem Th5:
StepWhile=0(a,I,P,s).(k+1)=StepWhile=0(a,I,P,StepWhile=0(a,I,P,s).k).1
proof
set sk=StepWhile=0(a,I,P,s).k;
set sk0=StepWhile=0(a,I,P,sk).0;
sk0=sk by Def1;
hence
StepWhile=0(a,I,P,s).(k+1) = Comput(P +*while=0(a,I), Initialize sk0,
(LifeSpan(P +*while=0(a,I) +* I,Initialize sk0) + 2)) by Def1
.=StepWhile=0(a,I,P,sk).(0+1) by Def1
.=StepWhile=0(a,I,P,sk).1;
end;
::$CT
theorem Th6:
for I being MacroInstruction of SCM+FSA,a being read-write Int-Location,
s being State of SCM+FSA holds StepWhile=0(a,I,P,s).1
= Comput(P +* while=0(a,I),Initialize s,
LifeSpan(P +* while=0(a,I)+* I,Initialize s) + 2)
proof
let I be MacroInstruction of SCM+FSA,a be read-write Int-Location,
s be State of SCM+FSA;
A1: StepWhile=0(a,I,P,s).0 = s by Def1;
thus StepWhile=0(a,I,P,s).1
= StepWhile=0(a,I,P,s).(0+1)
.= Comput(P +* while=0(a,I), Initialize s,
LifeSpan(P +* while=0(a,I)+* I,Initialize s) + 2) by A1,Def1;
end;
theorem Th7:
for I being MacroInstruction of SCM+FSA,a being read-write Int-Location,
s being State of SCM+FSA,k,n being Nat
st IC StepWhile=0(a,I,P,s).k = 0 &
StepWhile=0(a,I,P,s).k= Comput(P +* while=0(a,I),
(Initialize s),n)
holds StepWhile=0(a,I,P,s).k = Initialize(StepWhile=0(a,I,P,s).k) &
StepWhile=0(a,I,P,s).(k+1)=Comput(P +* while=0(a,I), Initialize s,
(n +(LifeSpan(P +* while=0(a,I) +* I,
Initialize(StepWhile=0(a,I,P,s).k)) + 2)))
proof
set D = Int-Locations \/ FinSeq-Locations;
let I be MacroInstruction of SCM+FSA,a be read-write Int-Location,
s be State of SCM+FSA,k,n be Nat;
set s1 = Initialize s,
P1 = P +* while=0(a,I);
set sk=StepWhile=0(a,I,P,s).k;
set s2=Initialize sk;
assume
A1: IC sk = 0;
assume
A2: sk = Comput(P1, s1,n);
sk is 0-started by A1;
then Start-At(0,SCM+FSA) c= sk by MEMSTR_0:29;
hence s2=sk by FUNCT_4:98;
hence
StepWhile=0(a,I,P,s).(k+1)
= Comput(P1, sk,LifeSpan(P +* while=0(a,I) +* I,
Initialize sk) + 2)
by Def1
.= Comput(P1, s1,n +(LifeSpan(P +* while=0(a,I) +* I,
Initialize sk) + 2))
by A2,EXTPRO_1:4;
end;
theorem Th8:
for I being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location, s being State of SCM+FSA st
(for k being Nat holds
I is_halting_on StepWhile=0(a,I,P,s).k,P+*while=0(a,I)) &
ex f being Function of
product the_Values_of SCM+FSA,NAT st
for k being Nat holds
((f.(StepWhile=0(a,I,P,s).(k+1)) < f.(StepWhile=0(a,I,P,s).k) or
f.(StepWhile=0(a,I,P,s).k) = 0) &
(f.(StepWhile=0(a,I,P,s).k)=0 iff (StepWhile=0(a,I,P,s).k).a <> 0))
holds while=0(a,I) is_halting_on s,P
proof
let I be really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location, s be State of
SCM+FSA;
assume
A1: for k being Nat holds
I is_halting_on StepWhile=0(a,I,P,s).k,P+*while=0(a,I);
set s1 = Initialize s,
P1 = P +* while=0(a,I);
A2: P1 +* while=0(a,I) = P1;
given f being Function of product the_Values_of SCM+FSA,NAT such that
A3: for k being Nat
holds (f.(StepWhile=0(a,I,P,s).(k+1)) < f.(StepWhile=0(a,I,P,s).k) or
f.(StepWhile=0(a,I,P,s).k) = 0) &
( f.(StepWhile=0(a,I,P,s).k)=0 iff
(StepWhile=0(a,I,P,s).k).a <> 0 );
deffunc F(Nat) = f.(StepWhile=0(a,I,P,s).$1);
A4: for k being Nat holds ( F(k+1) < F(k) or F(k) = 0 ) by A3;
consider m being Nat such that
A5: F(m)=0 and
A6: for n being Nat st F(n) =0 holds m <= n from NAT_1:sch 17(A4);
defpred P[Nat] means $1+1 <= m implies ex k st StepWhile=0(a,I,P,s)
.($1+1)= Comput(P1, s1,k);
A7: now
let k be Nat;
assume
A8: P[k];
now
set sk1=StepWhile=0(a,I,P,s).(k+1);
set sk=StepWhile=0(a,I,P,s).k;
assume
A9: (k+1)+ 1 <= m;
k + 0 < k+ (1+ 1) by XREAL_1:6;
then k < m by A9,XXREAL_0:2;
then F(k) <> 0 by A6;
then
A10: sk.a = 0 by A3;
A11: I is_halting_on sk,P+*while=0(a,I) by A1;
(k+1)+ 0 < (k+ 1)+ 1 by XREAL_1:6;
then consider n being Nat such that
A12: sk1 = Comput(P1, s1,n) by A8,A9,XXREAL_0:2;
take m=n +(LifeSpan(P +* while=0(a,I) +* I,
Initialize sk1) + 2);
A13: P+*while=0(a,I) +* while=0(a,I) = P+*while=0(a,I);
sk1= Comput(P +* while=0(a,I), Initialize sk,
(LifeSpan(P +* while=0(a,I) +* I,Initialize sk) + 2)) by Def1;
then IC sk1 = 0 by A11,A10,Th4,A13;
hence StepWhile=0(a,I,P,s).((k+1)+1)= Comput(P1, s1,m) by A12,Th7;
end;
hence P[k+1];
end;
A14: P[ 0]
proof
assume 0+1 <= m;
take n=(LifeSpan(P +* while=0(a,I)+* I,Initialize s) + 2);
thus thesis by Th6;
end;
A15: for k being Nat holds P[k] from NAT_1:sch 2(A14,A7);
now
per cases;
suppose
m=0;
then (StepWhile=0(a,I,P,s).0).a <> 0 by A3,A5;
then s.a <> 0 by Def1;
hence thesis by Th1;
end;
suppose
m<>0;
then consider i being Nat such that
A16: m=i+1 by NAT_1:6;
reconsider m,i as Element of NAT by ORDINAL1:def 12;
set sm=StepWhile=0(a,I,P,s).m;
set si=StepWhile=0(a,I,P,s).i;
i < m by A16,NAT_1:13;
then F(i) <> 0 by A6;
then
A17: si.a = 0 by A3;
A18: I is_halting_on si,P+*while=0(a,I) by A1;
sm= Comput(P +* while=0(a,I), (Initialize si),
(LifeSpan(P +* while=0(a,I) +* I,Initialize si) + 2))
by A16,Def1;
then sm is 0-started by A18,A17,Th4,A2;
then
A19: Start-At(0,SCM+FSA) c= sm by MEMSTR_0:29;
set p=(LifeSpan(P+*while=0(a,I)+* I,Initialize s) + 3);
set sm1=Initialize sm;
consider n being Nat such that
A20: sm = Comput(P1, s1,n) by A15,A16;
A21: sm1=sm by A19,FUNCT_4:98;
sm.a <> 0 by A3,A5;
then while=0(a,I) is_halting_on sm,P by Th1;
then P +* while=0(a,I) halts_on Initialize sm by SCMFSA7B:def 7;
then P +* while=0(a,I) halts_on Initialize sm;
then P1 halts_on sm1;
then consider j being Nat such that
A22: CurInstr(P1,Comput(P1,sm,j))
= halt SCM+FSA by A21;
A23: Comput(P1,s1,n+j)
= Comput(P1,Comput(P1,s1,n),j) by EXTPRO_1:4;
CurInstr(P1,Comput(P1,s1,n+j))
= halt SCM+FSA by A20,A22,A23;
then P1 halts_on s1 by EXTPRO_1:29;
hence while=0(a,I) is_halting_on s,P by SCMFSA7B:def 7;
end;
end;
hence thesis;
end;
theorem Th9:
for I being parahalting really-closed MacroInstruction of SCM+FSA,
a being read-write
Int-Location, s being State of SCM+FSA st
ex f being Function of product the_Values_of SCM+FSA,NAT st
for k being Nat
holds (f.(StepWhile=0(a,I,P,s).(k+1)) < f.(StepWhile=0(a,I,P,s).k)
or f.(StepWhile=0(a,I,P,s).k) = 0) &
(f.(StepWhile=0(a,I,P,s).k)=0 iff (StepWhile=0(a,I,P,s).k).a <> 0 )
holds while=0(a,I) is_halting_on s,P
proof
let I be parahalting really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location,s be State of SCM+FSA;
A1: for k being Nat holds
I is_halting_on StepWhile=0(a,I,P,s).k,P+*while=0(a,I)
by SCMFSA7B:19;
assume ex f being Function of product the_Values_of SCM+FSA,NAT st for
k being Nat holds (f.(StepWhile=0(a,I,P,s).(k+1)) < f.(StepWhile=0(a,I,P,s).k)
or f
.(StepWhile=0(a,I,P,s).k) = 0) & ( f.(StepWhile=0(a,I,P,s).k)=0
iff (StepWhile=0(a,I,P,s).k).a <> 0 );
hence thesis by A1,Th8;
end;
theorem
for I being parahalting really-closed MacroInstruction of SCM+FSA,
a being read-write
Int-Location st ex f being Function of product the_Values_of SCM+FSA,NAT
st (for s being State of SCM+FSA,P
holds (f.(StepWhile=0(a,I,P,s).1) < f.s
or f.s =
0) & ( f.s =0 iff s.a <> 0 )) holds while=0(a,I) is parahalting
proof
let I be parahalting really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location;
given f being Function of product the_Values_of SCM+FSA,NAT such that
A1: for s being State of SCM+FSA,P holds (f.(StepWhile=0(a,I,P,s).1) < f.s
or f.s = 0) & ( f.s =0 iff s.a <> 0 );
now let t be State of SCM+FSA;
let Q;
now
let k be Nat;
f.(StepWhile=0(a,I,Q,StepWhile=0(a,I,Q,t).k).1)
< f.(StepWhile=0(a,I,Q,t).
k) or f.(StepWhile=0(a,I,Q,t).k) = 0 by A1;
hence (f.(StepWhile=0(a,I,Q,t).(k+1)) < f.(StepWhile=0(a,I,Q,t).k)
or f.(StepWhile=0(a,I,Q,t).k) = 0) &
(f.(StepWhile=0(a,I,Q,t).k)=0 iff (StepWhile=0(a,I,Q,t).k).a <> 0 )
by A1,Th5;
end;
hence while=0(a,I) is_halting_on t,Q by Th9;
end;
hence thesis by SCMFSA7B:19;
end;
::$CT
theorem Th11:
for i being Instruction of SCM+FSA st i does not destroy intloc
0 holds Macro i is good
proof
let i be Instruction of SCM+FSA;
set I=Macro i;
A1: rng I = {i,halt SCM+FSA} by COMPOS_1:67;
assume
A2: i does not destroy intloc 0;
now
let x be Instruction of SCM+FSA;
assume
A3: x in rng I;
per cases by A1,A3,TARSKI:def 2;
suppose
x = i;
hence x does not destroy intloc 0 by A2;
end;
suppose
x = halt SCM+FSA;
hence x does not destroy intloc 0 by SCMFSA7B:5;
end;
end;
then I does not destroy intloc 0 by SCMFSA7B:def 4;
hence thesis by SCMFSA7B:def 5;
end;
registration
let I,J be good MacroInstruction of SCM+FSA,a be Int-Location;
cluster if=0(a,I,J) -> good;
correctness
proof
set i = a =0_goto (card J + 3);
reconsider Mi=Macro i as good Program of SCM+FSA by Th11,SCMFSA7B:12;
if=0(a,I,J) = Mi ";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
hence thesis;
end;
end;
registration
let I be good MacroInstruction of SCM+FSA,a be Int-Location;
cluster if=0(a,I) -> good;
correctness
proof
set i = a =0_goto 3;
reconsider Mi=Macro i as good Program of SCM+FSA by Th11,SCMFSA7B:12;
if=0(a,I)
= Mi ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
hence thesis;
end;
end;
registration
let I be good MacroInstruction of SCM+FSA,a be Int-Location;
cluster while=0(a,I) -> good;
correctness
proof
A1: goto 0 does not destroy intloc 0 by SCMFSA7B:11;
I does not destroy intloc 0 by SCMFSA7B:def 5;
then if=0(a, I ';' goto 0) does not destroy intloc 0 by SCMFSA8C:99;
then while=0(a,I) does not destroy intloc 0 by SCMFSA8A:42,A1;
hence thesis by SCMFSA7B:def 5;
end;
end;
:: -----------------------------------------------------------
:: WHILE>0 Statement
::$CT 6
theorem Th12:
for s being State of SCM+FSA, I being MacroInstruction of SCM+FSA, a
being read-write Int-Location
st s.a <= 0 holds while>0(a,I) is_halting_on s,P
proof
let s be State of SCM+FSA;
let I be MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
assume
A1: s.a <= 0;
set i = a >0_goto 3;
set s1 = Initialize s,
P1 = P +* while>0(a,I);
IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
then
A2: IC SCM+FSA in dom Start-At(0,SCM+FSA);
A3: IC s1 = IC Start-At(0,SCM+FSA) by A2,FUNCT_4:13
.= 0 by FUNCOP_1:72;
set loc5= (card I +4);
set s5 = Comput(P1,s1,3);
set s4 = Comput(P1,s1,2);
set s2 = Comput(P1,s1,1);
A4: 1 in dom while>0(a,I) by SCMFSA_X:9;
not a in dom Start-At(0,SCM+FSA) by SCMFSA_2:102;
then
A5: s1.a = s.a by FUNCT_4:11;
A6: (P1)/.IC s1 = P1.IC s1 by PBOOLE:143;
0 in dom while>0(a,I) by AFINSQ_1:65;
then P1. 0 = while>0(a,I). 0 by FUNCT_4:13
.= i by SCMFSA_X:10;
then
A7: CurInstr(P1,s1) = i by A3,A6;
A8: Comput(P1,s1,0+1) = Following(P1,Comput(P1,s1,0)) by EXTPRO_1:3
.= Exec(i,s1) by A7;
A9: IC Comput(P1,s1,1) = 0 + 1 by A1,A3,A8,A5,SCMFSA_2:71;
A10: (P1)/.IC Comput(P1,s1,1) = P1.IC Comput(P1,s1,1) by PBOOLE:143;
P1. 1 = (while>0(a,I)). 1 by A4,FUNCT_4:13
.= goto 2 by SCMFSA_X:10;
then
A11: CurInstr(P1,Comput(P1,s1,1))
= goto 2 by A9,A10;
A12: Comput(P1,s1,1+1) = Following(P1,s2) by EXTPRO_1:3
.= Exec(goto 2,s2) by A11;
A13: IC s4 = 2 by A12,SCMFSA_2:69;
A14: 2 in dom while>0(a,I) by SCMFSA_X:7;
A15: loc5 in dom while>0(a,I) by SCMFSA_X:8;
A16: (P1)/.IC s4 = P1.IC s4 by PBOOLE:143;
P1. 2 = (while>0(a,I)). 2 by A14,FUNCT_4:13
.= goto loc5 by SCMFSA_X:17;
then
A17: CurInstr(P1,s4) = goto loc5 by A13,A16;
A18: Comput(P1,s1,2+1) = Following(P1,s4) by EXTPRO_1:3
.= Exec(goto loc5,s4) by A17;
A19: IC s5 = loc5 by A18,SCMFSA_2:69;
A20: (P1)/.IC s5 = P1.IC s5 by PBOOLE:143;
P1.loc5 = while>0(a,I).loc5 by A15,FUNCT_4:13
.= halt SCM+FSA by SCMFSA_X:16;
then
CurInstr(P1,s5) = halt SCM+FSA by A19,A20;
then P1 halts_on s1 by EXTPRO_1:29;
hence while>0(a,I) is_halting_on s,P by SCMFSA7B:def 7;
thus thesis;
end;
theorem Th13:
for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA,
s being State of SCM+FSA,k being Nat
st I is_halting_on s,P
& k < LifeSpan(P +* I,Initialize s) &
IC Comput(P +* while>0(a,I),(Initialize s),1+k)
= IC Comput(P +* I, (Initialize s),k) + 3 &
DataPart Comput(P +* while>0(a,I),(Initialize s),1+k)
= DataPart Comput(P +* I,(Initialize s),k)
holds IC Comput(P +* while>0(a,I),(Initialize s),1+k+1) = IC
Comput(P +* I, (Initialize s),k+1) + 3 &
DataPart Comput(P +* while>0(a,I),(Initialize s),1+k+1) =
DataPart Comput(P +* I, (Initialize s),k+1)
proof
set J = Stop SCM+FSA;
let a be Int-Location;
set D = Int-Locations \/ FinSeq-Locations;
let I be really-closed MacroInstruction of SCM+FSA;
let s be State of SCM+FSA;
let k be Nat;
set s1 = Initialize s,
P1 = P +* while>0(a,I);
set sI = Initialize s,
PI = P +* I;
A1: I c= PI by FUNCT_4:25;
set sK1= Comput(P1, s1,1+k);
set sK2= Comput(PI, sI,k);
set l3=IC Comput(PI, sI,k);
set I1= I ';' goto 0;
set i = a >0_goto 3;
reconsider n = l3 as Element of NAT;
set Mi= i ";" Goto (card I1 + 1);
set J2= I1 ";" Stop SCM+FSA;
A2: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
A3: I c= PI by FUNCT_4:25;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom I by AFINSQ_1:65;
then
A4: n in dom I by AMISTD_1:21,A3;
then n < card I by AFINSQ_1:66;
then
A5: n+3 < card I+ 5 by XREAL_1:8;
A6: PI/.IC sK2 = PI.IC sK2 by PBOOLE:143;
A7: CurInstr(PI,sK2) = I. n by A4,A1,GRFUNC_1:2,A6;
assume I is_halting_on s,P;
then
A8: PI halts_on sI by SCMFSA7B:def 7;
assume k < LifeSpan(PI,sI);
then
I. n <> halt SCM+FSA by A7,A8,EXTPRO_1:def 15;
then
A9: n <> LastLoc I by COMPOS_1:def 14;
n <= LastLoc I by A4,VALUED_1:32;
then
A10: n < LastLoc I by A9,XXREAL_0:1;
then
A11: n in dom CutLastLoc I by COMPOS_2:26;
dom I c= dom I1 by COMPOS_1:21;
then
A12: n in dom I1 by A4;
dom I1 = dom CutLastLoc I \/ dom Reloc(Macro goto 0, card I -' 1)
by FUNCT_4:def 1;
then
A13: dom CutLastLoc I c= dom I1 by XBOOLE_1:7;
A14: dom CutLastLoc I misses dom Reloc(Macro goto 0, card I -' 1)
by COMPOS_1:18;
A15: n in dom I1 by A11,A13;
dom I c= dom I1 by COMPOS_1:21;
then LastLoc I <= LastLoc I1 by VALUED_1:68;
then n < LastLoc I1 by A10,XXREAL_0:2;
then
A16: I1.n <> halt SCM+FSA by A15,COMPOS_1:def 15;
dom I1 c= dom J2 by SCMFSA6A:17;
then
A17: n in dom J2 by A12;
then n + 3 in { il+3 where il is Nat: il in dom J2};
then
A18: n+3 in dom Shift(J2,3) by VALUED_1:def 12;
then
A19: Shift(J2,3)/.(n+3) =Shift(J2,3).( n +3) by PARTFUN1:def 6
.=J2. n by A17,VALUED_1:def 12
.= I1.n by A16,A15,SCMFSA6A:15
.=(CutLastLoc I). n by A11,FUNCT_4:16,A14
.=I.n by A10,COMPOS_2:27;
card while>0(a,I) = card I + 5 by SCMFSA_X:4;
then
A20: n+3 in dom while>0(a,I) by A5,AFINSQ_1:66;
I. n in rng I by A4,FUNCT_1:def 3;
then reconsider j = I. n as Instruction of SCM+FSA by A2;
A21: card Mi = card Macro i + card Goto (card I1 + 1) by SCMFSA6A:21
.= card Macro i + 1 by SCMFSA8A:15
.= 2 + 1 by COMPOS_1:56
.= 3;
then n+3 >= card Mi by NAT_1:11;
then
A22: not n+3 in dom Mi by AFINSQ_1:66;
A23: Comput(PI, sI,k+1) = Following(PI,sK2) by EXTPRO_1:3
.= Exec(j,sK2) by A7;
assume
A24: IC Comput(P1, s1,1+k)=l3 + 3;
:::B3: n < LastLoc I by B4,XXREAL_0:1;
n + 3 < LastLoc I + 3 by A10,XREAL_1:6;
then
A25: n + 3 <> card I - 1 + 3 by AFINSQ_1:91;
dom while>0(a,I) = dom if>0(a,I1) by FUNCT_7:30;
then
A26: n+3 in dom if>0(a,I1) by A20;
A27: if>0(a,I1) = Mi ";" J2 by SCMFSA6A:25;
then
dom if>0(a,I1) = dom Mi \/ dom Reloc(J2, 3) by SCMFSA6A:39,A21;
then
A28: (n+3) in dom Reloc(J2, 3) by A26,A22,XBOOLE_0:def 3;
A29: (P1)/.IC sK1 = P1.IC sK1 by PBOOLE:143;
A30: Reloc(J2,3) = IncAddr(Shift(J2,3),3) by COMPOS_1:34;
P1. (n+3) = (while>0(a,I)). (n+3) by A20,FUNCT_4:13
.= (Mi ";" J2). (n+3) by A27,FUNCT_7:32,A25
.= (Reloc(J2,3)).(n+3) by A28,SCMFSA6A:40,A21
.= IncAddr(j,3) by A18,A19,A30,COMPOS_1:def 21;
then
A31: CurInstr(P1,sK1) =IncAddr(j,3) by A24,A29;
assume
A32: DataPart sK1 = DataPart sK2;
Comput(P1, s1,1+k+1) = Following(P1,sK1) by EXTPRO_1:3
.= Exec(IncAddr(j,3),sK1) by A31;
hence thesis by A24,A32,A23,SCMFSA6A:8;
end;
theorem Th14:
for a being Int-Location, I being really-closed MacroInstruction of SCM+FSA,
s being State of SCM+FSA st I is_halting_on s,P &
IC Comput(P +* while>0(a,I), Initialize s,1 + LifeSpan(P +* I,Initialize s))
= IC Comput(P +* I,Initialize s,LifeSpan(P +* I,Initialize s) ) + 3
holds CurInstr(P +* while>0(a,I),
Comput(P +* while>0(a,I),Initialize s,
(1 + LifeSpan(P +* I,Initialize s)))) = goto 0
proof
set J3= Goto 0 ";" Stop SCM+FSA;
set J = Stop SCM+FSA;
let a be Int-Location;
let I be really-closed MacroInstruction of SCM+FSA;
let s be State of SCM+FSA;
set s1 = Initialize s,
P1 = P +* while>0(a,I);
set sI = Initialize s,
PI = P +* I;
A1: I c= PI by FUNCT_4:25;
set life=LifeSpan(P +* I,Initialize s);
set sK1= Comput(P1, s1,1+life);
set sK2= Comput(PI, sI,life);
set I1= I ';' goto 0;
set i = a >0_goto 3;
reconsider n = IC sK2 as Element of NAT;
set Mi= i ";" Goto (card I1 + 1);
set J2= I1 ";" Stop SCM+FSA;
A2: I c= PI by FUNCT_4:25;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom I by AFINSQ_1:65;
then
A3: n in dom I by AMISTD_1:21,A2;
then n < card I by AFINSQ_1:66;
then
A4: n+3 < card I+ 5 by XREAL_1:8;
assume I is_halting_on s,P;
then
A5: PI halts_on sI by SCMFSA7B:def 7;
A6: (PI)/.IC sK2 = PI.IC sK2 by PBOOLE:143;
A7: (P1)/.IC sK1 = P1.IC sK1 by PBOOLE:143;
assume
A8: IC sK1 = IC sK2 + 3;
CurInstr(PI,sK2) = I. n by A3,A1,GRFUNC_1:2,A6;
then
A9: I.IC sK2 = halt SCM+FSA by A5,EXTPRO_1:def 15;
IC sK2 = LastLoc I by A3,A9,COMPOS_1:def 15
.= card I - 1 by AFINSQ_1:91;
then
A10: IC sK2 + 3 = card I + 2;
card while>0(a,I) = card I + 5 by SCMFSA_X:4;
then
A11: n+3 in dom while>0(a,I) by A4,AFINSQ_1:66;
A12: n+3 in dom if>0(a,I1) by A11,FUNCT_7:30;
P1. (n+3) = (while>0(a,I)). (n+3) by FUNCT_4:13,A11
.= (while>0(a,I)).(card I + 2) by A10
.= goto 0 by FUNCT_7:31,A10,A12;
hence thesis by A8,A7;
end;
::$CT
theorem Th15:
for s being State of SCM+FSA,
I being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location
st I is_halting_on s,P & s.a >0
holds IC Comput(P +* while>0(a,I), Initialize s,
(LifeSpan(P +* I,Initialize s) + 2)) = 0 &
for k being Nat st k
<= LifeSpan(P +* I,Initialize s) + 2
holds IC Comput(P +* while>0(a,I),
(Initialize s),k) in dom while>0(a,I)
proof
set D = Int-Locations \/ FinSeq-Locations;
let s be State of SCM+FSA;
let I be really-closed MacroInstruction of SCM+FSA;
let a be read-write Int-Location;
set sI = Initialize s,
PI = P +* I;
set s1 = Initialize s,
P1 = P +* while>0(a,I);
defpred P[Nat] means $1 <= LifeSpan(PI,sI) implies IC Comput(
P1, s1
,1+$1) = IC Comput(PI, sI,$1)+ 3 & DataPart Comput(P1, s1,1+$1) = DataPart
Comput(PI, sI,$1);
assume
A1: I is_halting_on s,P;
A2: now
let k be Nat;
assume
A3: P[k];
now
A4: k + 0 < k + 1 by XREAL_1:6;
assume k + 1 <= LifeSpan(PI,sI);
then k < LifeSpan(PI,sI) by A4,XXREAL_0:2;
hence IC Comput(P1, s1,1+k+1) = IC Comput(PI,sI,k+1) + 3 &
DataPart Comput(P1, s1,1+k+1) = DataPart Comput(PI, sI,k+1)
by A1,A3,Th13;
end;
hence P[k + 1];
end;
reconsider l=LifeSpan(PI,sI) as Element of NAT by ORDINAL1:def 12;
set loc4= (card I + 3);
set i = a >0_goto 3;
set s2 = Comput(P1,s1,1);
IC SCM+FSA in dom (Start-At(0,SCM+FSA)) by MEMSTR_0:15;
then
A5: IC s1 = IC(Start-At(0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72;
not a in dom (Start-At(0,SCM+FSA)) by SCMFSA_2:102;
then
A6: s1.a = s.a by FUNCT_4:11;
assume
A7: s.a > 0;
A8: 0 in dom while>0(a,I) by AFINSQ_1:65;
A9: (P1)/.IC s1 = P1.IC s1 by PBOOLE:143;
P1. 0 = while>0(a,I). 0 by A8,FUNCT_4:13
.= i by SCMFSA_X:10;
then
A10: CurInstr(P1,s1) = i by A5,A9;
A11: Comput(P1,s1,0+1) = Following(P1,Comput(P1,s1,0)) by EXTPRO_1:3
.= Exec(i,s1) by A10;
then ( for c holds s2.c = s1.c)& for f holds s2.f = s1.f by SCMFSA_2:71;
then
A12: DataPart s2 = DataPart sI by SCMFSA_M:2;
A13: IC s2 = 3 by A7,A11,A6,SCMFSA_2:71;
A14: P[ 0]
proof
assume 0 <= LifeSpan(PI,sI);
A15: IC SCM+FSA in dom Start-At(0,SCM+FSA) by MEMSTR_0:15;
IC Comput(PI, sI,0)
= IC Start-At(0,SCM+FSA) by A15,FUNCT_4:13
.= 0 by FUNCOP_1:72;
hence thesis by A13,A12;
end;
A16: for k being Nat holds P[k] from NAT_1:sch 2(A14,A2);
set s4= Comput(P1, s1,1+LifeSpan(PI,sI)+1);
set s3= Comput(P1, s1,1+LifeSpan(PI,sI));
set s2= Comput(P1, s1,1+LifeSpan(PI,sI));
P[l] by A16;
then
A17: CurInstr(P1,s2) = goto 0 by A1,Th14;
A18: CurInstr(P1,s3) = goto 0 by A17;
A19: s4 = Following(P1,s3) by EXTPRO_1:3
.= Exec(goto 0,s3) by A18;
A20: IC s4 = 0 by A19,SCMFSA_2:69;
hence IC Comput(P1, s1,LifeSpan(PI,sI)+2) = 0;
A21: now
let k be Nat;
assume
A22: k <= LifeSpan(PI,sI)+2;
assume k<>0;
then consider n being Nat such that
A23: k = n+ 1 by NAT_1:6;
k<=LifeSpan(PI,sI)+1 or k >= LifeSpan(PI,sI)+1+1 by NAT_1:13;
then
A24: k <=LifeSpan(PI,sI)+1 or k = LifeSpan(PI,sI)+2 by A22,XXREAL_0:1;
reconsider n as Element of NAT by ORDINAL1:def 12;
per cases by A24;
suppose
k<=LifeSpan(PI,sI)+1;
then n <= LifeSpan(PI,sI) by A23,XREAL_1:6;
then
A25: IC Comput(P1,s1,1+n) = IC Comput(PI, sI,n) + 3
by A16;
reconsider m = IC Comput(PI, sI,n) as Element of NAT;
A26: I c= PI by FUNCT_4:25;
IC sI = 0 by MEMSTR_0:def 11;
then IC sI in dom I by AFINSQ_1:65;
then m in dom I by AMISTD_1:21,A26;
then m < card I by AFINSQ_1:66;
then
A27: m+3 < card I+ 5 by XREAL_1:8;
card while>0(a,I) = card I + 5 by SCMFSA_X:4;
hence IC Comput(P1,s1,k) in dom while>0(a,I) by A23,A25,A27,AFINSQ_1:66;
end;
suppose
k >= LifeSpan(PI,sI)+2;
then k = LifeSpan(PI,sI)+2 by A22,XXREAL_0:1;
hence IC Comput(P1,s1,k) in dom while>0(a,I) by A20,AFINSQ_1:65;
end;
end;
now
let k be Nat;
assume
A28: k <= LifeSpan(PI,sI)+2;
per cases;
suppose
k = 0;
hence IC Comput(P1,s1,k) in dom while>0(a,I) by A8,A5;
end;
suppose
k <>0;
hence IC Comput(P1,s1,k) in dom while>0(a,I) by A21,A28;
end;
end;
hence thesis;
end;
reserve s for State of SCM+FSA,
I for MacroInstruction of SCM+FSA,
a for read-write Int-Location;
definition
let s,I,a,P;
deffunc U(Nat,State of SCM+FSA)
= Comput(P +* while>0(a,I), Initialize $2,
LifeSpan(P +* while>0(a,I) +* I, Initialize $2) + 2);
deffunc V(Nat,State of SCM+FSA) = down U($1,$2);
func StepWhile>0(a,I,P,s) -> sequence of product the_Values_of
SCM+FSA means
:Def2:
it.0 = s & for i being Nat
holds it.(i+1)= Comput(P +* while>0(a,I), Initialize(it.i),
LifeSpan(P +* while>0(a,I) +* I, Initialize(it.i)) + 2);
existence
proof
reconsider ss=s as
Element of product the_Values_of SCM+FSA by CARD_3:107;
consider f being sequence of product the_Values_of SCM+FSA
such that
A1: f.0 = ss and
A2: for i being Nat holds f.(i+1)= V(i,f.i) from NAT_1:sch 12;
take f;
thus f.0 = s by A1;
let i be Nat;
f.(i+1)= V(i,f.i) by A2;
hence thesis;
end;
uniqueness
proof
let F1,F2 be sequence of product the_Values_of SCM+FSA such that
A3: F1.0 = s and
A4: for i being Nat holds F1.(i+1)= U(i,F1.i) and
A5: F2.0 = s and
A6: for i being Nat holds F2.(i+1)= U(i,F2.i);
reconsider s as Element of product the_Values_of SCM+FSA by CARD_3:107;
A7: F1.0 = s by A3;
A8: for i being Nat holds F1.(i+1)= V(i,F1.i) by A4;
A9: F2.0 = s by A5;
A10: for i being Nat holds F2.(i+1)= V(i,F2.i) by A6;
F1 = F2 from NAT_1:sch 16(A7,A8,A9,A10);
hence thesis;
end;
end;
theorem Th16:
StepWhile>0(a,I,P,s).(k+1)=StepWhile>0(a,I,P,StepWhile>0(a,I,P,s).k).1
proof
set sk=StepWhile>0(a,I,P,s).k;
set sk0=StepWhile>0(a,I,P,sk).0;
sk0=sk by Def2;
hence
StepWhile>0(a,I,P,s).(k+1) = Comput(P +* while>0(a,I),Initialize sk0,
LifeSpan(P +* while>0(a,I) +* I,Initialize sk0) + 2) by Def2
.=StepWhile>0(a,I,P,sk).(0+1) by Def2
.=StepWhile>0(a,I,P,sk).1;
end;
theorem Th17:
for I being MacroInstruction of SCM+FSA,a being read-write Int-Location,
s being State of SCM+FSA holds StepWhile>0(a,I,P,s).1
= Comput(P +* while>0(a,I),
Initialize s,
LifeSpan(P +* while>0(a,I)+* I,Initialize s) + 2)
proof
let I be MacroInstruction of SCM+FSA,a be read-write Int-Location,
s be State of SCM+FSA;
A1: StepWhile>0(a,I,P,s).0 = s by Def2;
thus StepWhile>0(a,I,P,s).1 = StepWhile>0(a,I,P,s).(0+1)
.= Comput(P +* while>0(a,I), (Initialize s),
(LifeSpan(P +* while>0(a,I)+* I,Initialize s)+ 2)) by A1,Def2;
end;
theorem Th18:
for I being MacroInstruction of SCM+FSA,a being read-write Int-Location,
s being State of SCM+FSA,k,n being Nat
st IC StepWhile>0(a,I,P,s).k =
0 & StepWhile>0(a,I,P,s).k= Comput(P +* while>0(a,I),
(Initialize s),n)
holds StepWhile>0(a,I,P,s).k = Initialize(StepWhile>0(a,I,P,s).k)
& StepWhile>0(a,I,P,s).(k+1)=
Comput(P +* while>0(a,I), Initialize s,
n +(LifeSpan(P +* while>0(a,I) +* I,Initialize(StepWhile>0(a,I,P,s).k)
) + 2))
proof
let I be MacroInstruction of SCM+FSA,a be read-write Int-Location,
s be State of SCM+FSA,k,n be Nat;
set D = Int-Locations \/ FinSeq-Locations;
set s1 = Initialize s,
P1 = P +* while>0(a,I);
set sk=StepWhile>0(a,I,P,s).k;
set s2=Initialize sk;
assume
A1: IC sk = 0;
assume
A2: sk = Comput(P1, s1,n);
sk is 0-started by A1;
then Start-At(0,SCM+FSA) c= sk by MEMSTR_0:29;
hence s2=sk by FUNCT_4:98;
hence
StepWhile>0(a,I,P,s).(k+1)=
Comput(P1, sk,LifeSpan(P +* while>0(a,I) +* I,
Initialize sk) +2)
by Def2
.= Comput(P1, s1,n +(LifeSpan(P +* while>0(a,I) +* I,
Initialize sk) + 2))
by A2,EXTPRO_1:4;
end;
theorem Th19:
for I being really-closed MacroInstruction of SCM+FSA,
a being read-write Int-Location,
s being State of SCM+FSA st (for k being Nat
holds
I is_halting_on StepWhile>0(a,I,P,s).k,P+*while>0(a,I)) &
ex f being Function of
product the_Values_of SCM+FSA,NAT st (for k being Nat holds (f.(
StepWhile>0(a,I,P,s).(k+1)) < f.(StepWhile>0(a,I,P,s).k) or
f.(StepWhile>0(a,I,P,s).k
) = 0) & ( f.(StepWhile>0(a,I,P,s).k)=0 iff
(StepWhile>0(a,I,P,s).k).a <= 0 ))
holds while>0(a,I) is_halting_on s,P
proof
let I be really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location, s be State of
SCM+FSA;
set D = Int-Locations \/ FinSeq-Locations;
assume
A1: for k being Nat holds
I is_halting_on StepWhile>0(a,I,P,s).k,P+*while>0(a,I);
set s1 = Initialize s,
P1 = P +* while>0(a,I);
A2: P1 +* while>0(a,I) = P1;
given f being Function of product the_Values_of SCM+FSA,NAT such that
A3: for k being Nat
holds (f.(StepWhile>0(a,I,P,s).(k+1)) < f.(StepWhile>0
(a,I,P,s).k) or f.(StepWhile>0(a,I,P,s).k) = 0) &
( f.(StepWhile>0(a,I,P,s).k)=0
iff
(StepWhile>0(a,I,P,s).k).a <= 0 );
deffunc F(Nat) = f.(StepWhile>0(a,I,P,s).$1);
A4: for k being Nat holds F(k+1) < F(k) or F(k) = 0 by A3;
consider m being Nat such that
A5: F(m)=0 and
A6: for n being Nat st F(n) =0 holds m <= n from NAT_1:sch 17(A4);
defpred P[Nat] means $1+1 <= m implies ex k st StepWhile>0(a,I,P,s)
.($1+1)= Comput(P1, s1,k);
A7: now
let k be Nat;
assume
A8: P[k];
now
set sk1=StepWhile>0(a,I,P,s).(k+1);
set sk=StepWhile>0(a,I,P,s).k;
assume
A9: (k+1)+ 1 <= m;
k + 0 < k+ (1+ 1) by XREAL_1:6;
then k < m by A9,XXREAL_0:2;
then F(k) <> 0 by A6;
then
A10: sk.a > 0 by A3;
A11: I is_halting_on sk,P+*while>0(a,I) by A1;
(k+1)+ 0 < (k+ 1)+ 1 by XREAL_1:6;
then consider n being Nat such that
A12: sk1 = Comput(P1, s1,n) by A8,A9,XXREAL_0:2;
take m=n +(LifeSpan(P +* while>0(a,I) +* I,
Initialize sk1) + 2);
sk1= Comput(P +* while>0(a,I), (Initialize sk),
(LifeSpan(P +* while>0(a,I) +* I,Initialize sk) + 2)) by Def2;
then IC sk1 = 0 by A11,A10,Th15,A2;
hence StepWhile>0(a,I,P,s).((k+1)+1)= Comput(P1, s1,m) by A12,Th18;
end;
hence P[k+1];
end;
A13: P[ 0]
proof
assume 0+1 <= m;
take n=(LifeSpan(P+*while>0(a,I)+* I,Initialize s) + 2);
thus thesis by Th17;
end;
A14: for k being Nat holds P[k] from NAT_1:sch 2(A13,A7);
now
per cases;
suppose
m=0;
then (StepWhile>0(a,I,P,s).0).a <= 0 by A3,A5;
then s.a <= 0 by Def2;
hence thesis by Th12;
end;
suppose
A15: m<>0;
set p=(LifeSpan(P+*while>0(a,I)+* I,Initialize s) + 3);
set sm=StepWhile>0(a,I,P,s).m;
set sm1=Initialize sm;
consider i being Nat such that
A16: m=i+1 by A15,NAT_1:6;
reconsider i as Element of NAT by ORDINAL1:def 12;
consider n being Nat such that
A17: sm = Comput(P1, s1,n) by A14,A16;
set si=StepWhile>0(a,I,P,s).i;
i < m by A16,NAT_1:13;
then F(i) <> 0 by A6;
then
A18: si.a > 0 by A3;
A19: I is_halting_on si,P+*while>0(a,I) by A1;
sm= Comput(P +* while>0(a,I), (Initialize si),
(LifeSpan(P +* while>0(a,I) +* I,Initialize si) + 2))
by A16,Def2;
then sm is 0-started by A19,A18,Th15,A2;
then Start-At(0,SCM+FSA) c= sm by MEMSTR_0:29;
then
A20: sm1=sm by FUNCT_4:98;
sm.a <= 0 by A3,A5;
then while>0(a,I) is_halting_on sm,P1 by Th12;
then P1 +* while>0(a,I) halts_on Initialize sm by SCMFSA7B:def 7;
then P1 halts_on sm1;
then consider j being Nat such that
A21: CurInstr(P1,Comput(P1,sm,j))
= halt SCM+FSA by A20;
A22: Comput(P1,s1,n+j)
= Comput(P1,Comput(P1,s1,n),j) by EXTPRO_1:4;
CurInstr(P1,Comput(P1,s1,n+j))
= halt SCM+FSA by A17,A21,A22;
then P1 halts_on s1 by EXTPRO_1:29;
hence while>0(a,I) is_halting_on s,P by SCMFSA7B:def 7;
end;
end;
hence thesis;
end;
theorem Th20:
for I being parahalting really-closed MacroInstruction of SCM+FSA,
a being read-write
Int-Location, s being State of SCM+FSA st
ex f being Function of product the_Values_of SCM+FSA,NAT st (for k being Nat
holds (f.(StepWhile>0(a,I,P,s).(k+
1)) < f.(StepWhile>0(a,I,P,s).k) or f.(StepWhile>0(a,I,P,s).k) = 0) & ( f.(
StepWhile>0(a,I,P,s).k)=0 iff (StepWhile>0(a,I,P,s).k).a <= 0 ) )
holds while>0(a,I) is_halting_on s,P
proof
let I be parahalting really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location,s be State of SCM+FSA;
A1: for k being Nat holds
I is_halting_on StepWhile>0(a,I,P,s).k,P+*while>0(a,I) by SCMFSA7B:19;
assume ex f being Function of product the_Values_of SCM+FSA,NAT st for
k being Nat holds (f.(StepWhile>0(a,I,P,s).(k+1)) < f.(StepWhile>0(a,I,P,s).k)
or f
.(StepWhile>0(a,I,P,s).k) = 0) & ( f.(StepWhile>0(a,I,P,s).k)=0
iff (StepWhile>0(a,I,P,s).k).a <= 0 );
hence thesis by A1,Th19;
end;
theorem
for I being parahalting really-closed MacroInstruction of SCM+FSA,
a being read-write
Int-Location st ex f being Function of product the_Values_of SCM+FSA,NAT
st (for s being State of SCM+FSA,P holds (f.(StepWhile>0(a,I,P,s).1) < f.s
or f.s =
0) & ( f.s =0 iff s.a <= 0 )) holds while>0(a,I) is parahalting
proof
let I be parahalting really-closed MacroInstruction of SCM+FSA,
a be read-write Int-Location;
given f being Function of product the_Values_of SCM+FSA,NAT such that
A1: for s being State of SCM+FSA,P holds (f.(StepWhile>0(a,I,P,s).1) < f.s
or f.s = 0) & ( f.s =0 iff s.a <= 0 );
now
let t be State of SCM+FSA;
let Q;
now
let k be Nat;
f.(StepWhile>0(a,I,Q,StepWhile>0(a,I,Q,t).k).1)
< f.(StepWhile>0(a,I,Q,t).
k) or f.(StepWhile>0(a,I,Q,t).k) = 0 by A1;
hence (f.(StepWhile>0(a,I,Q,t).(k+1)) < f.(StepWhile>0(a,I,Q,t).k) or f.(
StepWhile>0(a,I,Q,t).k) = 0) & ( f.(StepWhile>0(a,I,Q,t).k)=0
iff (StepWhile>0(a,I,Q,
t).k).a <= 0 ) by A1,Th16;
end;
hence while>0(a,I) is_halting_on t,Q by Th20;
end;
hence thesis by SCMFSA7B:19;
end;
registration
let I,J be good MacroInstruction of SCM+FSA,a be Int-Location;
cluster if>0(a,I,J) -> good;
coherence
proof
set i = a >0_goto (card J + 3);
reconsider Mi=Macro i as good Program of SCM+FSA by Th11,SCMFSA7B:13;
if>0(a,I,J) = Mi ";" J ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
hence thesis;
end;
end;
registration
let I be good MacroInstruction of SCM+FSA,a be Int-Location;
cluster if>0(a,I) -> good;
correctness
proof
set i = a >0_goto 3;
reconsider Mi=Macro i as good Program of SCM+FSA by Th11,SCMFSA7B:13;
if>0(a,I)
= Mi ";" Goto (card I + 1) ";" I ";" Stop SCM+FSA;
hence thesis;
end;
end;
registration
let I be good MacroInstruction of SCM+FSA,a be Int-Location;
cluster while>0(a,I) -> good;
correctness
proof
A1: goto 0 does not destroy intloc 0 by SCMFSA7B:11;
I does not destroy intloc 0 by SCMFSA7B:def 5;
then if>0(a, I ';' goto 0) does not destroy intloc 0 by SCMFSA8C:98;
then while>0(a,I) does not destroy intloc 0 by SCMFSA8A:42,A1;
hence thesis by SCMFSA7B:def 5;
end;
end;
theorem
for p be preProgram of SCM+FSA,l be Nat,
ic be Instruction of SCM+FSA st
(ex pc be Instruction of SCM+FSA st pc=p.l & UsedIntLoc pc =UsedIntLoc ic)
holds UsedILoc p = UsedILoc(p+*(l,ic))
proof
let p be preProgram of SCM+FSA,l be Nat, ic be Instruction of SCM+FSA;
given pc be Instruction of SCM+FSA such that
A1: pc = p.l and
A2: UsedIntLoc pc = UsedIntLoc ic;
{ UsedIntLoc i where i is Instruction of SCM+FSA : i in rng p} =
{ UsedIntLoc j where j is Instruction of SCM+FSA : j in rng(p+*(l,ic))}
from FUNCT_7:sch 7(A2,A1);
hence thesis;
end;
theorem
for p be preProgram of SCM+FSA,l be Nat,
ic be Instruction of SCM+FSA st (ex pc be Instruction of SCM+FSA
st pc=p.l & UsedInt*Loc pc=UsedInt*Loc ic)
holds UsedI*Loc p = UsedI*Loc (p +*(l,ic))
proof
let p be preProgram of SCM+FSA,l be Nat, ic be Instruction of SCM+FSA;
given pc be Instruction of SCM+FSA such that
A1: pc = p.l and
A2: UsedInt*Loc pc = UsedInt*Loc ic;
{ UsedInt*Loc i where i is Instruction of SCM+FSA : i in rng p} =
{ UsedInt*Loc j where j is Instruction of SCM+FSA : j in rng(p+*(l,ic))}
from FUNCT_7:sch 7(A2,A1);
hence thesis;
end;