Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Jing-Chao Chen,
and
- Yatsuka Nakamura
- Received June 17, 1998
- MML identifier: SCM_HALT
- [
Mizar article,
MML identifier index
]
environ
vocabulary SCMFSA6A, AMI_1, SCMFSA_2, FUNCT_1, RELAT_1, CAT_1, FUNCT_4, AMI_3,
BOOLE, FUNCOP_1, SCMFSA6B, FUNCT_7, SF_MASTR, FINSEQ_1, INT_1, AMI_5,
RELOC, SCM_1, CARD_1, SCMFSA6C, SCMFSA7B, SCMFSA_4, UNIALG_2, SCMFSA8B,
ARYTM_1, SCMFSA8C, SCMFSA8A, SCM_HALT, CARD_3;
notation TARSKI, XBOOLE_0, ENUMSET1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
RELAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_7, STRUCT_0, AMI_1,
AMI_3, AMI_5, SCMFSA_2, CQC_LANG, CARD_1, SCM_1, SCMFSA_4, SCMFSA6B,
SCMFSA_5, SCMFSA6A, SF_MASTR, SCMFSA8A, SCMFSA8B, SCMFSA8C, SCMFSA7B,
BINARITH, SCMFSA_3, SCMFSA6C;
constructors SCM_1, AMI_5, SCMFSA_3, SCMFSA_5, SF_MASTR, SCMFSA6A, SCMFSA6B,
SCMFSA6C, SETWISEO, SCMFSA8A, SCMFSA8B, SCMFSA8C, BINARITH;
clusters FUNCT_1, PRELAMB, AMI_1, SCMFSA_2, SCMFSA_4, INT_1, SCMFSA6A,
SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8C, SCMFSA6B, SCMFSA_9,
CQC_LANG, NAT_1, FRAENKEL, XREAL_0, XBOOLE_0, ORDINAL2, NUMBERS;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve m,n for Nat,
I for Macro-Instruction,
s,s1,s2 for State of SCM+FSA,
a for Int-Location,
f for FinSeq-Location;
definition let I be Macro-Instruction;
attr I is InitClosed means
:: SCM_HALT:def 1
for s being State of SCM+FSA, n being Nat
st Initialized I c= s
holds IC (Computation s).n in dom I;
attr I is InitHalting means
:: SCM_HALT:def 2
Initialized I is halting;
attr I is keepInt0_1 means
:: SCM_HALT:def 3
::def5
for s being State of SCM+FSA st Initialized I c= s
for k being Nat holds ((Computation s).k).intloc 0 = 1;
end;
theorem :: SCM_HALT:1 ::TM001
for x being set,i,m,n being Nat st
x in dom (((intloc i) .--> m) +* Start-At insloc n) holds
x=intloc i or x=IC SCM+FSA;
theorem :: SCM_HALT:2 ::TM002
for I being Macro-Instruction,i,m,n being Nat holds
dom I misses dom (((intloc i) .--> m) +* Start-At insloc n);
theorem :: SCM_HALT:3 ::I_iS
Initialized I = I +* (((intloc 0) .--> 1) +* Start-At insloc 0);
theorem :: SCM_HALT:4
Macro halt SCM+FSA is InitHalting;
definition
cluster InitHalting Macro-Instruction;
end;
theorem :: SCM_HALT:5 ::TM006=HA2,HA,SCMFSA6B:19
for I being InitHalting Macro-Instruction
st Initialized I c= s holds s is halting;
theorem :: SCM_HALT:6 ::TM007
I +* Start-At insloc 0 c= Initialized I;
theorem :: SCM_HALT:7 ::int0_1
for I being Macro-Instruction,s being State of SCM+FSA st
Initialized I c= s holds s.intloc 0 =1;
definition
cluster paraclosed -> InitClosed Macro-Instruction;
end;
definition
cluster parahalting -> InitHalting Macro-Instruction;
end;
definition
cluster InitHalting -> InitClosed Macro-Instruction;
cluster keepInt0_1 -> InitClosed Macro-Instruction;
cluster keeping_0 -> keepInt0_1 Macro-Instruction;
end;
theorem :: SCM_HALT:8 ::TM008=SCMFSA6B:22
for I being InitHalting Macro-Instruction,
a being read-write Int-Location
holds not a in UsedIntLoc I implies (IExec(I, s)).a = s.a;
theorem :: SCM_HALT:9 ::TM010=SCMFSA6B:23
for I being InitHalting Macro-Instruction,f being FinSeq-Location
holds not f in UsedInt*Loc I implies (IExec(I, s)).f = s.f;
definition let I be InitHalting Macro-Instruction;
cluster Initialized I -> halting;
end;
definition
cluster InitHalting -> non empty Macro-Instruction;
end;
theorem :: SCM_HALT:10 ::TM012=SCMFSA6B:25
for I being InitHalting Macro-Instruction holds dom I <> {};
theorem :: SCM_HALT:11 ::TM014=SCMFSA6B:26
for I being InitHalting Macro-Instruction holds insloc 0 in dom I;
theorem :: SCM_HALT:12 ::TM016=SCMFSA6B:27 ::T0
for J being InitHalting Macro-Instruction st Initialized J c= s1
for n being Nat st ProgramPart Relocated(J,n) c= s2 &
IC s2 = insloc n &
s1 | (Int-Locations \/ FinSeq-Locations)
= s2 | (Int-Locations \/ FinSeq-Locations)
for i being Nat holds
IC (Computation s1).i + n = IC (Computation s2).i &
IncAddr(CurInstr ((Computation s1).i),n) = CurInstr ((Computation s2).i) &
(Computation s1).i | (Int-Locations \/ FinSeq-Locations)
= (Computation s2).i | (Int-Locations \/ FinSeq-Locations);
theorem :: SCM_HALT:13 ::TM018=MacroAt0:
Initialized I c= s implies I c= s;
theorem :: SCM_HALT:14 :: TM020=SCMFSA6B:28 ::T13
for I being InitHalting Macro-Instruction st
Initialized I c= s1 & Initialized I c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
for k being Nat holds
(Computation s1).k, (Computation s2).k
equal_outside the Instruction-Locations of SCM+FSA &
CurInstr (Computation s1).k = CurInstr (Computation s2).k;
theorem :: SCM_HALT:15 ::TM022=SCMFSA6B:29 ::T14
for I being InitHalting Macro-Instruction st
Initialized I c= s1 & Initialized I c= s2 &
s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
LifeSpan s1 = LifeSpan s2 &
Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:16
Macro halt SCM+FSA is keeping_0;
definition
cluster keeping_0 InitHalting Macro-Instruction;
end;
definition
cluster keepInt0_1 InitHalting Macro-Instruction;
end;
theorem :: SCM_HALT:17 ::TM026=SCMFSA6B:35
for I being keepInt0_1 InitHalting Macro-Instruction
holds IExec(I, s).intloc 0 = 1;
theorem :: SCM_HALT:18 ::TM028=MAI1:
for I being InitClosed Macro-Instruction, J being Macro-Instruction
st Initialized I c= s & s is halting
for m st m <= LifeSpan s
holds (Computation s).m,(Computation(s+*(I ';' J))).m
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:19 ::TM030=IScommute:
for i,m,n being Nat holds
s+*I+*(((intloc i) .--> m) +* Start-At insloc n) =
s+*(((intloc i) .--> m) +* Start-At insloc n)+* I;
theorem :: SCM_HALT:20 ::TM031:
((intloc 0) .--> 1) +* Start-At insloc 0 c= s implies
Initialized I c= s +* (I +* (((intloc 0) .--> 1) +* Start-At insloc 0)) &
s +* (I +* (((intloc 0) .--> 1) +* Start-At insloc 0)) = s +* I &
s +* (I +* (((intloc 0) .--> 1) +* Start-At insloc 0)) +* Directed I =
s +* Directed I;
theorem :: SCM_HALT:21 ::TM032=Lemma01
for I being InitClosed Macro-Instruction
st s +*I is halting & Directed I c= s &
((intloc 0) .--> 1) +* Start-At insloc 0 c= s holds
IC (Computation s).(LifeSpan (s +*I) + 1)
= insloc card I;
theorem :: SCM_HALT:22 ::TM034=Lemma02
for I being InitClosed Macro-Instruction
st s +*I is halting & Directed I c= s &
((intloc 0) .--> 1) +* Start-At insloc 0 c= s holds
(Computation s).(LifeSpan (s +*I)) |
(Int-Locations \/ FinSeq-Locations) =
(Computation s).(LifeSpan (s +*I) + 1) |
(Int-Locations \/ FinSeq-Locations);
theorem :: SCM_HALT:23 ::TM036=Lemma0
for I being InitHalting Macro-Instruction
st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr (Computation (s +* Directed I)).k <> halt SCM+FSA;
theorem :: SCM_HALT:24 ::TM038=Keep2
for I being InitClosed Macro-Instruction st s +* Initialized I is halting
for J being Macro-Instruction, k being Nat
st k <= LifeSpan (s +* Initialized I ) holds
(Computation (s +* Initialized I)).k,
(Computation (s +* Initialized (I ';' J))).k
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:25 ::TM040=Th1:
for I being keepInt0_1 InitHalting Macro-Instruction,
J being InitHalting Macro-Instruction,
s being State of SCM+FSA st Initialized (I ';' J) c= s holds
IC (Computation s).(LifeSpan (s +* I) + 1) = insloc card I &
(Computation s).(LifeSpan (s +* I) + 1)
| (Int-Locations \/ FinSeq-Locations)
= ((Computation (s +* I)).(LifeSpan (s +* I)) +* Initialized J)
| (Int-Locations \/ FinSeq-Locations) &
ProgramPart Relocated(J,card I) c=
(Computation s).(LifeSpan (s +* I) + 1) &
(Computation s).(LifeSpan (s +* I) + 1).intloc 0 = 1 &
s is halting &
LifeSpan s
= LifeSpan (s +* I) + 1 + LifeSpan (Result (s +* I) +* Initialized J) &
(J is keeping_0 implies (Result s).intloc 0 = 1);
definition
let I be keepInt0_1 InitHalting Macro-Instruction,
J be InitHalting Macro-Instruction;
cluster I ';' J -> InitHalting;
end;
theorem :: SCM_HALT:26 ::TM042=Keep3
for I being keepInt0_1 Macro-Instruction
st s +* I is halting
for J being InitClosed Macro-Instruction
st Initialized (I ';' J) c= s
for k being Nat holds
(Computation (Result(s +*I) +* Initialized J )).k +* Start-At (IC
(Computation (Result(s +*I) +* Initialized J )).k + card I),
(Computation (s +* (I ';' J))).(LifeSpan (s +* I)+1+k)
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:27 ::Keep1
for I being keepInt0_1 Macro-Instruction
st not s +* Initialized I is halting
for J being Macro-Instruction, k being Nat
holds (Computation (s +* Initialized I)).k,
(Computation (s +* Initialized (I ';' J))).k
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:28 ::TM044=T22
for I being keepInt0_1 InitHalting Macro-Instruction,
J being InitHalting Macro-Instruction
holds
LifeSpan (s +* Initialized (I ';' J))
= LifeSpan (s +* Initialized I) + 1
+ LifeSpan (Result (s +* Initialized I) +* Initialized J);
theorem :: SCM_HALT:29 ::TM046
for I being keepInt0_1 InitHalting Macro-Instruction,
J being InitHalting Macro-Instruction
holds
IExec(I ';' J,s) =
IExec(J,IExec(I,s)) +* Start-At (IC IExec(J,IExec(I,s)) + card I);
definition
let i be parahalting Instruction of SCM+FSA;
cluster Macro i -> InitHalting;
end;
definition
let i be parahalting Instruction of SCM+FSA,
J be parahalting Macro-Instruction;
cluster i ';' J -> InitHalting;
end;
definition
let i be keeping_0 parahalting Instruction of SCM+FSA,
J be InitHalting Macro-Instruction;
cluster i ';' J -> InitHalting;
end;
definition
let I, J be keepInt0_1 Macro-Instruction;
cluster I ';' J -> keepInt0_1;
end;
definition
let j be keeping_0 parahalting Instruction of SCM+FSA,
I be keepInt0_1 InitHalting Macro-Instruction;
cluster I ';' j -> InitHalting keepInt0_1;
end;
definition
let i be keeping_0 parahalting Instruction of SCM+FSA,
J be keepInt0_1 InitHalting Macro-Instruction;
cluster i ';' J -> InitHalting keepInt0_1;
end;
definition
let j be parahalting Instruction of SCM+FSA,
I be parahalting Macro-Instruction;
cluster I ';' j -> InitHalting;
end;
definition
let i,j be parahalting Instruction of SCM+FSA;
cluster i ';' j -> InitHalting;
end;
theorem :: SCM_HALT:30 ::TM048
for I being keepInt0_1 InitHalting Macro-Instruction,
J being InitHalting Macro-Instruction
holds IExec(I ';' J, s).a = IExec(J,IExec(I,s)).a;
theorem :: SCM_HALT:31 ::TM050
for I being keepInt0_1 InitHalting Macro-Instruction,
J being InitHalting Macro-Instruction
holds IExec(I ';' J, s).f = IExec(J,IExec(I,s)).f;
theorem :: SCM_HALT:32
for I be keepInt0_1 InitHalting Macro-Instruction,s be State of SCM+FSA holds
(Initialize IExec(I,s)) | (Int-Locations \/ FinSeq-Locations)
= IExec(I,s) | (Int-Locations \/ FinSeq-Locations);
theorem :: SCM_HALT:33 ::TM051=miI:
for I being keepInt0_1 InitHalting Macro-Instruction,
j being parahalting Instruction of SCM+FSA
holds IExec(I ';' j, s).a = Exec(j, IExec(I, s)).a;
theorem :: SCM_HALT:34 ::TM053=miF
for I being keepInt0_1 InitHalting Macro-Instruction,
j being parahalting Instruction of SCM+FSA
holds IExec(I ';' j, s).f = Exec(j, IExec(I, s)).f;
definition
let I be Macro-Instruction;
let s be State of SCM+FSA;
pred I is_closed_onInit s means
:: SCM_HALT:def 4
::def3=D18
for k being Nat holds
IC (Computation (s +* Initialized I )).k in dom I;
pred I is_halting_onInit s means
:: SCM_HALT:def 5
::def4=D18'
s +* Initialized I is halting;
end;
theorem :: SCM_HALT:35 ::TM052=TQ6
for I being Macro-Instruction holds
I is InitClosed iff for s being State of SCM+FSA holds I is_closed_onInit s;
theorem :: SCM_HALT:36 ::TM054=*TQ6'
for I being Macro-Instruction holds
I is InitHalting iff for s being State of SCM+FSA holds I is_halting_onInit s;
theorem :: SCM_HALT:37 ::TM055=TQ9''(SCMFSA7B)
for s being State of SCM+FSA, I being Macro-Instruction, a being Int-Location
st I does_not_destroy a & I is_closed_onInit s & Initialized I c= s
holds for k being Nat holds (Computation s).k.a = s.a;
definition
cluster InitHalting good Macro-Instruction;
end;
definition
cluster InitClosed good -> keepInt0_1 Macro-Instruction;
end;
definition
cluster SCM+FSA-Stop -> InitHalting good;
end;
theorem :: SCM_HALT:38 ::TM056=TG25
for s being State of SCM+FSA,
i being keeping_0 parahalting Instruction of SCM+FSA,
J being InitHalting Macro-Instruction, a being Int-Location
holds IExec(i ';' J,s).a = IExec(J,Exec(i,Initialize s)).a;
theorem :: SCM_HALT:39 ::TM058=TG26
for s being State of SCM+FSA,
i being keeping_0 parahalting Instruction of SCM+FSA,
J being InitHalting Macro-Instruction, f being FinSeq-Location
holds IExec(i ';' J,s).f = IExec(J,Exec(i,Initialize s)).f;
theorem :: SCM_HALT:40 ::TM060
for s being State of SCM+FSA, I being Macro-Instruction holds
I is_closed_onInit s iff I is_closed_on Initialize s;
theorem :: SCM_HALT:41 ::TM062
for s being State of SCM+FSA, I being Macro-Instruction holds
I is_halting_onInit s iff I is_halting_on Initialize s;
theorem :: SCM_HALT:42 ::TM064(SCMFSA8C:17)
for I be Macro-Instruction, s be State of SCM+FSA holds
IExec(I,s) = IExec(I,Initialize s);
theorem :: SCM_HALT:43 ::ThIF0_1'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & I is_closed_onInit s & I is_halting_onInit s holds
if=0(a,I,J) is_closed_onInit s & if=0(a,I,J) is_halting_onInit s;
theorem :: SCM_HALT:44 ::ThIF0_1(@BBB8)
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & I is_closed_onInit s & I is_halting_onInit s holds
IExec(if=0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3);
theorem :: SCM_HALT:45 ::ThIF0_2'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a <> 0 & J is_closed_onInit s & J is_halting_onInit s holds
if=0(a,I,J) is_closed_onInit s & if=0(a,I,J) is_halting_onInit s;
theorem :: SCM_HALT:46 ::ThIF0_2
for I,J being Macro-Instruction, a being read-write Int-Location holds
for s being State of SCM+FSA
st s.a <> 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec(if=0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3)
;
theorem :: SCM_HALT:47 ::=ThIF0
for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction,
a being read-write Int-Location holds
if=0(a,I,J) is InitHalting &
(s.a = 0 implies IExec(if=0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + 3)) &
(s.a <> 0 implies IExec(if=0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + 3));
theorem :: SCM_HALT:48 ::ThIF0'
for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction,
a being read-write Int-Location holds
IC IExec(if=0(a,I,J),s) = insloc (card I + card J + 3) &
(s.a = 0 implies
((for d being Int-Location holds
IExec(if=0(a,I,J),s).d = IExec(I,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,I,J),s).f = IExec(I,s).f)) &
(s.a <> 0 implies
((for d being Int-Location holds
IExec(if=0(a,I,J),s).d = IExec(J,s).d) &
for f being FinSeq-Location holds
IExec(if=0(a,I,J),s).f = IExec(J,s).f));
theorem :: SCM_HALT:49 ::ThIFg0_1'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & I is_closed_onInit s & I is_halting_onInit s holds
if>0(a,I,J) is_closed_onInit s & if>0(a,I,J) is_halting_onInit s;
theorem :: SCM_HALT:50 ::ThIFg0_1
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & I is_closed_onInit s & I is_halting_onInit s holds
IExec(if>0(a,I,J),s) = IExec(I,s) +* Start-At insloc (card I + card J + 3);
theorem :: SCM_HALT:51 ::ThIFg0_2'
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a <= 0 & J is_closed_onInit s & J is_halting_onInit s holds
if>0(a,I,J) is_closed_onInit s & if>0(a,I,J) is_halting_onInit s;
theorem :: SCM_HALT:52 ::ThIFg0_2
for I,J being Macro-Instruction, a being read-write Int-Location holds
for s being State of SCM+FSA
st s.a <= 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec(if>0(a,I,J),s) = IExec(J,s) +* Start-At insloc (card I + card J + 3);
theorem :: SCM_HALT:53 ::ThIFg0
for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction,
a being read-write Int-Location holds
if>0(a,I,J) is InitHalting &
(s.a > 0 implies IExec(if>0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + 3)) &
(s.a <= 0 implies IExec(if>0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + 3));
theorem :: SCM_HALT:54 ::ThIFg0'
for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction,
a being read-write Int-Location holds
IC IExec(if>0(a,I,J),s) = insloc (card I + card J + 3) &
(s.a > 0 implies
((for d being Int-Location holds
IExec(if>0(a,I,J),s).d = IExec(I,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,I,J),s).f = IExec(I,s).f)) &
(s.a <= 0 implies
((for d being Int-Location holds
IExec(if>0(a,I,J),s).d = IExec(J,s).d) &
for f being FinSeq-Location holds
IExec(if>0(a,I,J),s).f = IExec(J,s).f));
theorem :: SCM_HALT:55 ::ThIFl0_1
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a < 0 & I is_closed_onInit s & I is_halting_onInit s holds
IExec(if<0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + card J + 7);
theorem :: SCM_HALT:56 ::ThIFl0_2
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a = 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec(if<0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + card J + 7);
theorem :: SCM_HALT:57 ::ThIFl0_3
for s being State of SCM+FSA, I,J being Macro-Instruction,
a being read-write Int-Location
st s.a > 0 & J is_closed_onInit s & J is_halting_onInit s holds
IExec(if<0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + card J + 7);
theorem :: SCM_HALT:58 ::ThIFl0
for s being State of SCM+FSA, I,J being InitHalting Macro-Instruction,
a being read-write Int-Location holds
(if<0(a,I,J) is InitHalting &
(s.a < 0 implies IExec(if<0(a,I,J),s) =
IExec(I,s) +* Start-At insloc (card I + card J + card J + 7)) &
(s.a >= 0 implies IExec(if<0(a,I,J),s) =
IExec(J,s) +* Start-At insloc (card I + card J + card J + 7)));
definition
let I,J be InitHalting Macro-Instruction;
let a be read-write Int-Location;
cluster if=0(a,I,J) -> InitHalting;
cluster if>0(a,I,J) -> InitHalting;
cluster if<0(a,I,J) -> InitHalting;
end;
theorem :: SCM_HALT:59 ::TM202
for I being Macro-Instruction holds
I is InitHalting iff for s being State of SCM+FSA holds
I is_halting_on Initialize s;
theorem :: SCM_HALT:60 ::TM204
for I being Macro-Instruction holds
I is InitClosed iff for s being State of SCM+FSA holds
I is_closed_on Initialize s;
theorem :: SCM_HALT:61 ::TM206=T200724
for s being State of SCM+FSA, I being InitHalting Macro-Instruction,
a being read-write Int-Location holds
IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).
(LifeSpan (Initialize s +* (I +* Start-At insloc 0))).a;
theorem :: SCM_HALT:62 ::TM208=TMP29
for s being State of SCM+FSA, I being InitHalting Macro-Instruction,
a being Int-Location,k being Nat st I does_not_destroy a holds
IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).k.a;
theorem :: SCM_HALT:63 ::TM209=TMP29''
for s being State of SCM+FSA, I being InitHalting Macro-Instruction,
a being Int-Location st I does_not_destroy a holds
IExec(I,s).a = (Initialize s).a;
theorem :: SCM_HALT:64 ::TM210=TMP27
for s be State of SCM+FSA,I be keepInt0_1 InitHalting Macro-Instruction,
a being read-write Int-Location st I does_not_destroy a holds
(Computation (Initialize s +* (I ';' SubFrom(a,intloc 0) +*
Start-At insloc 0))).(LifeSpan (Initialize s +*
(I ';' SubFrom(a,intloc 0) +* Start-At insloc 0))).a = s.a - 1;
theorem :: SCM_HALT:65 ::MAI1
for s being State of SCM+FSA, I being InitClosed Macro-Instruction
st Initialized I c= s & s is halting
for m being Nat st m <= LifeSpan s
holds (Computation s).m,(Computation (s +* loop I)).m
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:66
for s being State of SCM+FSA, I being InitHalting Macro-Instruction
st Initialized I c= s holds for k being Nat st k <= LifeSpan s holds
CurInstr (Computation (s +* loop I)).k <> halt SCM+FSA;
theorem :: SCM_HALT:67 ::I_SI
I c= s +* Initialized I;
theorem :: SCM_HALT:68 ::TMP24
for s being State of SCM+FSA, I being Macro-Instruction
st I is_closed_onInit s & I is_halting_onInit s
for m being Nat st m <= LifeSpan (s +* Initialized I)
holds (Computation (s +* Initialized I)).m,
(Computation(s +* Initialized (loop I))).m
equal_outside the Instruction-Locations of SCM+FSA;
theorem :: SCM_HALT:69 ::TMP25
for s being State of SCM+FSA, I being Macro-Instruction
st I is_closed_onInit s & I is_halting_onInit s
for m being Nat st m < LifeSpan (s +* Initialized I) holds
CurInstr (Computation (s +* Initialized I)).m =
CurInstr (Computation(s +* Initialized(loop I))).m;
theorem :: SCM_HALT:70 ::InsLoc
for l being Instruction-Location of SCM+FSA holds
not l in dom (((intloc 0) .--> 1) +* Start-At insloc 0);
theorem :: SCM_HALT:71 ::_TMP23
for s being State of SCM+FSA, I being Macro-Instruction
st I is_closed_onInit s & I is_halting_onInit s holds
(CurInstr (Computation (s +* Initialized (loop I))).
LifeSpan (s +* Initialized I) = goto insloc 0 &
for m being Nat st m <= LifeSpan (s +* Initialized I) holds
CurInstr (Computation (s +* Initialized (loop I))).m <> halt SCM+FSA);
theorem :: SCM_HALT:72 ::TMP26
for s being State of SCM+FSA, I being Macro-Instruction
st I is_closed_onInit s & I is_halting_onInit s holds
CurInstr (Computation (s +* Initialized loop I)).
LifeSpan (s +* Initialized I) = goto insloc 0;
theorem :: SCM_HALT:73 ::TMP22
for s being State of SCM+FSA, I being good InitHalting Macro-Instruction,
a being read-write Int-Location st
I does_not_destroy a & s.intloc 0 = 1 & s.a > 0 holds
loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0)) is_pseudo-closed_on s;
theorem :: SCM_HALT:74
for s being State of SCM+FSA, I being good InitHalting Macro-Instruction,
a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds
Initialized loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0))
is_pseudo-closed_on s;
theorem :: SCM_HALT:75
for s being State of SCM+FSA, I being good InitHalting Macro-Instruction,
a being read-write Int-Location
st I does_not_destroy a & s.intloc 0 = 1 holds
Times(a,I) is_closed_on s & Times(a,I) is_halting_on s;
theorem :: SCM_HALT:76 ::Itime
for I being good InitHalting Macro-Instruction,
a being read-write Int-Location st I does_not_destroy a holds
Initialized Times(a,I) is halting;
definition
let a be read-write Int-Location,I be good Macro-Instruction;
cluster Times(a,I) -> good;
end;
theorem :: SCM_HALT:77 ::TMP22'
for s being State of SCM+FSA, I being good InitHalting Macro-Instruction,
a being read-write Int-Location st I does_not_destroy a &
s.a > 0 holds
ex s2 being State of SCM+FSA, k being Nat st
s2 = s +* Initialized (loop if=0(a,Goto insloc 2,
I ';' SubFrom(a,intloc 0))) &
k = LifeSpan (s +* Initialized (if=0(a,Goto insloc 2,
I ';' SubFrom(a,intloc 0)))) + 1 &
(Computation s2).k.a = s.a - 1 &
(Computation s2).k.intloc 0 = 1 &
(for b being read-write Int-Location st b <> a holds
(Computation s2).k.b = IExec(I,s).b) &
(for f being FinSeq-Location holds (Computation s2).k.f = IExec(I,s).f) &
IC (Computation s2).k = insloc 0 &
for n being Nat st n <= k holds
IC (Computation s2).n in
dom loop if=0(a,Goto insloc 2,I ';' SubFrom(a,intloc 0));
theorem :: SCM_HALT:78 ::T1
for s being State of SCM+FSA, I being good InitHalting Macro-Instruction,
a being read-write Int-Location st s.intloc 0 = 1 & s.a <= 0 holds
IExec(Times(a,I),s) | (Int-Locations \/ FinSeq-Locations) =
s | (Int-Locations \/ FinSeq-Locations);
theorem :: SCM_HALT:79 ::T2
for s being State of SCM+FSA, I being good InitHalting Macro-Instruction,
a being read-write Int-Location st I does_not_destroy a & s.a > 0 holds
IExec(I ';' SubFrom(a,intloc 0),s).a = s.a - 1 &
IExec(Times(a,I),s) | (Int-Locations \/ FinSeq-Locations) =
IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)) |
(Int-Locations \/ FinSeq-Locations);
theorem :: SCM_HALT:80 ::T03
for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
f be FinSeq-Location,a be read-write Int-Location st s.a <= 0 holds
IExec(Times(a,I),s).f=s.f;
theorem :: SCM_HALT:81 ::T04
for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
b be Int-Location,a be read-write Int-Location st s.a <= 0 holds
IExec(Times(a,I),s).b=(Initialize s).b;
theorem :: SCM_HALT:82 ::T05
for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
f be FinSeq-Location,a be read-write Int-Location st
I does_not_destroy a & s.a > 0 holds IExec(Times(a,I),s).f
=IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)).f;
theorem :: SCM_HALT:83 ::T06
for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
b be Int-Location,a be read-write Int-Location st
I does_not_destroy a & s.a > 0 holds IExec(Times(a,I),s).b
=IExec(Times(a,I),IExec(I ';' SubFrom(a,intloc 0),s)).b;
definition let i be Instruction of SCM+FSA;
attr i is good means
:: SCM_HALT:def 6
::defB1
i does_not_destroy intloc 0;
end;
definition
cluster parahalting good Instruction of SCM+FSA;
end;
definition
let i be good Instruction of SCM+FSA,
J be good Macro-Instruction;
cluster i ';' J -> good;
cluster J ';' i -> good;
end;
definition
let i,j be good Instruction of SCM+FSA;
cluster i ';' j -> good;
end;
definition
let a be read-write Int-Location,b be Int-Location;
cluster a := b -> good;
cluster SubFrom(a,b) -> good;
end;
definition
let a be read-write Int-Location,b be Int-Location,f be FinSeq-Location;
cluster a:=(f,b) -> good;
end;
definition
let a,b be Int-Location,f be FinSeq-Location;
cluster (f,a):=b -> good;
end;
definition
let a be read-write Int-Location,f be FinSeq-Location;
cluster a:=len f -> good;
end;
definition
let n be Nat;
cluster intloc (n+1) -> read-write;
end;
Back to top