scmfsa9a.miz
begin
reserve p,p1,p2,h for
Instruction-Sequence of
SCM+FSA ;
reserve k,l,n for
Nat,
j for
Integer,
i,i1 for
Instruction of
SCM+FSA ;
theorem ::
SCMFSA9A:1
Th1: (
UsedILoc (l
.--> i))
= (
UsedIntLoc i)
proof
(
rng (l
.--> i))
=
{i} by
FUNCOP_1: 8;
hence (
UsedILoc (l
.--> i))
= (
union { (
UsedIntLoc i1) : i1
in
{i} })
.= (
UsedIntLoc i) from
SUBSET_1:sch 5;
end;
theorem ::
SCMFSA9A:2
Th2: (
UsedI*Loc (l
.--> i))
= (
UsedInt*Loc i)
proof
(
rng (l
.--> i))
=
{i} by
FUNCOP_1: 8;
hence (
UsedI*Loc (l
.--> i))
= (
union { (
UsedInt*Loc i1) : i1
in
{i} })
.= (
UsedInt*Loc i) from
SUBSET_1:sch 5;
end;
theorem ::
SCMFSA9A:3
Th3: (
UsedILoc (
Stop
SCM+FSA ))
=
{} by
Th1,
SF_MASTR: 13;
theorem ::
SCMFSA9A:4
Th4: (
UsedI*Loc (
Stop
SCM+FSA ))
=
{}
proof
thus (
UsedI*Loc (
Stop
SCM+FSA ))
= (
UsedInt*Loc (
halt
SCM+FSA )) by
Th2
.=
{} by
SF_MASTR: 32;
end;
theorem ::
SCMFSA9A:5
Th5: (
UsedILoc (
Goto l))
=
{}
proof
(
Goto l)
= (
Load (
goto l)) by
SCMFSA8A:def 1;
hence (
UsedILoc (
Goto l))
= (
UsedIntLoc (
goto l)) by
Th1
.=
{} by
SF_MASTR: 15;
end;
theorem ::
SCMFSA9A:6
Th6: (
UsedI*Loc (
Goto l))
=
{}
proof
(
Goto l)
= (
Load (
goto l)) by
SCMFSA8A:def 1;
hence (
UsedI*Loc (
Goto l))
= (
UsedInt*Loc (
goto l)) by
Th2
.=
{} by
SF_MASTR: 32;
end;
reserve s,s1,s2 for
State of
SCM+FSA ,
a for
read-write
Int-Location,
b for
Int-Location,
I,J for
MacroInstruction of
SCM+FSA ,
Ig for
good
MacroInstruction of
SCM+FSA ,
i,j,k,m,n for
Nat;
set D = (
Int-Locations
\/
FinSeq-Locations );
set SAt = (
Start-At (
0 ,
SCM+FSA ));
theorem ::
SCMFSA9A:7
(
UsedILoc (
if=0 (b,I,J)))
= ((
{b}
\/ (
UsedILoc I))
\/ (
UsedILoc J))
proof
set I5 = (
Stop
SCM+FSA );
set a = b;
set I1 = (a
=0_goto ((
card J)
+ 3));
set I3 = (
Goto ((
card I)
+ 1));
thus (
UsedILoc (
if=0 (a,I,J)))
= (
UsedILoc ((((I1
";" J)
";" I3)
";" I)
";" I5))
.= ((
UsedILoc (((I1
";" J)
";" I3)
";" I))
\/
{} ) by
Th3,
SF_MASTR: 27
.= ((
UsedILoc ((I1
";" J)
";" I3))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (I1
";" J))
\/ (
UsedILoc I3))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (I1
";" J))
\/
{} )
\/ (
UsedILoc I)) by
Th5
.= (((
UsedIntLoc I1)
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 29
.= ((
{a}
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 16
.= ((
{a}
\/ (
UsedILoc I))
\/ (
UsedILoc J)) by
XBOOLE_1: 4;
end;
theorem ::
SCMFSA9A:8
for a be
Int-Location holds (
UsedI*Loc (
if=0 (a,I,J)))
= ((
UsedI*Loc I)
\/ (
UsedI*Loc J))
proof
set I5 = (
Stop
SCM+FSA );
let a be
Int-Location;
set I1 = (a
=0_goto ((
card J)
+ 3));
set I3 = (
Goto ((
card I)
+ 1));
thus (
UsedI*Loc (
if=0 (a,I,J)))
= (
UsedI*Loc ((((I1
";" J)
";" I3)
";" I)
";" I5))
.= ((
UsedI*Loc (((I1
";" J)
";" I3)
";" I))
\/
{} ) by
Th4,
SF_MASTR: 43
.= ((
UsedI*Loc ((I1
";" J)
";" I3))
\/ (
UsedI*Loc I)) by
SF_MASTR: 43
.= (((
UsedI*Loc (I1
";" J))
\/ (
UsedI*Loc I3))
\/ (
UsedI*Loc I)) by
SF_MASTR: 43
.= (((
UsedI*Loc (I1
";" J))
\/
{} )
\/ (
UsedI*Loc I)) by
Th6
.= (((
UsedInt*Loc I1)
\/ (
UsedI*Loc J))
\/ (
UsedI*Loc I)) by
SF_MASTR: 45
.= ((
{}
\/ (
UsedI*Loc J))
\/ (
UsedI*Loc I)) by
SF_MASTR: 32
.= ((
UsedI*Loc I)
\/ (
UsedI*Loc J));
end;
theorem ::
SCMFSA9A:9
(
UsedILoc (
if>0 (b,I,J)))
= ((
{b}
\/ (
UsedILoc I))
\/ (
UsedILoc J))
proof
set I5 = (
Stop
SCM+FSA );
set a = b;
set I1 = (a
>0_goto ((
card J)
+ 3));
set I3 = (
Goto ((
card I)
+ 1));
thus (
UsedILoc (
if>0 (a,I,J)))
= (
UsedILoc ((((I1
";" J)
";" I3)
";" I)
";" I5))
.= ((
UsedILoc (((I1
";" J)
";" I3)
";" I))
\/
{} ) by
Th3,
SF_MASTR: 27
.= ((
UsedILoc ((I1
";" J)
";" I3))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (I1
";" J))
\/ (
UsedILoc I3))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (I1
";" J))
\/
{} )
\/ (
UsedILoc I)) by
Th5
.= (((
UsedIntLoc I1)
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 29
.= ((
{a}
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 16
.= ((
{a}
\/ (
UsedILoc I))
\/ (
UsedILoc J)) by
XBOOLE_1: 4;
end;
theorem ::
SCMFSA9A:10
(
UsedI*Loc (
if>0 (b,I,J)))
= ((
UsedI*Loc I)
\/ (
UsedI*Loc J))
proof
set I5 = (
Stop
SCM+FSA );
set a = b;
set I1 = (a
>0_goto ((
card J)
+ 3));
set I3 = (
Goto ((
card I)
+ 1));
thus (
UsedI*Loc (
if>0 (a,I,J)))
= (
UsedI*Loc ((((I1
";" J)
";" I3)
";" I)
";" I5))
.= ((
UsedI*Loc (((I1
";" J)
";" I3)
";" I))
\/
{} ) by
Th4,
SF_MASTR: 43
.= ((
UsedI*Loc ((I1
";" J)
";" I3))
\/ (
UsedI*Loc I)) by
SF_MASTR: 43
.= (((
UsedI*Loc (I1
";" J))
\/ (
UsedI*Loc I3))
\/ (
UsedI*Loc I)) by
SF_MASTR: 43
.= (((
UsedI*Loc (I1
";" J))
\/
{} )
\/ (
UsedI*Loc I)) by
Th6
.= (((
UsedInt*Loc I1)
\/ (
UsedI*Loc J))
\/ (
UsedI*Loc I)) by
SF_MASTR: 45
.= ((
{}
\/ (
UsedI*Loc J))
\/ (
UsedI*Loc I)) by
SF_MASTR: 32
.= ((
UsedI*Loc I)
\/ (
UsedI*Loc J));
end;
begin
Lm1: for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds ((
if=0 (a,(I
';' (
goto
0 ))))
. ((
card (I
';' (
goto
0 )))
+ 1))
= (
goto ((
card (I
';' (
goto
0 )))
+ 1))
proof
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
set I1 = (I
';' (
goto
0 ));
set i = (a
=0_goto 3);
set c4 = ((
card I1)
+ 1);
set Mi = (((
Macro i)
";" (
Goto ((
card I1)
+ 1)))
";" I);
A1: (
card Mi)
= (
card ((i
";" (
Goto ((
card I1)
+ 1)))
";" I))
.= ((
card (i
";" (
Goto ((
card I1)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card (
Goto ((
card I1)
+ 1)))
+ 2)
+ (
card I)) by
SCMFSA6A: 33
.= ((1
+ 2)
+ (
card I)) by
SCMFSA8A: 15
.= ((
card I)
+ 3);
A2: (c4
+
0 )
= (((
card I)
+ 1)
+ 1) by
COMPOS_2: 11
.= (((
card I)
+ 3)
- 1)
.= (
LastLoc Mi) by
AFINSQ_1: 91,
A1;
then
A3: c4
= ((
card Mi)
-' 1) by
AFINSQ_1: 70;
(
LastLoc (Mi
';' (
goto
0 )))
= ((
LastLoc Mi)
+ (
LastLoc (
Macro (
goto
0 )))) by
COMPOS_2: 43
.= ((
LastLoc Mi)
+ 1) by
COMPOS_2: 30;
then
A4: c4
< (
LastLoc (Mi
';' (
goto
0 ))) by
A2,
NAT_1: 13;
A5:
0
in (
dom (
Macro (
goto
0 ))) by
AFINSQ_1: 65;
then
A6: ((
Macro (
goto
0 ))
/.
0 )
= ((
Macro (
goto
0 ))
.
0 ) by
PARTFUN1:def 6
.= (
goto
0 ) by
COMPOS_1: 58;
thus ((
if=0 (a,I1))
. c4)
= ((((((a
=0_goto 3)
";" (
Goto ((
card I1)
+ 1)))
";" I)
';' (
goto
0 ))
";" (
Stop
SCM+FSA ))
. c4) by
SCMFSA_X: 35
.= (((((a
=0_goto 3)
";" (
Goto ((
card I1)
+ 1)))
";" I)
';' (
goto
0 ))
. c4) by
A4,
SCMFSA6A: 41
.= ((
IncAddr ((
Macro (
goto
0 )),((
card Mi)
-' 1)))
.
0 ) by
A2,
COMPOS_1: 23
.= (
IncAddr (((
Macro (
goto
0 ))
/.
0 ),((
card Mi)
-' 1))) by
A5,
COMPOS_1:def 21
.= (
IncAddr ((
goto
0 ),c4)) by
A6,
A3
.= (
goto (
0
+ c4)) by
SCMFSA_4: 1
.= (
goto c4);
end;
Lm2: for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds ((
if>0 (a,(I
';' (
goto
0 ))))
. ((
card (I
';' (
goto
0 )))
+ 1))
= (
goto ((
card (I
';' (
goto
0 )))
+ 1))
proof
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
set I1 = (I
';' (
goto
0 ));
set i = (a
>0_goto 3);
set c4 = ((
card I1)
+ 1);
set Mi = (((
Macro i)
";" (
Goto ((
card I1)
+ 1)))
";" I);
A1: (
card Mi)
= (
card ((i
";" (
Goto ((
card I1)
+ 1)))
";" I))
.= ((
card (i
";" (
Goto ((
card I1)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card (
Goto ((
card I1)
+ 1)))
+ 2)
+ (
card I)) by
SCMFSA6A: 33
.= ((1
+ 2)
+ (
card I)) by
SCMFSA8A: 15
.= ((
card I)
+ 3);
A2: (c4
+
0 )
= (((
card I)
+ 1)
+ 1) by
COMPOS_2: 11
.= (((
card I)
+ 3)
- 1)
.= (
LastLoc Mi) by
AFINSQ_1: 91,
A1;
then
A3: c4
= ((
card Mi)
-' 1) by
AFINSQ_1: 70;
(
LastLoc (Mi
';' (
goto
0 )))
= ((
LastLoc Mi)
+ (
LastLoc (
Macro (
goto
0 )))) by
COMPOS_2: 43
.= ((
LastLoc Mi)
+ 1) by
COMPOS_2: 30;
then
A4: c4
< (
LastLoc (Mi
';' (
goto
0 ))) by
A2,
NAT_1: 13;
A5:
0
in (
dom (
Macro (
goto
0 ))) by
AFINSQ_1: 65;
then
A6: ((
Macro (
goto
0 ))
/.
0 )
= ((
Macro (
goto
0 ))
.
0 ) by
PARTFUN1:def 6
.= (
goto
0 ) by
COMPOS_1: 58;
thus ((
if>0 (a,I1))
. c4)
= ((((((a
>0_goto 3)
";" (
Goto ((
card I1)
+ 1)))
";" I)
';' (
goto
0 ))
";" (
Stop
SCM+FSA ))
. c4) by
SCMFSA_X: 36
.= (((((a
>0_goto 3)
";" (
Goto ((
card I1)
+ 1)))
";" I)
';' (
goto
0 ))
. c4) by
A4,
SCMFSA6A: 41
.= ((
IncAddr ((
Macro (
goto
0 )),((
card Mi)
-' 1)))
.
0 ) by
A2,
COMPOS_1: 23
.= (
IncAddr (((
Macro (
goto
0 ))
/.
0 ),((
card Mi)
-' 1))) by
A5,
COMPOS_1:def 21
.= (
IncAddr ((
goto
0 ),c4)) by
A6,
A3
.= (
goto (
0
+ c4)) by
SCMFSA_4: 1
.= (
goto c4);
end;
Lm3: for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds (
UsedILoc (
if=0 (a,(I
';' (
goto
0 )))))
= (
UsedILoc ((
if=0 (a,(I
';' (
goto
0 ))))
+* (((
card I)
+ 2),(
goto
0 ))))
proof
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
set I1 = (I
';' (
goto
0 ));
set Lc4 = ((
card I)
+ 2);
set if0 = (
if=0 (a,I1));
A1: Lc4
= (((
card I)
+ 1)
+ 1)
.= ((
card I1)
+ 1) by
COMPOS_2: 11;
A2: (
card (
if=0 (a,I1)))
= ((
card I1)
+ 4) by
SCMFSA_X: 1;
Lc4
< ((
card I1)
+ 4) by
XREAL_1: 6,
A1;
then
A3: Lc4
in (
dom (
if=0 (a,I1))) by
A2,
AFINSQ_1: 66;
A4: (if0
. Lc4)
in (
rng if0) by
A3,
FUNCT_1: 3;
(
rng if0)
c= the
InstructionsF of
SCM+FSA by
RELAT_1:def 19;
then
reconsider pc = (if0
. Lc4) as
Instruction of
SCM+FSA by
A4;
(
UsedIntLoc pc)
= (
UsedIntLoc (
goto (
0
+ Lc4))) by
Lm1,
A1
.=
{} by
SF_MASTR: 15
.= (
UsedIntLoc (
goto
0 )) by
SF_MASTR: 15;
hence (
UsedILoc if0)
= (
UsedILoc (if0
+* (Lc4,(
goto
0 )))) by
SCMFSA_9: 49;
end;
Lm4: for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds (
UsedI*Loc (
if=0 (a,(I
';' (
goto
0 )))))
= (
UsedI*Loc ((
if=0 (a,(I
';' (
goto
0 ))))
+* (((
card I)
+ 2),(
goto
0 ))))
proof
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
set Lc4 = ((
card I)
+ 2);
set IG = (I
';' (
goto
0 ));
set if0 = (
if=0 (a,IG));
A1: Lc4
= (((
card I)
+ 1)
+ 1)
.= ((
card IG)
+ 1) by
COMPOS_2: 11;
A2: (
card (
if=0 (a,IG)))
= ((
card IG)
+ 4) by
SCMFSA_X: 1;
Lc4
< ((
card IG)
+ 4) by
XREAL_1: 6,
A1;
then
A3: Lc4
in (
dom (
if=0 (a,IG))) by
A2,
AFINSQ_1: 66;
A4: (if0
. Lc4)
in (
rng if0) by
A3,
FUNCT_1: 3;
(
rng if0)
c= the
InstructionsF of
SCM+FSA by
RELAT_1:def 19;
then
reconsider pc = (if0
. Lc4) as
Instruction of
SCM+FSA by
A4;
(
UsedInt*Loc pc)
= (
UsedInt*Loc (
goto (
0
+ Lc4))) by
Lm1,
A1
.=
{} by
SF_MASTR: 32
.= (
UsedInt*Loc (
goto
0 )) by
SF_MASTR: 32;
hence (
UsedI*Loc if0)
= (
UsedI*Loc (if0
+* (Lc4,(
goto
0 )))) by
SCMFSA_9: 50;
end;
theorem ::
SCMFSA9A:11
(
UsedILoc (
while=0 (b,I)))
= (
{b}
\/ (
UsedILoc I))
proof
set J = (
Stop
SCM+FSA );
set a = b;
set IG = (I
';' (
goto
0 ));
A1: (
UsedILoc (I
';' (
goto
0 )))
= (
UsedILoc I) by
SF_MASTR: 66;
thus (
UsedILoc (
while=0 (a,I)))
= (
UsedILoc (
if=0 (a,IG))) by
Lm3
.= ((
UsedILoc (((a
=0_goto 3)
";" (
Goto ((
card IG)
+ 1)))
";" (I
';' (
goto
0 ))))
\/
{} ) by
Th3,
SF_MASTR: 27
.= ((
UsedILoc ((a
=0_goto 3)
";" (
Goto ((
card IG)
+ 1))))
\/ (
UsedILoc I)) by
A1,
SF_MASTR: 27
.= (((
UsedIntLoc (a
=0_goto 3))
\/ (
UsedILoc (
Goto ((
card IG)
+ 1))))
\/ (
UsedILoc I)) by
SF_MASTR: 29
.= (((
UsedIntLoc (a
=0_goto 3))
\/
{} )
\/ (
UsedILoc I)) by
Th5
.= (
{a}
\/ (
UsedILoc I)) by
SF_MASTR: 16;
end;
theorem ::
SCMFSA9A:12
(
UsedI*Loc (
while=0 (b,I)))
= (
UsedI*Loc I)
proof
set J = (
Stop
SCM+FSA );
set a = b;
set IG = (I
';' (
goto
0 ));
A1: (
UsedI*Loc (I
';' (
goto
0 )))
= (
UsedI*Loc I) by
SF_MASTR: 67;
thus (
UsedI*Loc (
while=0 (a,I)))
= (
UsedI*Loc (
if=0 (a,IG))) by
Lm4
.= ((
UsedI*Loc (((a
=0_goto 3)
";" (
Goto ((
card IG)
+ 1)))
";" (I
';' (
goto
0 ))))
\/
{} ) by
Th4,
SF_MASTR: 43
.= ((
UsedI*Loc ((a
=0_goto 3)
";" (
Goto ((
card IG)
+ 1))))
\/ (
UsedI*Loc I)) by
A1,
SF_MASTR: 43
.= (((
UsedInt*Loc (a
=0_goto 3))
\/ (
UsedI*Loc (
Goto ((
card IG)
+ 1))))
\/ (
UsedI*Loc I)) by
SF_MASTR: 45
.= (((
UsedInt*Loc (a
=0_goto 3))
\/
{} )
\/ (
UsedI*Loc I)) by
Th6
.= (
{}
\/ (
UsedI*Loc I)) by
SF_MASTR: 32
.= (
UsedI*Loc I);
end;
definition
let p;
let s be
State of
SCM+FSA , a be
read-write
Int-Location, I be
MacroInstruction of
SCM+FSA ;
::
SCMFSA9A:def1
pred
ProperBodyWhile=0 a,I,s,p means for k be
Nat st (((
StepWhile=0 (a,I,p,s))
. k)
. a)
=
0 holds I
is_halting_on (((
StepWhile=0 (a,I,p,s))
. k),(p
+* (
while=0 (a,I))));
::
SCMFSA9A:def2
pred
WithVariantWhile=0 a,I,s,p means ex f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT st for k be
Nat holds (f
. ((
StepWhile=0 (a,I,p,s))
. (k
+ 1)))
< (f
. ((
StepWhile=0 (a,I,p,s))
. k)) or (((
StepWhile=0 (a,I,p,s))
. k)
. a)
<>
0 ;
end
theorem ::
SCMFSA9A:13
Th13: for I be
parahalting
MacroInstruction of
SCM+FSA holds
ProperBodyWhile=0 (a,I,s,p) by
SCMFSA7B: 19;
theorem ::
SCMFSA9A:14
Th14: for I be
really-closed
MacroInstruction of
SCM+FSA holds
ProperBodyWhile=0 (a,I,s,p) &
WithVariantWhile=0 (a,I,s,p) implies (
while=0 (a,I))
is_halting_on (s,p)
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume
A1: for k be
Nat st (((
StepWhile=0 (a,I,p,s))
. k)
. a)
=
0 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)));
defpred
S[
Nat] means (((
StepWhile=0 (a,I,p,s))
. $1)
. a)
<>
0 ;
given f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A2: for k be
Nat holds ((f
. ((
StepWhile=0 (a,I,p,s))
. (k
+ 1)))
< (f
. ((
StepWhile=0 (a,I,p,s))
. k)) or (((
StepWhile=0 (a,I,p,s))
. k)
. a)
<>
0 );
deffunc
F(
Nat) = (f
. ((
StepWhile=0 (a,I,p,s))
. $1));
A3: for k holds (
F(+)
<
F(k) or
S[k]) by
A2;
consider m be
Nat such that
A4:
S[m] and
A5: for n st
S[n] holds m
<= n from
NAT_1:sch 18(
A3);
defpred
P[
Nat] means ($1
+ 1)
<= m implies ex k st ((
StepWhile=0 (a,I,p,s))
. ($1
+ 1))
= (
Comput (p1,s1,k));
A6:
now
let k be
Nat;
assume
A7:
P[k];
now
set sk1 = ((
StepWhile=0 (a,I,p,s))
. (k
+ 1));
set sk = ((
StepWhile=0 (a,I,p,s))
. k), pk = (p
+* (
while=0 (a,I)));
assume
A8: ((k
+ 1)
+ 1)
<= m;
(k
+
0 )
< (k
+ (1
+ 1)) by
XREAL_1: 6;
then k
< m by
A8,
XXREAL_0: 2;
then
A9: (sk
. a)
=
0 by
A5;
((k
+ 1)
+
0 )
< ((k
+ 1)
+ 1) by
XREAL_1: 6;
then
consider n be
Nat such that
A10: sk1
= (
Comput (p1,s1,n)) by
A7,
A8,
XXREAL_0: 2;
A11: sk1
= (
Comput ((pk
+* (
while=0 (a,I))),(
Initialize sk),((
LifeSpan (((pk
+* (
while=0 (a,I)))
+* I),(
Initialize sk)))
+ 2))) by
SCMFSA_9:def 4;
take m = (n
+ ((
LifeSpan ((pk
+* I),(
Initialize sk1)))
+ 2));
I
is_halting_on (sk,pk) by
A1,
A9;
then (
IC sk1)
=
0 by
A11,
A9,
SCMFSA_9: 22;
then ((
StepWhile=0 (a,I,p,s))
. ((k
+ 1)
+ 1))
= (
Comput (p1,s1,(n
+ ((
LifeSpan ((p1
+* I),(
Initialize ((
StepWhile=0 (a,I,p,s))
. (k
+ 1)))))
+ 2)))) by
A10,
SCMFSA_9: 26;
hence ((
StepWhile=0 (a,I,p,s))
. ((k
+ 1)
+ 1))
= (
Comput (p1,s1,m));
end;
hence
P[(k
+ 1)];
end;
A12:
P[
0 ]
proof
assume (
0
+ 1)
<= m;
take n = ((
LifeSpan ((p1
+* I),(
Initialize s)))
+ 2);
thus thesis by
SCMFSA_9: 25;
end;
A13: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A12,
A6);
per cases ;
suppose m
=
0 ;
then (s
. a)
<>
0 by
A4,
SCMFSA_9:def 4;
hence thesis by
SCMFSA_9: 18;
end;
suppose
A14: m
<>
0 ;
set ii = ((
LifeSpan (((p
+* (
while=0 (a,I)))
+* I),(
Initialize s)))
+ 2);
set sm = ((
StepWhile=0 (a,I,p,s))
. m), pm = (p
+* (
while=0 (a,I)));
set sm1 = (
Initialize sm), pm1 = (pm
+* (
while=0 (a,I)));
consider i be
Nat such that
A15: m
= (i
+ 1) by
A14,
NAT_1: 6;
reconsider i as
Element of
NAT by
ORDINAL1:def 12;
set si = ((
StepWhile=0 (a,I,p,s))
. i), psi = (p
+* (
while=0 (a,I)));
A16: sm
= (
Comput ((psi
+* (
while=0 (a,I))),(
Initialize si),((
LifeSpan ((psi
+* I),(
Initialize si)))
+ 2))) by
A15,
SCMFSA_9:def 4;
m
= (i
+ 1) by
A15;
then
consider n be
Nat such that
A17: sm
= (
Comput (p1,s1,n)) by
A13;
i
< m by
A15,
NAT_1: 13;
then
A18: (si
. a)
=
0 by
A5;
then I
is_halting_on (si,psi) by
A1;
then (
IC sm)
=
0 by
A16,
A18,
SCMFSA_9: 22;
then (
Start-At (
0 ,
SCM+FSA ))
c= sm by
MEMSTR_0: 30;
then
A19: sm1
= sm by
FUNCT_4: 98;
(
while=0 (a,I))
is_halting_on (sm,pm) by
A4,
SCMFSA_9: 18;
then pm1
halts_on sm1 by
SCMFSA7B:def 7;
then
consider j be
Nat such that
A20: (
CurInstr (pm,(
Comput (pm,sm,j))))
= (
halt
SCM+FSA ) by
A19;
A21: (
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,
A20,
A21;
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;
theorem ::
SCMFSA9A:15
Th15: for I be
parahalting
really-closed
MacroInstruction of
SCM+FSA st
WithVariantWhile=0 (a,I,s,p) holds (
while=0 (a,I))
is_halting_on (s,p)
proof
let I be
parahalting
really-closed
MacroInstruction of
SCM+FSA such that
A1:
WithVariantWhile=0 (a,I,s,p);
ProperBodyWhile=0 (a,I,s,p) by
SCMFSA7B: 19;
hence thesis by
A1,
Th14;
end;
theorem ::
SCMFSA9A:16
Th16: for s be
0
-started
State of
SCM+FSA st (
while=0 (a,I))
c= p & (s
. a)
<>
0 holds (
LifeSpan (p,s))
= 3 & for k be
Nat holds (
DataPart (
Comput (p,s,k)))
= (
DataPart s)
proof
let s be
0
-started
State of
SCM+FSA ;
A1: (
Start-At (
0 ,
SCM+FSA ))
c= s by
MEMSTR_0: 29;
assume that
A2: (
while=0 (a,I))
c= p and
A3: (s
. a)
<>
0 ;
A4: (p
+* (
while=0 (a,I)))
= p by
A2,
FUNCT_4: 98;
set i = (a
=0_goto 3);
set s1 = (
Initialize s), p1 = (p
+* (
while=0 (a,I)));
A5: (
while=0 (a,I))
c= p1 by
FUNCT_4: 25;
A6: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
SCMFSA_2: 102;
then
A7: (s1
. a)
= (s
. a) by
FUNCT_4: 11;
A8: 1
in (
dom (
while=0 (a,I))) by
SCMFSA_X: 9;
A9: (p1
. 1)
= ((
while=0 (a,I))
. 1) by
A8,
FUNCT_4: 13
.= (
goto 2) by
SCMFSA_X: 10;
A10: (
IC s1)
= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A6,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
A11: (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
A12: (
CurInstr (p1,s1))
= i by
A10,
A11;
A13: (
Comput (p1,s1,(
0
+ 1)))
= (
Following (p1,(
Comput (p1,s1,
0 )))) by
EXTPRO_1: 3
.= (
Exec (i,s1)) by
A12;
set loc5 = ((
card I)
+ 4);
set s5 = (
Comput (p1,s1,3)), p5 = p1;
set s4 = (
Comput (p1,s1,2)), p4 = p1;
set s2 = (
Comput (p1,s1,1));
A14: 2
in (
dom (
while=0 (a,I))) by
SCMFSA_X: 5;
A15: (p4
. 2)
= ((
while=0 (a,I))
. 2) by
A14,
FUNCT_4: 13
.= (
goto loc5) by
SCMFSA_X: 12;
A16: loc5
in (
dom (
while=0 (a,I))) by
SCMFSA_X: 6;
A17: (p5
. loc5)
= ((
while=0 (a,I))
. loc5) by
A16,
A5,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
SCMFSA_X: 11;
A18: (for c be
Int-Location holds ((
Exec ((
goto loc5),s4))
. c)
= (s4
. c)) & for f be
FinSeq-Location holds ((
Exec ((
goto loc5),s4))
. f)
= (s4
. f) by
SCMFSA_2: 69;
A19: (for c be
Int-Location holds ((
Exec ((
goto 2),s2))
. c)
= (s2
. c)) & for f be
FinSeq-Location holds ((
Exec ((
goto 2),s2))
. f)
= (s2
. f) by
SCMFSA_2: 69;
A20: (p1
/. (
IC (
Comput (p1,s1,1))))
= (p1
. (
IC (
Comput (p1,s1,1)))) by
PBOOLE: 143;
(
IC (
Comput (p1,s1,1)))
= (
0
+ 1) by
A3,
A10,
A13,
A7,
SCMFSA_2: 70;
then
A21: (
CurInstr (p1,(
Comput (p1,s1,1))))
= (
goto 2) by
A9,
A20;
A22: (
Comput (p1,s1,(1
+ 1)))
= (
Following (p1,s2)) by
EXTPRO_1: 3
.= (
Exec ((
goto 2),s2)) by
A21;
A23: (p4
/. (
IC s4))
= (p4
. (
IC s4)) by
PBOOLE: 143;
(
IC s4)
= 2 by
A22,
SCMFSA_2: 69;
then
A24: (
CurInstr (p4,s4))
= (
goto loc5) by
A15,
A23;
A25: (
Comput (p1,s1,(2
+ 1)))
= (
Following (p1,s4)) by
EXTPRO_1: 3
.= (
Exec ((
goto loc5),s4)) by
A24;
A26: (p5
/. (
IC s5))
= (p5
. (
IC s5)) by
PBOOLE: 143;
(
IC s5)
= loc5 by
A25,
SCMFSA_2: 69;
then
A27: (
CurInstr (p5,s5))
= (
halt
SCM+FSA ) by
A17,
A26;
then
A28: p1
halts_on s1 by
EXTPRO_1: 29;
A29: s
= s1 by
A1,
FUNCT_4: 98;
now
let k;
assume
A30: (
CurInstr (p,(
Comput (p,s,k))))
= (
halt
SCM+FSA );
assume 3
> k;
then (2
+ 1)
> k;
then k
<= 2 by
NAT_1: 13;
then k
=
0 or ... or k
= 2;
per cases ;
suppose k
=
0 ;
then (
Comput (p,s,k))
= s;
hence contradiction by
A29,
A12,
A30,
A4;
end;
suppose k
= 1;
hence contradiction by
A29,
A21,
A30,
A4;
end;
suppose k
= 2;
hence contradiction by
A29,
A24,
A30,
A4;
end;
end;
hence
A31: (
LifeSpan (p,s))
= 3 by
A29,
A27,
A28,
A4,
EXTPRO_1:def 15;
A32: (for c be
Int-Location holds ((
Exec (i,s1))
. c)
= (s1
. c)) & for f be
FinSeq-Location holds ((
Exec (i,s1))
. f)
= (s1
. f) by
SCMFSA_2: 70;
then
A33: (
DataPart (
Comput (p,s,1)))
= (
DataPart s) by
A29,
A13,
A4,
SCMFSA_M: 2;
then (
DataPart (
Comput (p,s,2)))
= (
DataPart s) by
A29,
A22,
A19,
A4,
SCMFSA_M: 2;
then
A34: (
DataPart (
Comput (p,s,3)))
= (
DataPart s) by
A29,
A25,
A18,
A4,
SCMFSA_M: 2;
let k be
Nat;
k
<= 2 or 2
< k;
then
A35: (k
=
0 or ... or k
= 2) or (2
+ 1)
<= k by
NAT_1: 13;
per cases by
A35;
suppose k
=
0 ;
hence thesis;
end;
suppose k
= 1;
hence thesis by
A29,
A13,
A32,
A4,
SCMFSA_M: 2;
end;
suppose k
= 2;
hence thesis by
A29,
A22,
A19,
A33,
A4,
SCMFSA_M: 2;
end;
suppose 3
<= k;
then (
CurInstr (p,(
Comput (p,s,k))))
= (
halt
SCM+FSA ) by
A29,
A28,
A31,
A4,
EXTPRO_1: 36;
hence thesis by
A31,
A34,
EXTPRO_1: 24;
end;
end;
theorem ::
SCMFSA9A:17
Th17: for I be
really-closed
MacroInstruction of
SCM+FSA holds I
is_halting_on (s,p) & (s
. a)
=
0 implies (
DataPart (
Comput ((p
+* (
while=0 (a,I))),(
Initialize s),((
LifeSpan ((p
+* I),(
Initialize s)))
+ 2))))
= (
DataPart (
Comput ((p
+* I),(
Initialize s),(
LifeSpan ((p
+* I),(
Initialize s))))))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1: I
is_halting_on (s,p) and
A2: (s
. a)
=
0 ;
set sI = (
Initialize s), pI = (p
+* I);
set s1 = (
Initialize s), p1 = (p
+* (
while=0 (a,I)));
defpred
P[
Nat] means $1
<= (
LifeSpan ((p
+* I),sI)) implies (
IC (
Comput (p1,s1,(1
+ $1))))
= ((
IC (
Comput ((p
+* I),sI,$1)))
+ 3) & (
DataPart (
Comput (p1,s1,(1
+ $1))))
= (
DataPart (
Comput ((p
+* I),sI,$1)));
A3:
now
let k be
Nat;
assume
A4:
P[k];
now
A5: (k
+
0 )
< (k
+ 1) by
XREAL_1: 6;
assume (k
+ 1)
<= (
LifeSpan ((p
+* I),sI));
then k
< (
LifeSpan ((p
+* I),sI)) by
A5,
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,
A4,
SCMFSA_9: 19;
end;
hence
P[(k
+ 1)];
end;
set i = (a
=0_goto 3);
set s2 = (
Comput (p1,s1,1)), p2 = p1;
A6: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A7: (
IC s1)
= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A6,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
SCMFSA_2: 102;
then
A8: (s1
. a)
= (s
. a) by
FUNCT_4: 11;
set loc4 = ((
card I)
+ 2);
A9: (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
A10: (
CurInstr (p1,s1))
= i by
A7,
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 be
Int-Location holds (s2
. c)
= (s1
. c)) & for f be
FinSeq-Location holds (s2
. f)
= (s1
. f) by
SCMFSA_2: 70;
then
A12: (
DataPart s2)
= (
DataPart sI) by
SCMFSA_M: 2;
A13: (
IC s2)
= 3 by
A2,
A11,
A8,
SCMFSA_2: 70;
A14:
P[
0 ]
proof
assume
0
<= (
LifeSpan ((p
+* I),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;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A14,
A3);
then
A16:
P[(
LifeSpan ((p
+* I),sI))];
set s4 = (
Comput (p1,s1,((1
+ (
LifeSpan ((p
+* I),sI)))
+ 1))), p4 = p1;
set s3 = (
Comput (p1,s1,(1
+ (
LifeSpan ((p
+* I),sI))))), p3 = p1;
set s2 = (
Comput (p1,s1,(1
+ (
LifeSpan ((p
+* I),sI)))));
A17: (
CurInstr (p2,s2))
= (
goto
0 ) by
A1,
A16,
SCMFSA_9: 20;
A18: (
CurInstr (p3,s3))
= (
goto
0 ) by
A17;
s4
= (
Following (p1,s3)) by
EXTPRO_1: 3
.= (
Exec ((
goto
0 ),s3)) by
A18;
then (for c be
Int-Location holds (s4
. c)
= (s3
. c)) & for f be
FinSeq-Location holds (s4
. f)
= (s3
. f) by
SCMFSA_2: 69;
hence (
DataPart (
Comput (p1,s1,((
LifeSpan ((p
+* I),sI))
+ 2))))
= (
DataPart s3) by
SCMFSA_M: 2
.= (
DataPart (
Comput (pI,sI,(
LifeSpan ((p
+* I),sI))))) by
A16;
end;
theorem ::
SCMFSA9A:18
Th18: (((
StepWhile=0 (a,I,p,s))
. k)
. a)
<>
0 implies (
DataPart ((
StepWhile=0 (a,I,p,s))
. (k
+ 1)))
= (
DataPart ((
StepWhile=0 (a,I,p,s))
. k))
proof
assume
A1: (((
StepWhile=0 (a,I,p,s))
. k)
. a)
<>
0 ;
set SW = (
StepWhile=0 (a,I,p,s)), PW = (p
+* (
while=0 (a,I)));
A2: (
while=0 (a,I))
c= PW by
FUNCT_4: 25;
A3: (
DataPart (
Initialize (SW
. k)))
= (
DataPart (SW
. k)) by
MEMSTR_0: 79;
then
A4: ((SW
. k)
. a)
= ((
Initialize (SW
. k))
. a) by
SCMFSA_M: 2;
thus (
DataPart (SW
. (k
+ 1)))
= (
DataPart (
Comput ((PW
+* (
while=0 (a,I))),(
Initialize (SW
. k)),((
LifeSpan ((PW
+* I),(
Initialize (SW
. k))))
+ 2)))) by
SCMFSA_9:def 4
.= (
DataPart ((
StepWhile=0 (a,I,p,s))
. k)) by
A1,
A3,
A4,
Th16,
A2;
end;
theorem ::
SCMFSA9A:19
Th19: for I be
really-closed
MacroInstruction of
SCM+FSA holds (I
is_halting_on ((
Initialized ((
StepWhile=0 (a,I,p,s))
. k)),(p
+* (
while=0 (a,I)))) or I is
parahalting) & (((
StepWhile=0 (a,I,p,s))
. k)
. a)
=
0 & (((
StepWhile=0 (a,I,p,s))
. k)
. (
intloc
0 ))
= 1 implies (
DataPart ((
StepWhile=0 (a,I,p,s))
. (k
+ 1)))
= (
DataPart (
IExec (I,(p
+* (
while=0 (a,I))),((
StepWhile=0 (a,I,p,s))
. k))))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
set Ins =
NAT ;
assume that
A1: I
is_halting_on ((
Initialized ((
StepWhile=0 (a,I,p,s))
. k)),(p
+* (
while=0 (a,I)))) or I is
parahalting and
A2: (((
StepWhile=0 (a,I,p,s))
. k)
. a)
=
0 and
A3: (((
StepWhile=0 (a,I,p,s))
. k)
. (
intloc
0 ))
= 1;
set ISWk = (
Initialized ((
StepWhile=0 (a,I,p,s))
. k));
set SW = (
StepWhile=0 (a,I,p,s)), PW = (p
+* (
while=0 (a,I)));
set SWkI = (
Initialized (SW
. k)), PWI = ((p
+* (
while=0 (a,I)))
+* I);
(
DataPart ISWk)
= (
DataPart (SW
. k)) by
A3,
SCMFSA_M: 19;
then
A4: I
is_halting_on ((SW
. k),PW) by
A1,
SCMFSA7B: 19,
SCMFSA8B: 5;
I
is_halting_on (ISWk,PW) by
A1,
SCMFSA7B: 19;
then
A5: I
is_halting_on ((
Initialized (SW
. k)),PW);
(
Initialized (SW
. k))
= (
Initialize (
Initialized (SW
. k))) by
MEMSTR_0: 44;
then
A6: (PW
+* I)
halts_on (
Initialized (SW
. k)) by
A5,
SCMFSA7B:def 7;
A7: PWI
halts_on SWkI by
A6;
set SWkIS = (
Initialize (SW
. k)), PWIS = (PW
+* I);
A8: SWkI
= SWkIS by
A3,
SCMFSA_M: 18;
A9: (SW
. (k
+ 1))
= (
Comput ((PW
+* (
while=0 (a,I))),(
Initialize (SW
. k)),((
LifeSpan (PWIS,SWkIS))
+ 2))) by
SCMFSA_9:def 4;
A10: (
DataPart (
IExec (I,PW,(SW
. k))))
= (
DataPart (
Result (PWI,SWkI))) by
SCMFSA6B:def 1
.= (
DataPart (
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))) by
A8,
A7,
EXTPRO_1: 23;
thus (
DataPart ((
StepWhile=0 (a,I,p,s))
. (k
+ 1)))
= (
DataPart (
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))) by
A2,
A4,
Th17,
A9
.= (
DataPart (
IExec (I,PW,((
StepWhile=0 (a,I,p,s))
. k)))) by
A10;
end;
theorem ::
SCMFSA9A:20
for Ig be
good
really-closed
MacroInstruction of
SCM+FSA holds (
ProperBodyWhile=0 (a,Ig,s,p) or Ig is
parahalting) & (s
. (
intloc
0 ))
= 1 implies for k holds (((
StepWhile=0 (a,Ig,p,s))
. k)
. (
intloc
0 ))
= 1
proof
let Ig be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = Ig;
assume that
A1:
ProperBodyWhile=0 (a,I,s,p) or I is
parahalting and
A2: (s
. (
intloc
0 ))
= 1;
set SW = (
StepWhile=0 (a,I,p,s)), PW = (p
+* (
while=0 (a,I)));
defpred
X[
Nat] means ((SW
. $1)
. (
intloc
0 ))
= 1;
A3: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat such that
A4: ((SW
. k)
. (
intloc
0 ))
= 1;
per cases ;
suppose ((SW
. k)
. a)
<>
0 ;
then (
DataPart (SW
. (k
+ 1)))
= (
DataPart (SW
. k)) by
Th18;
hence thesis by
A4,
SCMFSA_M: 2;
end;
suppose
A5: ((SW
. k)
. a)
=
0 ;
set Ins =
NAT ;
set SWkIS = (
Initialize (SW
. k)), PWIS = (PW
+* I);
set SWkI = (
Initialized (SW
. k)), PWI = ((p
+* (
while=0 (a,I)))
+* I);
set ISWk = (
Initialized ((
StepWhile=0 (a,I,p,s))
. k));
A6: (
DataPart (SW
. k))
= (
DataPart ISWk) by
A4,
SCMFSA_M: 19;
A7:
ProperBodyWhile=0 (a,I,s,p) by
A1,
Th13;
I
is_halting_on ((SW
. k),PW) by
A5,
A7;
then
A8: I
is_halting_on ((
Initialized (SW
. k)),PW) by
A6,
SCMFSA8B: 5;
(
Initialized (SW
. k))
= (
Initialize (
Initialized (SW
. k))) by
MEMSTR_0: 44;
then
A9: (PW
+* I)
halts_on (
Initialized (SW
. k)) by
A8,
SCMFSA7B:def 7;
A10: PWI
halts_on SWkI by
A9;
A11: SWkI
= SWkIS by
A4,
SCMFSA_M: 18;
A12: (
DataPart (
IExec (I,PW,(SW
. k))))
= (
DataPart (
Result (PWI,SWkI))) by
SCMFSA6B:def 1
.= (
DataPart (
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))) by
A11,
A10,
EXTPRO_1: 23;
(
DataPart (SW
. (k
+ 1)))
= (
DataPart (
IExec (I,PW,(SW
. k)))) by
A4,
A5,
A8,
Th19;
hence ((SW
. (k
+ 1))
. (
intloc
0 ))
= ((
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))
. (
intloc
0 )) by
A12,
SCMFSA_M: 2
.= 1 by
A4,
SCMFSA8C: 68;
end;
end;
A13:
X[
0 ] by
A2,
SCMFSA_9:def 4;
thus for k be
Nat holds
X[k] from
NAT_1:sch 2(
A13,
A3);
end;
theorem ::
SCMFSA9A:21
for I be
really-closed
MacroInstruction of
SCM+FSA holds
ProperBodyWhile=0 (a,I,s1,p1) & (
DataPart s1)
= (
DataPart s2) implies for k holds (
DataPart ((
StepWhile=0 (a,I,p1,s1))
. k))
= (
DataPart ((
StepWhile=0 (a,I,p2,s2))
. k))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1:
ProperBodyWhile=0 (a,I,s1,p1) and
A2: (
DataPart s1)
= (
DataPart s2);
set WH = (
while=0 (a,I));
set ST2 = (
StepWhile=0 (a,I,p2,s2)), PT2 = (p2
+* (
while=0 (a,I)));
set ST1 = (
StepWhile=0 (a,I,p1,s1)), PT1 = (p1
+* (
while=0 (a,I)));
defpred
X[
Nat] means (
DataPart (ST1
. $1))
= (
DataPart (ST2
. $1));
A3: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k;
set ST1kI = (
Initialize (ST1
. k)), PT1I = (PT1
+* I);
set ST2kI = (
Initialize (ST2
. k)), PT2I = (PT2
+* I);
A4: I
c= PT1I by
FUNCT_4: 25;
A5: I
c= PT2I by
FUNCT_4: 25;
assume
A6: (
DataPart (ST1
. k))
= (
DataPart (ST2
. k));
then
A7: ((ST1
. k)
. a)
= ((ST2
. k)
. a) by
SCMFSA_M: 2;
per cases ;
suppose
A8: ((ST1
. k)
. a)
<>
0 ;
hence (
DataPart (ST1
. (k
+ 1)))
= (
DataPart (ST1
. k)) by
Th18
.= (
DataPart (ST2
. (k
+ 1))) by
A6,
A7,
A8,
Th18;
end;
suppose
A9: ((ST1
. k)
. a)
=
0 ;
A10: I
is_halting_on ((ST1
. k),PT1) by
A1,
A9;
then
A11: I
is_halting_on ((ST2
. k),PT2) by
A6,
SCMFSA8B: 5;
A12: (
DataPart (ST1
. (k
+ 1)))
= (
DataPart (
Comput ((PT1
+* (
while=0 (a,I))),(
Initialize (ST1
. k)),((
LifeSpan (PT1I,ST1kI))
+ 2)))) by
SCMFSA_9:def 4
.= (
DataPart (
Comput (PT1I,ST1kI,(
LifeSpan (PT1I,ST1kI))))) by
A9,
A10,
Th17;
A13: (
DataPart (ST2
. (k
+ 1)))
= (
DataPart (
Comput ((PT2
+* (
while=0 (a,I))),(
Initialize (ST2
. k)),((
LifeSpan (PT2I,ST2kI))
+ 2)))) by
SCMFSA_9:def 4
.= (
DataPart (
Comput (PT2I,ST2kI,(
LifeSpan (PT2I,ST2kI))))) by
A7,
A9,
A11,
Th17;
A14: (
DataPart (ST1
. k))
= (
DataPart ST1kI) by
MEMSTR_0: 79;
A15: (
DataPart ST1kI)
= (
DataPart (ST1
. k)) by
MEMSTR_0: 79
.= (
DataPart ST2kI) by
A6,
MEMSTR_0: 79;
I
is_halting_on (ST1kI,PT1I) by
A10,
A14,
SCMFSA8B: 5;
then (
LifeSpan (PT1I,ST1kI))
= (
LifeSpan (PT2I,ST2kI)) by
A15,
A4,
A5,
SCMFSA8C: 18;
hence thesis by
A12,
A13,
A15,
A4,
A5,
SCMFSA8C: 17;
end;
end;
(
DataPart (ST1
.
0 ))
= (
DataPart s1) by
SCMFSA_9:def 4
.= (
DataPart (ST2
.
0 )) by
A2,
SCMFSA_9:def 4;
then
A16:
X[
0 ];
thus for k holds
X[k] from
NAT_1:sch 2(
A16,
A3);
end;
definition
let p;
let s be
State of
SCM+FSA , a be
read-write
Int-Location, I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1:
ProperBodyWhile=0 (a,I,s,p) or I is
parahalting and
A2:
WithVariantWhile=0 (a,I,s,p);
::
SCMFSA9A:def3
func
ExitsAtWhile=0 (a,I,p,s) ->
Nat means
:
Def3: ex k be
Nat st it
= k & (((
StepWhile=0 (a,I,p,s))
. k)
. a)
<>
0 & (for i be
Nat st (((
StepWhile=0 (a,I,p,s))
. i)
. a)
<>
0 holds k
<= i) & (
DataPart (
Comput ((p
+* (
while=0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while=0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile=0 (a,I,p,s))
. k));
existence
proof
set S = (
Initialize s), P = (p
+* (
while=0 (a,I)));
set SW = (
StepWhile=0 (a,I,p,s)), PW = (p
+* (
while=0 (a,I)));
A3: (
while=0 (a,I))
c= PW by
FUNCT_4: 25;
defpred
X[
Nat] means ((SW
. $1)
. a)
<>
0 ;
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A4: for k be
Nat holds (f
. (SW
. (k
+ 1)))
< (f
. (SW
. k)) or
X[k] by
A2;
deffunc
U(
Nat) = (f
. (SW
. $1));
A5: for k be
Nat holds
U(+)
<
U(k) or
X[k] by
A4;
consider m such that
A6:
X[m] and
A7: for n st
X[n] holds m
<= n from
NAT_1:sch 18(
A5);
take m, m;
thus m
= m;
thus ((SW
. m)
. a)
<>
0 by
A6;
thus for n st ((SW
. n)
. a)
<>
0 holds m
<= n by
A7;
defpred
P[
Nat] means ($1
+ 1)
<= m implies ex k st ((
StepWhile=0 (a,I,p,s))
. ($1
+ 1))
= (
Comput (P,S,k));
A8:
ProperBodyWhile=0 (a,I,s,p) by
A1,
Th13;
A9:
now
let k be
Nat;
assume
A10:
P[k];
now
set sk1 = ((
StepWhile=0 (a,I,p,s))
. (k
+ 1));
set sk = ((
StepWhile=0 (a,I,p,s))
. k), pk = (p
+* (
while=0 (a,I)));
assume
A11: ((k
+ 1)
+ 1)
<= m;
(k
+
0 )
< (k
+ (1
+ 1)) by
XREAL_1: 6;
then k
< m by
A11,
XXREAL_0: 2;
then
A12: (sk
. a)
=
0 by
A7;
((k
+ 1)
+
0 )
< ((k
+ 1)
+ 1) by
XREAL_1: 6;
then
consider n be
Nat such that
A13: sk1
= (
Comput (P,S,n)) by
A10,
A11,
XXREAL_0: 2;
A14: sk1
= (
Comput ((pk
+* (
while=0 (a,I))),(
Initialize sk),((
LifeSpan ((pk
+* I),(
Initialize sk)))
+ 2))) by
SCMFSA_9:def 4;
take m = (n
+ ((
LifeSpan ((pk
+* I),(
Initialize sk1)))
+ 2));
I
is_halting_on (sk,pk) by
A8,
A12;
then (
IC sk1)
=
0 by
A14,
A12,
SCMFSA_9: 22;
hence ((
StepWhile=0 (a,I,p,s))
. ((k
+ 1)
+ 1))
= (
Comput (P,S,m)) by
A13,
SCMFSA_9: 26;
end;
hence
P[(k
+ 1)];
end;
A15: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A16:
P[
0 ]
proof
assume (
0
+ 1)
<= m;
take n = ((
LifeSpan (((p
+* (
while=0 (a,I)))
+* I),(
Initialize s)))
+ 2);
thus thesis by
SCMFSA_9: 25;
end;
A17: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A16,
A9);
per cases ;
suppose
A18: m
=
0 ;
A19: (
DataPart S)
= (
DataPart s) by
MEMSTR_0: 79
.= (
DataPart (SW
. m)) by
A18,
SCMFSA_9:def 4;
then (S
. a)
= ((SW
. m)
. a) by
SCMFSA_M: 2;
hence thesis by
A6,
A19,
Th16,
A3;
end;
suppose
A20: m
<>
0 ;
set sm = ((
StepWhile=0 (a,I,p,s))
. m), pm = (p
+* (
while=0 (a,I)));
set sm1 = (
Initialize sm), pm1 = (pm
+* (
while=0 (a,I)));
consider i be
Nat such that
A21: m
= (i
+ 1) by
A20,
NAT_1: 6;
reconsider i as
Element of
NAT by
ORDINAL1:def 12;
set si = ((
StepWhile=0 (a,I,p,s))
. i), psi = (p
+* (
while=0 (a,I)));
A22: sm
= (
Comput ((psi
+* (
while=0 (a,I))),(
Initialize si),((
LifeSpan ((psi
+* I),(
Initialize si)))
+ 2))) by
A21,
SCMFSA_9:def 4;
m
= (i
+ 1) by
A21;
then
consider n be
Nat such that
A23: sm
= (
Comput (P,S,n)) by
A17;
i
< m by
A21,
NAT_1: 13;
then
A24: (si
. a)
=
0 by
A7;
then I
is_halting_on (si,psi) by
A8;
then
A25: (
IC sm)
=
0 by
A22,
A24,
SCMFSA_9: 22;
A26: (
IC sm1)
= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A15,
FUNCT_4: 13
.= (
IC sm) by
A25,
FUNCOP_1: 72;
(
DataPart sm1)
= (
DataPart sm) by
MEMSTR_0: 79;
then
A27: sm1
= sm by
A26,
MEMSTR_0: 78;
(
while=0 (a,I))
is_halting_on (sm,pm) by
A6,
SCMFSA_9: 18;
then pm1
halts_on sm1 by
SCMFSA7B:def 7;
then
consider j be
Nat such that
A28: (
CurInstr (pm,(
Comput (pm,sm,j))))
= (
halt
SCM+FSA ) by
A27;
A29: (
Comput (P,S,(n
+ j)))
= (
Comput (P,(
Comput (P,S,n)),j)) by
EXTPRO_1: 4;
(
CurInstr (P,(
Comput (P,S,(n
+ j)))))
= (
halt
SCM+FSA ) by
A23,
A28,
A29;
then
A30: (
Comput (P,S,(
LifeSpan (P,S))))
= (
Comput (P,S,(n
+ j))) by
EXTPRO_1: 24
.= (
Comput (P,sm,j)) by
A23,
EXTPRO_1: 4
.= (
Comput (pm,sm,(
LifeSpan (pm,sm)))) by
A28,
EXTPRO_1: 24;
(
Start-At (
0 ,
SCM+FSA ))
c= sm by
A27,
FUNCT_4: 25;
then sm is
0
-started by
MEMSTR_0: 29;
hence thesis by
A6,
A30,
Th16,
A3;
end;
end;
uniqueness
proof
let it1,it2 be
Nat;
given k1 be
Nat such that
A31: it1
= k1 and
A32: (((
StepWhile=0 (a,I,p,s))
. k1)
. a)
<>
0 & for i be
Nat st (((
StepWhile=0 (a,I,p,s))
. i)
. a)
<>
0 holds k1
<= i and (
DataPart (
Comput ((p
+* (
while=0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while=0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile=0 (a,I,p,s))
. k1));
given k2 be
Nat such that
A33: it2
= k2 and
A34: (((
StepWhile=0 (a,I,p,s))
. k2)
. a)
<>
0 & for i be
Nat st (((
StepWhile=0 (a,I,p,s))
. i)
. a)
<>
0 holds k2
<= i and (
DataPart (
Comput ((p
+* (
while=0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while=0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile=0 (a,I,p,s))
. k2));
k1
<= k2 & k2
<= k1 by
A32,
A34;
hence thesis by
A31,
A33,
XXREAL_0: 1;
end;
end
theorem ::
SCMFSA9A:22
(s
. (
intloc
0 ))
= 1 & (s
. a)
<>
0 implies (
DataPart (
IExec ((
while=0 (a,I)),p,s)))
= (
DataPart s)
proof
set Ins =
NAT ;
assume that
A1: (s
. (
intloc
0 ))
= 1 and
A2: (s
. a)
<>
0 ;
set WH = (
while=0 (a,I));
set Is = (
Initialized s), pds = (p
+* WH);
A3: (
while=0 (a,I))
c= pds by
FUNCT_4: 25;
A4: Is
= (
Initialize Is) by
MEMSTR_0: 44;
(Is
. a)
= (s
. a) by
SCMFSA_M: 37;
then WH
is_halting_on (Is,p) by
A2,
SCMFSA_9: 18;
then
A5: pds
halts_on Is by
A4,
SCMFSA7B:def 7;
A6: (Is
. a)
= (s
. a) by
SCMFSA_M: 37;
thus (
DataPart (
IExec (WH,p,s)))
= (
DataPart (
Result ((p
+* WH),(
Initialized s)))) by
SCMFSA6B:def 1
.= (
DataPart (
Comput (pds,Is,(
LifeSpan (pds,Is))))) by
A5,
EXTPRO_1: 23
.= (
DataPart (
Initialized s)) by
A2,
A6,
Th16,
A3
.= (
DataPart s) by
A1,
SCMFSA_M: 19;
end;
theorem ::
SCMFSA9A:23
for I be
really-closed
MacroInstruction of
SCM+FSA holds (
ProperBodyWhile=0 (a,I,(
Initialized s),p) or I is
parahalting) &
WithVariantWhile=0 (a,I,(
Initialized s),p) implies (
DataPart (
IExec ((
while=0 (a,I)),p,s)))
= (
DataPart ((
StepWhile=0 (a,I,p,(
Initialized s)))
. (
ExitsAtWhile=0 (a,I,p,(
Initialized s)))))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
set Ins =
NAT ;
set WH = (
while=0 (a,I));
set Is = (
Initialized s), pds = (p
+* WH);
A1: Is
= (
Initialize Is) by
MEMSTR_0: 44;
assume
A2: (
ProperBodyWhile=0 (a,I,(
Initialized s),p) or I is
parahalting) &
WithVariantWhile=0 (a,I,(
Initialized s),p);
then
A3: ex k be
Nat st (
ExitsAtWhile=0 (a,I,p,Is))
= k & (((
StepWhile=0 (a,I,p,Is))
. k)
. a)
<>
0 & (for i be
Nat st (((
StepWhile=0 (a,I,p,Is))
. i)
. a)
<>
0 holds k
<= i) & (
DataPart (
Comput ((p
+* (
while=0 (a,I))),(
Initialize Is),(
LifeSpan ((p
+* (
while=0 (a,I))),(
Initialize Is))))))
= (
DataPart ((
StepWhile=0 (a,I,p,Is))
. k)) by
Def3;
WH
is_halting_on (Is,p) by
A2,
Th14,
Th15;
then
A4: pds
halts_on Is by
A1,
SCMFSA7B:def 7;
thus (
DataPart (
IExec ((
while=0 (a,I)),p,s)))
= (
DataPart (
Result ((p
+* WH),(
Initialized s)))) by
SCMFSA6B:def 1
.= (
DataPart ((
StepWhile=0 (a,I,p,Is))
. (
ExitsAtWhile=0 (a,I,p,Is)))) by
A1,
A4,
A3,
EXTPRO_1: 23;
end;
begin
Lm5: for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds (
UsedILoc (
if>0 (a,(I
';' (
goto
0 )))))
= (
UsedILoc ((
if>0 (a,(I
';' (
goto
0 ))))
+* (((
card I)
+ 2),(
goto
0 ))))
proof
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
set I1 = (I
';' (
goto
0 ));
set Lc4 = ((
card I)
+ 2);
set if0 = (
if>0 (a,I1));
A1: Lc4
= (((
card I)
+ 1)
+ 1)
.= ((
card I1)
+ 1) by
COMPOS_2: 11;
A2: (
card (
if>0 (a,I1)))
= ((
card I1)
+ 4) by
SCMFSA_X: 2;
Lc4
< ((
card I1)
+ 4) by
XREAL_1: 6,
A1;
then
A3: Lc4
in (
dom (
if>0 (a,I1))) by
A2,
AFINSQ_1: 66;
A4: (if0
. Lc4)
in (
rng if0) by
A3,
FUNCT_1: 3;
(
rng if0)
c= the
InstructionsF of
SCM+FSA by
RELAT_1:def 19;
then
reconsider pc = (if0
. Lc4) as
Instruction of
SCM+FSA by
A4;
(
UsedIntLoc pc)
= (
UsedIntLoc (
goto (
0
+ Lc4))) by
Lm2,
A1
.=
{} by
SF_MASTR: 15
.= (
UsedIntLoc (
goto
0 )) by
SF_MASTR: 15;
hence (
UsedILoc if0)
= (
UsedILoc (if0
+* (Lc4,(
goto
0 )))) by
SCMFSA_9: 49;
end;
Lm6: for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds (
UsedI*Loc (
if>0 (a,(I
';' (
goto
0 )))))
= (
UsedI*Loc ((
if>0 (a,(I
';' (
goto
0 ))))
+* (((
card I)
+ 2),(
goto
0 ))))
proof
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
set Lc4 = ((
card I)
+ 2);
set IG = (I
';' (
goto
0 ));
set if0 = (
if>0 (a,IG));
A1: Lc4
= (((
card I)
+ 1)
+ 1)
.= ((
card IG)
+ 1) by
COMPOS_2: 11;
A2: (
card (
if>0 (a,IG)))
= ((
card IG)
+ 4) by
SCMFSA_X: 2;
Lc4
< ((
card IG)
+ 4) by
XREAL_1: 6,
A1;
then
A3: Lc4
in (
dom (
if>0 (a,IG))) by
A2,
AFINSQ_1: 66;
A4: (if0
. Lc4)
in (
rng if0) by
A3,
FUNCT_1: 3;
(
rng if0)
c= the
InstructionsF of
SCM+FSA by
RELAT_1:def 19;
then
reconsider pc = (if0
. Lc4) as
Instruction of
SCM+FSA by
A4;
(
UsedInt*Loc pc)
= (
UsedInt*Loc (
goto (
0
+ Lc4))) by
Lm2,
A1
.=
{} by
SF_MASTR: 32
.= (
UsedInt*Loc (
goto
0 )) by
SF_MASTR: 32;
hence (
UsedI*Loc if0)
= (
UsedI*Loc (if0
+* (Lc4,(
goto
0 )))) by
SCMFSA_9: 50;
end;
theorem ::
SCMFSA9A:24
Th24: (
UsedILoc (
while>0 (b,I)))
= (
{b}
\/ (
UsedILoc I))
proof
set J = (
Stop
SCM+FSA );
set a = b;
set IG = (I
';' (
goto
0 ));
A1: (
UsedILoc (I
';' (
goto
0 )))
= (
UsedILoc I) by
SF_MASTR: 66;
thus (
UsedILoc (
while>0 (a,I)))
= (
UsedILoc (
if>0 (a,IG))) by
Lm5
.= ((
UsedILoc (((a
>0_goto 3)
";" (
Goto ((
card IG)
+ 1)))
";" IG))
\/
{} ) by
Th3,
SF_MASTR: 27
.= ((
UsedILoc ((a
>0_goto 3)
";" (
Goto ((
card IG)
+ 1))))
\/ (
UsedILoc I)) by
A1,
SF_MASTR: 27
.= (((
UsedIntLoc (a
>0_goto 3))
\/ (
UsedILoc (
Goto ((
card IG)
+ 1))))
\/ (
UsedILoc I)) by
SF_MASTR: 29
.= (((
UsedIntLoc (a
>0_goto 3))
\/
{} )
\/ (
UsedILoc I)) by
Th5
.= (
{a}
\/ (
UsedILoc I)) by
SF_MASTR: 16;
end;
theorem ::
SCMFSA9A:25
Th25: (
UsedI*Loc (
while>0 (b,I)))
= (
UsedI*Loc I)
proof
set J = (
Stop
SCM+FSA );
set a = b;
set IG = (I
';' (
goto
0 ));
A1: (
UsedI*Loc (I
';' (
goto
0 )))
= (
UsedI*Loc I) by
SF_MASTR: 67;
thus (
UsedI*Loc (
while>0 (a,I)))
= (
UsedI*Loc (
if>0 (a,IG))) by
Lm6
.= ((
UsedI*Loc (((a
>0_goto 3)
";" (
Goto ((
card IG)
+ 1)))
";" IG))
\/
{} ) by
Th4,
SF_MASTR: 43
.= ((
UsedI*Loc ((a
>0_goto 3)
";" (
Goto ((
card IG)
+ 1))))
\/ (
UsedI*Loc I)) by
A1,
SF_MASTR: 43
.= (((
UsedInt*Loc (a
>0_goto 3))
\/ (
UsedI*Loc (
Goto ((
card IG)
+ 1))))
\/ (
UsedI*Loc I)) by
SF_MASTR: 45
.= (((
UsedInt*Loc (a
>0_goto 3))
\/
{} )
\/ (
UsedI*Loc I)) by
Th6
.= (
{}
\/ (
UsedI*Loc I)) by
SF_MASTR: 32
.= (
UsedI*Loc I);
end;
definition
let p;
let s be
State of
SCM+FSA , a be
read-write
Int-Location, I be
MacroInstruction of
SCM+FSA ;
::
SCMFSA9A:def4
pred
ProperBodyWhile>0 a,I,s,p means for k be
Nat st (((
StepWhile>0 (a,I,p,s))
. k)
. a)
>
0 holds I
is_halting_on (((
StepWhile>0 (a,I,p,s))
. k),(p
+* (
while>0 (a,I))));
::
SCMFSA9A:def5
pred
WithVariantWhile>0 a,I,s,p means ex f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT st for k be
Nat holds ((f
. ((
StepWhile>0 (a,I,p,s))
. (k
+ 1)))
< (f
. ((
StepWhile>0 (a,I,p,s))
. k)) or (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 );
end
theorem ::
SCMFSA9A:26
Th26: for I be
parahalting
MacroInstruction of
SCM+FSA holds
ProperBodyWhile>0 (a,I,s,p) by
SCMFSA7B: 19;
theorem ::
SCMFSA9A:27
Th27: for I be
really-closed
MacroInstruction of
SCM+FSA holds
ProperBodyWhile>0 (a,I,s,p) &
WithVariantWhile>0 (a,I,s,p) implies (
while>0 (a,I))
is_halting_on (s,p)
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume
A1: for k be
Nat st (((
StepWhile>0 (a,I,p,s))
. k)
. a)
>
0 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)));
defpred
S[
Nat] means (((
StepWhile>0 (a,I,p,s))
. $1)
. a)
<=
0 ;
given f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A2: for k be
Nat holds ((f
. ((
StepWhile>0 (a,I,p,s))
. (k
+ 1)))
< (f
. ((
StepWhile>0 (a,I,p,s))
. k)) or (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 );
deffunc
F(
Nat) = (f
. ((
StepWhile>0 (a,I,p,s))
. $1));
A3: for k holds
F(+)
<
F(k) or
S[k] by
A2;
consider m be
Nat such that
A4:
S[m] and
A5: for n st
S[n] holds m
<= n from
NAT_1:sch 18(
A3);
defpred
P[
Nat] means ($1
+ 1)
<= m implies ex k st ((
StepWhile>0 (a,I,p,s))
. ($1
+ 1))
= (
Comput (p1,s1,k));
A6:
now
let k be
Nat;
assume
A7:
P[k];
now
set sk1 = ((
StepWhile>0 (a,I,p,s))
. (k
+ 1));
set sk = ((
StepWhile>0 (a,I,p,s))
. k), pk = (p
+* (
while>0 (a,I)));
assume
A8: ((k
+ 1)
+ 1)
<= m;
(k
+
0 )
< (k
+ (1
+ 1)) by
XREAL_1: 6;
then k
< m by
A8,
XXREAL_0: 2;
then
A9: (sk
. a)
>
0 by
A5;
((k
+ 1)
+
0 )
< ((k
+ 1)
+ 1) by
XREAL_1: 6;
then
consider n be
Nat such that
A10: sk1
= (
Comput (p1,s1,n)) by
A7,
A8,
XXREAL_0: 2;
A11: sk1
= (
Comput ((pk
+* (
while>0 (a,I))),(
Initialize sk),((
LifeSpan ((pk
+* I),(
Initialize sk)))
+ 2))) by
SCMFSA_9:def 5;
take m = (n
+ ((
LifeSpan ((pk
+* I),(
Initialize sk1)))
+ 2));
I
is_halting_on (sk,pk) by
A1,
A9;
then (
IC sk1)
=
0 by
A11,
A9,
SCMFSA_9: 42;
hence ((
StepWhile>0 (a,I,p,s))
. ((k
+ 1)
+ 1))
= (
Comput (p1,s1,m)) by
A10,
SCMFSA_9: 45;
end;
hence
P[(k
+ 1)];
end;
A12:
P[
0 ]
proof
assume (
0
+ 1)
<= m;
take n = ((
LifeSpan (((p
+* (
while>0 (a,I)))
+* I),(
Initialize s)))
+ 2);
thus thesis by
SCMFSA_9: 44;
end;
A13: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A12,
A6);
per cases ;
suppose m
=
0 ;
then (s
. a)
<=
0 by
A4,
SCMFSA_9:def 5;
hence thesis by
SCMFSA_9: 38;
end;
suppose
A14: m
<>
0 ;
set ii = ((
LifeSpan (((p
+* (
while>0 (a,I)))
+* I),(
Initialize s)))
+ 2);
set sm = ((
StepWhile>0 (a,I,p,s))
. m), pm = (p
+* (
while>0 (a,I)));
set sm1 = (
Initialize sm), pm1 = (pm
+* (
while>0 (a,I)));
consider i be
Nat such that
A15: m
= (i
+ 1) by
A14,
NAT_1: 6;
reconsider i as
Element of
NAT by
ORDINAL1:def 12;
set si = ((
StepWhile>0 (a,I,p,s))
. i), psi = (p
+* (
while>0 (a,I)));
A16: sm
= (
Comput ((psi
+* (
while>0 (a,I))),(
Initialize si),((
LifeSpan ((psi
+* I),(
Initialize si)))
+ 2))) by
A15,
SCMFSA_9:def 5;
m
= (i
+ 1) by
A15;
then
consider n be
Nat such that
A17: sm
= (
Comput (p1,s1,n)) by
A13;
i
< m by
A15,
NAT_1: 13;
then
A18: (si
. a)
>
0 by
A5;
then I
is_halting_on (si,psi) by
A1;
then (
IC sm)
=
0 by
A16,
A18,
SCMFSA_9: 42;
then (
Start-At (
0 ,
SCM+FSA ))
c= sm by
MEMSTR_0: 30;
then
A19: sm1
= sm by
FUNCT_4: 98;
(
while>0 (a,I))
is_halting_on (sm,pm) by
A4,
SCMFSA_9: 38;
then pm1
halts_on sm1 by
SCMFSA7B:def 7;
then
consider j be
Nat such that
A20: (
CurInstr (pm,(
Comput (pm,sm,j))))
= (
halt
SCM+FSA ) by
A19;
A21: (
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,
A20,
A21;
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;
theorem ::
SCMFSA9A:28
Th28: for I be
parahalting
really-closed
MacroInstruction of
SCM+FSA st
WithVariantWhile>0 (a,I,s,p) holds (
while>0 (a,I))
is_halting_on (s,p)
proof
let I be
parahalting
really-closed
MacroInstruction of
SCM+FSA such that
A1:
WithVariantWhile>0 (a,I,s,p);
ProperBodyWhile>0 (a,I,s,p) by
SCMFSA7B: 19;
hence thesis by
A1,
Th27;
end;
theorem ::
SCMFSA9A:29
Th29: for s be
0
-started
State of
SCM+FSA st (
while>0 (a,I))
c= p & (s
. a)
<=
0 holds (
LifeSpan (p,s))
= 3 & for k be
Nat holds (
DataPart (
Comput (p,s,k)))
= (
DataPart s)
proof
let s be
0
-started
State of
SCM+FSA ;
A1: (
Start-At (
0 ,
SCM+FSA ))
c= s by
MEMSTR_0: 29;
assume that
A2: (
while>0 (a,I))
c= p and
A3: (s
. a)
<=
0 ;
A4: (p
+* (
while>0 (a,I)))
= p by
A2,
FUNCT_4: 98;
set i = (a
>0_goto 3);
set s1 = (
Initialize s), p1 = (p
+* (
while>0 (a,I)));
A5: (
while>0 (a,I))
c= p1 by
FUNCT_4: 25;
A6: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
SCMFSA_2: 102;
then
A7: (s1
. a)
= (s
. a) by
FUNCT_4: 11;
A8: 1
in (
dom (
while>0 (a,I))) by
SCMFSA_X: 9;
A9: (p1
. 1)
= ((
while>0 (a,I))
. 1) by
A8,
FUNCT_4: 13
.= (
goto 2) by
SCMFSA_X: 10;
A10: (
IC s1)
= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A6,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
A11: (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
A12: (
CurInstr (p1,s1))
= i by
A10,
A11;
A13: (
Comput (p1,s1,(
0
+ 1)))
= (
Following (p1,(
Comput (p1,s1,
0 )))) by
EXTPRO_1: 3
.= (
Exec (i,s1)) by
A12;
set loc5 = ((
card I)
+ 4);
set s5 = (
Comput (p1,s1,3)), p5 = p1;
set s4 = (
Comput (p1,s1,2)), p4 = p1;
set s2 = (
Comput (p1,s1,1));
A14: 2
in (
dom (
while>0 (a,I))) by
SCMFSA_X: 7;
A15: (p4
. 2)
= ((
while>0 (a,I))
. 2) by
A14,
FUNCT_4: 13
.= (
goto loc5) by
SCMFSA_X: 17;
A16: loc5
in (
dom (
while>0 (a,I))) by
SCMFSA_X: 8;
A17: (p5
. loc5)
= ((
while>0 (a,I))
. loc5) by
A16,
A5,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
SCMFSA_X: 16;
A18: (for c be
Int-Location holds ((
Exec ((
goto loc5),s4))
. c)
= (s4
. c)) & for f be
FinSeq-Location holds ((
Exec ((
goto loc5),s4))
. f)
= (s4
. f) by
SCMFSA_2: 69;
A19: (for c be
Int-Location holds ((
Exec ((
goto 2),s2))
. c)
= (s2
. c)) & for f be
FinSeq-Location holds ((
Exec ((
goto 2),s2))
. f)
= (s2
. f) by
SCMFSA_2: 69;
A20: (p1
/. (
IC (
Comput (p1,s1,1))))
= (p1
. (
IC (
Comput (p1,s1,1)))) by
PBOOLE: 143;
(
IC (
Comput (p1,s1,1)))
= (
0
+ 1) by
A3,
A10,
A13,
A7,
SCMFSA_2: 71;
then
A21: (
CurInstr (p1,(
Comput (p1,s1,1))))
= (
goto 2) by
A9,
A20;
A22: (
Comput (p1,s1,(1
+ 1)))
= (
Following (p1,s2)) by
EXTPRO_1: 3
.= (
Exec ((
goto 2),s2)) by
A21;
A23: (p4
/. (
IC s4))
= (p4
. (
IC s4)) by
PBOOLE: 143;
(
IC s4)
= 2 by
A22,
SCMFSA_2: 69;
then
A24: (
CurInstr (p4,s4))
= (
goto loc5) by
A15,
A23;
A25: (
Comput (p1,s1,(2
+ 1)))
= (
Following (p1,s4)) by
EXTPRO_1: 3
.= (
Exec ((
goto loc5),s4)) by
A24;
A26: (p5
/. (
IC s5))
= (p5
. (
IC s5)) by
PBOOLE: 143;
(
IC s5)
= loc5 by
A25,
SCMFSA_2: 69;
then
A27: (
CurInstr (p5,s5))
= (
halt
SCM+FSA ) by
A17,
A26;
then
A28: p1
halts_on s1 by
EXTPRO_1: 29;
A29: s
= s1 by
A1,
FUNCT_4: 98;
now
let k;
assume
A30: (
CurInstr (p,(
Comput (p,s,k))))
= (
halt
SCM+FSA );
assume 3
> k;
then (2
+ 1)
> k;
then k
<= 2 by
NAT_1: 13;
then k
=
0 or ... or k
= 2;
per cases ;
suppose k
=
0 ;
then (
Comput (p,s,k))
= s;
hence contradiction by
A29,
A12,
A30,
A4;
end;
suppose k
= 1;
hence contradiction by
A29,
A21,
A30,
A4;
end;
suppose k
= 2;
hence contradiction by
A29,
A24,
A30,
A4;
end;
end;
hence
A31: (
LifeSpan (p,s))
= 3 by
A29,
A27,
A28,
A4,
EXTPRO_1:def 15;
A32: (for c be
Int-Location holds ((
Exec (i,s1))
. c)
= (s1
. c)) & for f be
FinSeq-Location holds ((
Exec (i,s1))
. f)
= (s1
. f) by
SCMFSA_2: 71;
then
A33: (
DataPart (
Comput (p,s,1)))
= (
DataPart s) by
A29,
A13,
A4,
SCMFSA_M: 2;
then (
DataPart (
Comput (p,s,2)))
= (
DataPart s) by
A29,
A22,
A19,
A4,
SCMFSA_M: 2;
then
A34: (
DataPart (
Comput (p,s,3)))
= (
DataPart s) by
A29,
A25,
A18,
A4,
SCMFSA_M: 2;
let k be
Nat;
k
<= 2 or 2
< k;
then
A35: (k
=
0 or ... or k
= 2) or (2
+ 1)
<= k by
NAT_1: 13;
per cases by
A35;
suppose k
=
0 ;
hence thesis;
end;
suppose k
= 1;
hence thesis by
A29,
A13,
A32,
A4,
SCMFSA_M: 2;
end;
suppose k
= 2;
hence thesis by
A29,
A22,
A19,
A33,
A4,
SCMFSA_M: 2;
end;
suppose 3
<= k;
then (
CurInstr (p,(
Comput (p,s,k))))
= (
halt
SCM+FSA ) by
A29,
A28,
A31,
A4,
EXTPRO_1: 36;
hence thesis by
A31,
A34,
EXTPRO_1: 24;
end;
end;
theorem ::
SCMFSA9A:30
Th30: for I be
really-closed
MacroInstruction of
SCM+FSA holds I
is_halting_on (s,p) & (s
. a)
>
0 implies (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize s),((
LifeSpan ((p
+* I),(
Initialize s)))
+ 2))))
= (
DataPart (
Comput ((p
+* I),(
Initialize s),(
LifeSpan ((p
+* I),(
Initialize s))))))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1: I
is_halting_on (s,p) and
A2: (s
. a)
>
0 ;
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)));
A3:
now
let k be
Nat;
assume
A4:
P[k];
now
A5: (k
+
0 )
< (k
+ 1) by
XREAL_1: 6;
assume (k
+ 1)
<= (
LifeSpan (pI,sI));
then k
< (
LifeSpan (pI,sI)) by
A5,
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,
A4,
SCMFSA_9: 39;
end;
hence
P[(k
+ 1)];
end;
set i = (a
>0_goto 3);
set s2 = (
Comput (p1,s1,1)), p2 = p1;
A6: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A7: (
IC s1)
= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A6,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
SCMFSA_2: 102;
then
A8: (s1
. a)
= (s
. a) by
FUNCT_4: 11;
set loc4 = ((
card I)
+ 3);
A9: (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
A10: (
CurInstr (p1,s1))
= i by
A7,
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 be
Int-Location holds (s2
. c)
= (s1
. c)) & for f be
FinSeq-Location holds (s2
. f)
= (s1
. f) by
SCMFSA_2: 71;
then
A12: (
DataPart s2)
= (
DataPart sI) by
SCMFSA_M: 2;
A13: (
IC s2)
= 3 by
A2,
A11,
A8,
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;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A14,
A3);
then
A16:
P[(
LifeSpan (pI,sI))];
set s4 = (
Comput (p1,s1,((1
+ (
LifeSpan (pI,sI)))
+ 1))), p4 = p1;
set s3 = (
Comput (p1,s1,(1
+ (
LifeSpan (pI,sI))))), p3 = p1;
set s2 = (
Comput (p1,s1,(1
+ (
LifeSpan (pI,sI)))));
A17: (
CurInstr (p2,s2))
= (
goto
0 ) by
A1,
A16,
SCMFSA_9: 40;
A18: (
CurInstr (p3,s3))
= (
goto
0 ) by
A17;
s4
= (
Following (p1,s3)) by
EXTPRO_1: 3
.= (
Exec ((
goto
0 ),s3)) by
A18;
then (for c be
Int-Location holds (s4
. c)
= (s3
. c)) & for f be
FinSeq-Location holds (s4
. f)
= (s3
. f) by
SCMFSA_2: 69;
hence (
DataPart (
Comput (p1,s1,((
LifeSpan (pI,sI))
+ 2))))
= (
DataPart s3) by
SCMFSA_M: 2
.= (
DataPart (
Comput (pI,sI,(
LifeSpan (pI,sI))))) by
A16;
end;
theorem ::
SCMFSA9A:31
Th31: (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 implies (
DataPart ((
StepWhile>0 (a,I,p,s))
. (k
+ 1)))
= (
DataPart ((
StepWhile>0 (a,I,p,s))
. k))
proof
assume
A1: (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 ;
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
A2: (
while>0 (a,I))
c= PW by
FUNCT_4: 25;
A3: (
DataPart (
Initialize (SW
. k)))
= (
DataPart (SW
. k)) by
MEMSTR_0: 79;
then
A4: ((SW
. k)
. a)
= ((
Initialize (SW
. k))
. a) by
SCMFSA_M: 2;
thus (
DataPart (SW
. (k
+ 1)))
= (
DataPart (
Comput ((PW
+* (
while>0 (a,I))),(
Initialize (SW
. k)),((
LifeSpan ((PW
+* I),(
Initialize (SW
. k))))
+ 2)))) by
SCMFSA_9:def 5
.= (
DataPart ((
StepWhile>0 (a,I,p,s))
. k)) by
A1,
A3,
A4,
Th29,
A2;
end;
theorem ::
SCMFSA9A:32
Th32: for I be
really-closed
MacroInstruction of
SCM+FSA holds (I
is_halting_on ((
Initialized ((
StepWhile>0 (a,I,p,s))
. k)),(p
+* (
while>0 (a,I)))) or I is
parahalting) & (((
StepWhile>0 (a,I,p,s))
. k)
. a)
>
0 & (((
StepWhile>0 (a,I,p,s))
. k)
. (
intloc
0 ))
= 1 implies (
DataPart ((
StepWhile>0 (a,I,p,s))
. (k
+ 1)))
= (
DataPart (
IExec (I,(p
+* (
while>0 (a,I))),((
StepWhile>0 (a,I,p,s))
. k))))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
set Ins =
NAT ;
assume that
A1: I
is_halting_on ((
Initialized ((
StepWhile>0 (a,I,p,s))
. k)),(p
+* (
while>0 (a,I)))) or I is
parahalting and
A2: (((
StepWhile>0 (a,I,p,s))
. k)
. a)
>
0 and
A3: (((
StepWhile>0 (a,I,p,s))
. k)
. (
intloc
0 ))
= 1;
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
set ISWk = (
Initialized (SW
. k));
set SWkI = (
Initialized (SW
. k)), PWI = ((p
+* (
while>0 (a,I)))
+* I);
(
DataPart ISWk)
= (
DataPart (SW
. k)) by
A3,
SCMFSA_M: 19;
then
A4: I
is_halting_on ((SW
. k),PW) by
A1,
SCMFSA7B: 19,
SCMFSA8B: 5;
I
is_halting_on (ISWk,PW) by
A1,
SCMFSA7B: 19;
then
A5: I
is_halting_on ((
Initialized (SW
. k)),PW);
(
Initialized (SW
. k))
= (
Initialize (
Initialized (SW
. k))) by
MEMSTR_0: 44;
then
A6: (PW
+* I)
halts_on (
Initialized (SW
. k)) by
A5,
SCMFSA7B:def 7;
A7: PWI
halts_on SWkI by
A6;
set SWkIS = (
Initialize (SW
. k)), PWIS = (PW
+* I);
A8: SWkI
= SWkIS by
A3,
SCMFSA_M: 18;
A9: (SW
. (k
+ 1))
= (
Comput ((PW
+* (
while>0 (a,I))),(
Initialize (SW
. k)),((
LifeSpan (PWIS,SWkIS))
+ 2))) by
SCMFSA_9:def 5;
A10: (
DataPart (
IExec (I,PW,(SW
. k))))
= (
DataPart (
Result (PWI,SWkI))) by
SCMFSA6B:def 1
.= (
DataPart (
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))) by
A8,
A7,
EXTPRO_1: 23;
thus (
DataPart ((
StepWhile>0 (a,I,p,s))
. (k
+ 1)))
= (
DataPart (
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))) by
A2,
A4,
Th30,
A9
.= (
DataPart (
IExec (I,PW,((
StepWhile>0 (a,I,p,s))
. k)))) by
A10;
end;
theorem ::
SCMFSA9A:33
Th33: for Ig be
good
really-closed
MacroInstruction of
SCM+FSA holds (
ProperBodyWhile>0 (a,Ig,s,p) or Ig is
parahalting) & (s
. (
intloc
0 ))
= 1 implies for k holds (((
StepWhile>0 (a,Ig,p,s))
. k)
. (
intloc
0 ))
= 1
proof
let Ig be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = Ig;
assume that
A1:
ProperBodyWhile>0 (a,I,s,p) or I is
parahalting and
A2: (s
. (
intloc
0 ))
= 1;
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
defpred
X[
Nat] means ((SW
. $1)
. (
intloc
0 ))
= 1;
A3: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat such that
A4: ((SW
. k)
. (
intloc
0 ))
= 1;
per cases ;
suppose ((SW
. k)
. a)
<=
0 ;
then (
DataPart (SW
. (k
+ 1)))
= (
DataPart (SW
. k)) by
Th31;
hence thesis by
A4,
SCMFSA_M: 2;
end;
suppose
A5: ((SW
. k)
. a)
>
0 ;
set SWkI = (
Initialized (SW
. k)), PWI = ((p
+* (
while>0 (a,I)))
+* I);
A6: (
DataPart (SW
. k))
= (
DataPart SWkI) by
A4,
SCMFSA_M: 19;
set Ins =
NAT ;
set SWkIS = (
Initialize (SW
. k)), PWIS = (PW
+* I);
A7: SWkI
= SWkIS by
A4,
SCMFSA_M: 18;
A8:
ProperBodyWhile>0 (a,I,s,p) by
A1,
Th26;
I
is_halting_on ((SW
. k),PW) by
A5,
A8;
then
A9: I
is_halting_on ((
Initialized (SW
. k)),PW) by
A6,
SCMFSA8B: 5;
(
Initialized (SW
. k))
= (
Initialize (
Initialized (SW
. k))) by
MEMSTR_0: 44;
then
A10: (PW
+* I)
halts_on (
Initialized (SW
. k)) by
A9,
SCMFSA7B:def 7;
A11: PWI
halts_on SWkI by
A10;
A12: (
DataPart (
IExec (I,PW,(SW
. k))))
= (
DataPart (
Result (PWI,SWkI))) by
SCMFSA6B:def 1
.= (
DataPart (
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))) by
A7,
A11,
EXTPRO_1: 23;
(
DataPart (SW
. (k
+ 1)))
= (
DataPart (
IExec (I,PW,(SW
. k)))) by
A4,
A5,
A9,
Th32;
hence ((SW
. (k
+ 1))
. (
intloc
0 ))
= ((
Comput (PWIS,SWkIS,(
LifeSpan (PWIS,SWkIS))))
. (
intloc
0 )) by
A12,
SCMFSA_M: 2
.= 1 by
A4,
SCMFSA8C: 68;
end;
end;
A13:
X[
0 ] by
A2,
SCMFSA_9:def 5;
thus for k be
Nat holds
X[k] from
NAT_1:sch 2(
A13,
A3);
end;
theorem ::
SCMFSA9A:34
Th34: for I be
really-closed
MacroInstruction of
SCM+FSA holds
ProperBodyWhile>0 (a,I,s1,p1) & (
DataPart s1)
= (
DataPart s2) implies for k holds (
DataPart ((
StepWhile>0 (a,I,p1,s1))
. k))
= (
DataPart ((
StepWhile>0 (a,I,p2,s2))
. k))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1:
ProperBodyWhile>0 (a,I,s1,p1) and
A2: (
DataPart s1)
= (
DataPart s2);
set WH = (
while>0 (a,I));
set ST2 = (
StepWhile>0 (a,I,p2,s2)), PT2 = (p2
+* (
while>0 (a,I)));
set ST1 = (
StepWhile>0 (a,I,p1,s1)), PT1 = (p1
+* (
while>0 (a,I)));
defpred
X[
Nat] means (
DataPart (ST1
. $1))
= (
DataPart (ST2
. $1));
A3: for k st
X[k] holds
X[(k
+ 1)]
proof
let k;
set ST1kI = (
Initialize (ST1
. k)), PT1I = (PT1
+* I);
set ST2kI = (
Initialize (ST2
. k)), PT2I = (PT2
+* I);
A4: I
c= PT1I by
FUNCT_4: 25;
A5: I
c= PT2I by
FUNCT_4: 25;
assume
A6: (
DataPart (ST1
. k))
= (
DataPart (ST2
. k));
then
A7: ((ST1
. k)
. a)
= ((ST2
. k)
. a) by
SCMFSA_M: 2;
per cases ;
suppose
A8: ((ST1
. k)
. a)
<=
0 ;
hence (
DataPart (ST1
. (k
+ 1)))
= (
DataPart (ST1
. k)) by
Th31
.= (
DataPart (ST2
. (k
+ 1))) by
A6,
A7,
A8,
Th31;
end;
suppose
A9: ((ST1
. k)
. a)
>
0 ;
A10: I
is_halting_on ((ST1
. k),PT1) by
A1,
A9;
then
A11: I
is_halting_on ((ST2
. k),PT2) by
A6,
SCMFSA8B: 5;
A12: (
DataPart (ST1
. (k
+ 1)))
= (
DataPart (
Comput ((PT1
+* (
while>0 (a,I))),(
Initialize (ST1
. k)),((
LifeSpan (PT1I,ST1kI))
+ 2)))) by
SCMFSA_9:def 5
.= (
DataPart (
Comput (PT1I,ST1kI,(
LifeSpan (PT1I,ST1kI))))) by
A9,
A10,
Th30;
A13: (
DataPart (ST2
. (k
+ 1)))
= (
DataPart (
Comput ((PT2
+* (
while>0 (a,I))),(
Initialize (ST2
. k)),((
LifeSpan (PT2I,ST2kI))
+ 2)))) by
SCMFSA_9:def 5
.= (
DataPart (
Comput (PT2I,ST2kI,(
LifeSpan (PT2I,ST2kI))))) by
A7,
A9,
A11,
Th30;
A14: (
DataPart (ST1
. k))
= (
DataPart ST1kI) by
MEMSTR_0: 79;
A15: (
DataPart ST1kI)
= (
DataPart (ST1
. k)) by
MEMSTR_0: 79
.= (
DataPart ST2kI) by
A6,
MEMSTR_0: 79;
I
is_halting_on (ST1kI,PT1I) by
A10,
A14,
SCMFSA8B: 5;
then (
LifeSpan (PT1I,ST1kI))
= (
LifeSpan (PT2I,ST2kI)) by
A15,
A4,
A5,
SCMFSA8C: 18;
hence thesis by
A12,
A13,
A15,
A4,
A5,
SCMFSA8C: 17;
end;
end;
(
DataPart (ST1
.
0 ))
= (
DataPart s1) by
SCMFSA_9:def 5
.= (
DataPart (ST2
.
0 )) by
A2,
SCMFSA_9:def 5;
then
A16:
X[
0 ];
thus for k holds
X[k] from
NAT_1:sch 2(
A16,
A3);
end;
definition
let p;
let s be
State of
SCM+FSA , a be
read-write
Int-Location, I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1:
ProperBodyWhile>0 (a,I,s,p) or I is
parahalting and
A2:
WithVariantWhile>0 (a,I,s,p);
::
SCMFSA9A:def6
func
ExitsAtWhile>0 (a,I,p,s) ->
Nat means
:
Def6: ex k be
Nat st it
= k & (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 & (for i be
Nat st (((
StepWhile>0 (a,I,p,s))
. i)
. a)
<=
0 holds k
<= i) & (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while>0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile>0 (a,I,p,s))
. k));
existence
proof
set S = (
Initialize s), P = (p
+* (
while>0 (a,I)));
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
A3: (
while>0 (a,I))
c= PW by
FUNCT_4: 25;
defpred
X[
Nat] means ((SW
. $1)
. a)
<=
0 ;
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A4: for k be
Nat holds (f
. (SW
. (k
+ 1)))
< (f
. (SW
. k)) or
X[k] by
A2;
deffunc
U(
Nat) = (f
. (SW
. $1));
A5: for k be
Nat holds
U(+)
<
U(k) or
X[k] by
A4;
consider m such that
A6:
X[m] and
A7: for n st
X[n] holds m
<= n from
NAT_1:sch 18(
A5);
take m, m;
thus m
= m;
thus ((SW
. m)
. a)
<=
0 by
A6;
thus for n st ((SW
. n)
. a)
<=
0 holds m
<= n by
A7;
defpred
P[
Nat] means ($1
+ 1)
<= m implies ex k st ((
StepWhile>0 (a,I,p,s))
. ($1
+ 1))
= (
Comput (P,S,k));
A8:
ProperBodyWhile>0 (a,I,s,p) by
A1,
Th26;
A9:
now
let k be
Nat;
assume
A10:
P[k];
now
set sk1 = ((
StepWhile>0 (a,I,p,s))
. (k
+ 1));
set sk = ((
StepWhile>0 (a,I,p,s))
. k), pk = (p
+* (
while>0 (a,I)));
assume
A11: ((k
+ 1)
+ 1)
<= m;
(k
+
0 )
< (k
+ (1
+ 1)) by
XREAL_1: 6;
then k
< m by
A11,
XXREAL_0: 2;
then
A12: (sk
. a)
>
0 by
A7;
((k
+ 1)
+
0 )
< ((k
+ 1)
+ 1) by
XREAL_1: 6;
then
consider n be
Nat such that
A13: sk1
= (
Comput (P,S,n)) by
A10,
A11,
XXREAL_0: 2;
A14: sk1
= (
Comput ((pk
+* (
while>0 (a,I))),(
Initialize sk),((
LifeSpan ((pk
+* I),(
Initialize sk)))
+ 2))) by
SCMFSA_9:def 5;
take m = (n
+ ((
LifeSpan ((pk
+* I),(
Initialize sk1)))
+ 2));
I
is_halting_on (sk,pk) by
A8,
A12;
then (
IC sk1)
=
0 by
A14,
A12,
SCMFSA_9: 42;
hence ((
StepWhile>0 (a,I,p,s))
. ((k
+ 1)
+ 1))
= (
Comput (P,S,m)) by
A13,
SCMFSA_9: 45;
end;
hence
P[(k
+ 1)];
end;
A15: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A16:
P[
0 ]
proof
assume (
0
+ 1)
<= m;
take n = ((
LifeSpan (((p
+* (
while>0 (a,I)))
+* I),(
Initialize s)))
+ 2);
thus thesis by
SCMFSA_9: 44;
end;
A17: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A16,
A9);
per cases ;
suppose
A18: m
=
0 ;
A19: (
DataPart S)
= (
DataPart s) by
MEMSTR_0: 79
.= (
DataPart (SW
. m)) by
A18,
SCMFSA_9:def 5;
then (S
. a)
= ((SW
. m)
. a) by
SCMFSA_M: 2;
hence thesis by
A6,
A19,
Th29,
A3;
end;
suppose
A20: m
<>
0 ;
set sm = ((
StepWhile>0 (a,I,p,s))
. m), pm = (p
+* (
while>0 (a,I)));
set sm1 = (
Initialize sm), pm1 = (pm
+* (
while>0 (a,I)));
consider i be
Nat such that
A21: m
= (i
+ 1) by
A20,
NAT_1: 6;
reconsider i as
Element of
NAT by
ORDINAL1:def 12;
set si = ((
StepWhile>0 (a,I,p,s))
. i), psi = (p
+* (
while>0 (a,I)));
A22: sm
= (
Comput ((psi
+* (
while>0 (a,I))),(
Initialize si),((
LifeSpan ((psi
+* I),(
Initialize si)))
+ 2))) by
A21,
SCMFSA_9:def 5;
m
= (i
+ 1) by
A21;
then
consider n be
Nat such that
A23: sm
= (
Comput (P,S,n)) by
A17;
i
< m by
A21,
NAT_1: 13;
then
A24: (si
. a)
>
0 by
A7;
then I
is_halting_on (si,psi) by
A8;
then
A25: (
IC sm)
=
0 by
A22,
A24,
SCMFSA_9: 42;
A26: (
IC sm1)
= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A15,
FUNCT_4: 13
.= (
IC sm) by
A25,
FUNCOP_1: 72;
(
DataPart sm1)
= (
DataPart sm) by
MEMSTR_0: 79;
then
A27: sm1
= sm by
A26,
MEMSTR_0: 78;
(
while>0 (a,I))
is_halting_on (sm,pm) by
A6,
SCMFSA_9: 38;
then pm1
halts_on sm1 by
SCMFSA7B:def 7;
then
consider j be
Nat such that
A28: (
CurInstr (pm,(
Comput (pm,sm,j))))
= (
halt
SCM+FSA ) by
A27;
A29: (
Comput (P,S,(n
+ j)))
= (
Comput (P,(
Comput (P,S,n)),j)) by
EXTPRO_1: 4;
(
CurInstr (P,(
Comput (P,S,(n
+ j)))))
= (
halt
SCM+FSA ) by
A23,
A28,
A29;
then
A30: (
Comput (P,S,(
LifeSpan (P,S))))
= (
Comput (P,S,(n
+ j))) by
EXTPRO_1: 24
.= (
Comput (P,sm,j)) by
A23,
EXTPRO_1: 4
.= (
Comput (pm,sm,(
LifeSpan (pm,sm)))) by
A28,
EXTPRO_1: 24;
(
Start-At (
0 ,
SCM+FSA ))
c= sm by
A27,
FUNCT_4: 25;
then sm is
0
-started by
MEMSTR_0: 29;
hence thesis by
A6,
A30,
Th29,
A3;
end;
end;
uniqueness
proof
let it1,it2 be
Nat;
given k1 be
Nat such that
A31: it1
= k1 and
A32: (((
StepWhile>0 (a,I,p,s))
. k1)
. a)
<=
0 & for i be
Nat st (((
StepWhile>0 (a,I,p,s))
. i)
. a)
<=
0 holds k1
<= i and (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while>0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile>0 (a,I,p,s))
. k1));
given k2 be
Nat such that
A33: it2
= k2 and
A34: (((
StepWhile>0 (a,I,p,s))
. k2)
. a)
<=
0 & for i be
Nat st (((
StepWhile>0 (a,I,p,s))
. i)
. a)
<=
0 holds k2
<= i and (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while>0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile>0 (a,I,p,s))
. k2));
k1
<= k2 & k2
<= k1 by
A32,
A34;
hence thesis by
A31,
A33,
XXREAL_0: 1;
end;
end
theorem ::
SCMFSA9A:35
Th35: (s
. (
intloc
0 ))
= 1 & (s
. a)
<=
0 implies (
DataPart (
IExec ((
while>0 (a,I)),p,s)))
= (
DataPart s)
proof
assume that
A1: (s
. (
intloc
0 ))
= 1 and
A2: (s
. a)
<=
0 ;
set WH = (
while>0 (a,I));
set Is = (
Initialized s), pds = (p
+* WH);
A3: (
while>0 (a,I))
c= pds by
FUNCT_4: 25;
A4: Is
= (
Initialize Is) by
MEMSTR_0: 44;
(Is
. a)
= (s
. a) by
SCMFSA_M: 37;
then WH
is_halting_on (Is,p) by
A2,
SCMFSA_9: 38;
then
A5: pds
halts_on Is by
A4,
SCMFSA7B:def 7;
A6: (Is
. a)
= (s
. a) by
SCMFSA_M: 37;
thus (
DataPart (
IExec (WH,p,s)))
= (
DataPart (
Result ((p
+* WH),(
Initialized s)))) by
SCMFSA6B:def 1
.= (
DataPart (
Comput (pds,Is,(
LifeSpan (pds,Is))))) by
A5,
EXTPRO_1: 23
.= (
DataPart (
Initialized s)) by
A2,
A6,
Th29,
A3
.= (
DataPart s) by
A1,
SCMFSA_M: 19;
end;
theorem ::
SCMFSA9A:36
Th36: for I be
really-closed
MacroInstruction of
SCM+FSA holds (
ProperBodyWhile>0 (a,I,(
Initialized s),p) or I is
parahalting) &
WithVariantWhile>0 (a,I,(
Initialized s),p) implies (
DataPart (
IExec ((
while>0 (a,I)),p,s)))
= (
DataPart ((
StepWhile>0 (a,I,p,(
Initialized s)))
. (
ExitsAtWhile>0 (a,I,p,(
Initialized s)))))
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
set Ins =
NAT ;
set WH = (
while>0 (a,I));
set Is = (
Initialized s), pds = (p
+* WH);
A1: Is
= (
Initialize Is) by
MEMSTR_0: 44;
assume
A2: (
ProperBodyWhile>0 (a,I,(
Initialized s),p) or I is
parahalting) &
WithVariantWhile>0 (a,I,(
Initialized s),p);
then
A3: ex k be
Nat st (
ExitsAtWhile>0 (a,I,p,Is))
= k & (((
StepWhile>0 (a,I,p,Is))
. k)
. a)
<=
0 & (for i be
Nat st (((
StepWhile>0 (a,I,p,Is))
. i)
. a)
<=
0 holds k
<= i) & (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize Is),(
LifeSpan ((p
+* (
while>0 (a,I))),(
Initialize Is))))))
= (
DataPart ((
StepWhile>0 (a,I,p,Is))
. k)) by
Def6;
WH
is_halting_on (Is,p) by
A2,
Th27,
Th28;
then
A4: pds
halts_on Is by
A1,
SCMFSA7B:def 7;
thus (
DataPart (
IExec (WH,p,s)))
= (
DataPart (
Result ((p
+* WH),(
Initialized s)))) by
SCMFSA6B:def 1
.= (
DataPart ((
StepWhile>0 (a,I,p,Is))
. (
ExitsAtWhile>0 (a,I,p,Is)))) by
A1,
A4,
A3,
EXTPRO_1: 23;
end;
theorem ::
SCMFSA9A:37
Th37: (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 implies for n be
Nat st k
<= n holds (
DataPart ((
StepWhile>0 (a,I,p,s))
. n))
= (
DataPart ((
StepWhile>0 (a,I,p,s))
. k))
proof
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
defpred
P[
Nat] means k
<= $1 implies (
DataPart (SW
. $1))
= (
DataPart (SW
. k));
assume
A1: (((
StepWhile>0 (a,I,p,s))
. k)
. a)
<=
0 ;
A2:
now
let n be
Nat such that
A3:
P[n];
thus
P[(n
+ 1)]
proof
assume
A4: k
<= (n
+ 1);
per cases by
A4,
NAT_1: 8;
suppose
A5: k
<= n;
then ((SW
. n)
. a)
<=
0 by
A1,
A3,
SCMFSA_M: 2;
hence thesis by
A3,
A5,
Th31;
end;
suppose k
= (n
+ 1);
hence thesis;
end;
end;
end;
A6:
P[
0 ];
thus for n be
Nat holds
P[n] from
NAT_1:sch 2(
A6,
A2);
end;
theorem ::
SCMFSA9A:38
for I be
really-closed
MacroInstruction of
SCM+FSA holds (
DataPart s1)
= (
DataPart s2) &
ProperBodyWhile>0 (a,I,s1,p1) implies
ProperBodyWhile>0 (a,I,s2,p2)
proof
let I be
really-closed
MacroInstruction of
SCM+FSA ;
assume that
A1: (
DataPart s1)
= (
DataPart s2) and
A2:
ProperBodyWhile>0 (a,I,s1,p1);
let k be
Nat such that
A3: (((
StepWhile>0 (a,I,p2,s2))
. k)
. a)
>
0 ;
A4: (
DataPart ((
StepWhile>0 (a,I,p2,s2))
. k))
= (
DataPart ((
StepWhile>0 (a,I,p1,s1))
. k)) by
A1,
A2,
Th34;
then (((
StepWhile>0 (a,I,p1,s1))
. k)
. a)
>
0 by
A3,
SCMFSA_M: 2;
then I
is_halting_on (((
StepWhile>0 (a,I,p1,s1))
. k),(p1
+* (
while>0 (a,I)))) by
A2;
hence thesis by
A4,
SCMFSA8B: 5;
end;
Lm7: for I be
really-closed
Program of
SCM+FSA holds (s
. (
intloc
0 ))
= 1 implies (I
is_halting_on (s,p) iff I
is_halting_on ((
Initialized s),p))
proof
let I be
really-closed
Program of
SCM+FSA ;
assume (s
. (
intloc
0 ))
= 1;
then (
DataPart (
Initialized s))
= (
DataPart s) by
SCMFSA_M: 19;
hence thesis by
SCMFSA8B: 5;
end;
theorem ::
SCMFSA9A:39
Th39: for Ig be
good
really-closed
MacroInstruction of
SCM+FSA holds (s
. (
intloc
0 ))
= 1 &
ProperBodyWhile>0 (a,Ig,s,p) &
WithVariantWhile>0 (a,Ig,s,p) implies for i, j st i
<> j & i
<= (
ExitsAtWhile>0 (a,Ig,p,s)) & j
<= (
ExitsAtWhile>0 (a,Ig,p,s)) holds ((
StepWhile>0 (a,Ig,p,s))
. i)
<> ((
StepWhile>0 (a,Ig,p,s))
. j) & (
DataPart ((
StepWhile>0 (a,Ig,p,s))
. i))
<> (
DataPart ((
StepWhile>0 (a,Ig,p,s))
. j))
proof
let Ig be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = Ig;
assume that
A1: (s
. (
intloc
0 ))
= 1 and
A2:
ProperBodyWhile>0 (a,I,s,p) and
A3:
WithVariantWhile>0 (a,I,s,p);
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
consider K be
Nat such that
A4: (
ExitsAtWhile>0 (a,I,p,s))
= K and
A5: ((SW
. K)
. a)
<=
0 and
A6: for i be
Nat st ((SW
. i)
. a)
<=
0 holds K
<= i and (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while>0 (a,I))),(s
+* (
Start-At (
0 ,
SCM+FSA ))))))))
= (
DataPart (SW
. K)) by
A2,
A3,
Def6;
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A7: for k be
Nat holds (f
. (SW
. (k
+ 1)))
< (f
. (SW
. k)) or ((SW
. k)
. a)
<=
0 by
A3;
A8: for i,j be
Nat st i
< j & i
<= K & j
<= K holds (
DataPart (SW
. i))
<> (
DataPart (SW
. j))
proof
let i,j be
Nat such that
A9: i
< j and i
<= K and
A10: j
<= K;
per cases by
A10,
XXREAL_0: 1;
suppose
A11: j
= K;
assume (
DataPart (SW
. i))
= (
DataPart (SW
. j));
then ((SW
. i)
. a)
<=
0 by
A5,
A11,
SCMFSA_M: 2;
hence contradiction by
A6,
A9,
A11;
end;
suppose
A12: j
< K;
defpred
X[
Nat] means (j
+ $1)
<= K implies (
DataPart (SW
. (i
+ $1)))
= (
DataPart (SW
. (j
+ $1)));
A13: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat such that
A14: (j
+ k)
<= K implies (
DataPart (SW
. (i
+ k)))
= (
DataPart (SW
. (j
+ k))) and
A15: (j
+ (k
+ 1))
<= K;
A16: ((SW
. (j
+ k))
. (
intloc
0 ))
= 1 by
A1,
A2,
Th33;
A17: (j
+ k)
< ((j
+ k)
+ 1) by
XREAL_1: 29;
then
A18: (j
+ k)
< K by
A15,
XXREAL_0: 2;
then
A19: ((SW
. (j
+ k))
. a)
>
0 by
A6;
A20: I
is_halting_on ((SW
. (j
+ k)),PW) by
A2,
A19;
then
A21: I
is_halting_on ((
Initialized (SW
. (j
+ k))),PW) by
A16,
Lm7;
A22: ((SW
. (i
+ k))
. (
intloc
0 ))
= 1 by
A1,
A2,
Th33;
A23: ((SW
. (i
+ k))
. a)
>
0
proof
assume not thesis;
then
A24: K
<= (i
+ k) by
A6;
(i
+ k)
< (j
+ k) by
A9,
XREAL_1: 6;
hence contradiction by
A18,
A24,
XXREAL_0: 2;
end;
I
is_halting_on ((SW
. (i
+ k)),PW) by
A2,
A23;
then
A25: I
is_halting_on ((
Initialized (SW
. (i
+ k))),PW) by
A22,
Lm7;
thus (
DataPart (SW
. (i
+ (k
+ 1))))
= (
DataPart (SW
. ((i
+ k)
+ 1)))
.= (
DataPart (
IExec (I,PW,(SW
. (i
+ k))))) by
A22,
A23,
A25,
Th32
.= (
DataPart (
IExec (I,PW,(SW
. (j
+ k))))) by
A14,
A15,
A17,
A16,
A20,
SCMFSA8C: 20,
XXREAL_0: 2
.= (
DataPart (SW
. ((j
+ k)
+ 1))) by
A16,
A19,
A21,
Th32
.= (
DataPart (SW
. (j
+ (k
+ 1))));
end;
consider p be
Element of
NAT such that
A26: K
= (j
+ p) and 1
<= p by
A12,
FINSEQ_4: 84;
assume (
DataPart (SW
. i))
= (
DataPart (SW
. j));
then
A27:
X[
0 ];
for k be
Nat holds
X[k] from
NAT_1:sch 2(
A27,
A13);
then (
DataPart (SW
. (i
+ p)))
= (
DataPart (SW
. K)) by
A26;
then
A28: ((SW
. (i
+ p))
. a)
<=
0 by
A5,
SCMFSA_M: 2;
(i
+ p)
< K by
A9,
A26,
XREAL_1: 6;
hence contradiction by
A6,
A28;
end;
end;
A29: for i,j be
Nat st i
< j & i
<= K & j
<= K holds (SW
. i)
<> (SW
. j)
proof
let i,j be
Nat;
assume that
A30: i
< j and i
<= K and
A31: j
<= K;
defpred
X[
Nat] means i
< $1 & $1
<= j implies (f
. (SW
. $1))
< (f
. (SW
. i));
A32: i
< K by
A30,
A31,
XXREAL_0: 2;
A33: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat such that
A34: i
< k & k
<= j implies (f
. (SW
. k))
< (f
. (SW
. i)) and
A35: i
< (k
+ 1) and
A36: (k
+ 1)
<= j;
A37: i
<= k by
A35,
NAT_1: 13;
per cases by
A37,
XXREAL_0: 1;
suppose
A38: i
= k;
not ((SW
. i)
. a)
<=
0 by
A6,
A32;
hence thesis by
A7,
A38;
end;
suppose
A39: i
< k;
A40: k
< j by
A36,
NAT_1: 13;
now
assume ((SW
. k)
. a)
<=
0 ;
then K
<= k by
A6;
hence contradiction by
A31,
A40,
XXREAL_0: 2;
end;
then (f
. (SW
. (k
+ 1)))
< (f
. (SW
. k)) by
A7;
hence thesis by
A34,
A36,
A39,
NAT_1: 13,
XXREAL_0: 2;
end;
end;
assume
A41: (SW
. i)
= (SW
. j);
A42:
X[
0 ];
for k be
Nat holds
X[k] from
NAT_1:sch 2(
A42,
A33);
hence contradiction by
A30,
A41;
end;
given i,j be
Nat such that
A43: i
<> j and
A44: i
<= (
ExitsAtWhile>0 (a,I,p,s)) & j
<= (
ExitsAtWhile>0 (a,I,p,s)) & ((SW
. i)
= (SW
. j) or (
DataPart (SW
. i))
= (
DataPart (SW
. j)));
i
< j or j
< i by
A43,
XXREAL_0: 1;
hence contradiction by
A4,
A29,
A8,
A44;
end;
::$Canceled
theorem ::
SCMFSA9A:40
Th40: for Ig be
good
really-closed
MacroInstruction of
SCM+FSA holds (s
. (
intloc
0 ))
= 1 &
ProperBodyWhile>0 (a,Ig,s,p) &
WithVariantWhile>0 (a,Ig,s,p) implies ex f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT st f is
on_data_only & for k be
Nat holds (f
. ((
StepWhile>0 (a,Ig,p,s))
. (k
+ 1)))
< (f
. ((
StepWhile>0 (a,Ig,p,s))
. k)) or (((
StepWhile>0 (a,Ig,p,s))
. k)
. a)
<=
0
proof
let Ig be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = Ig;
assume that
A1: (s
. (
intloc
0 ))
= 1 and
A2:
ProperBodyWhile>0 (a,I,s,p) and
A3:
WithVariantWhile>0 (a,I,s,p);
set SW = (
StepWhile>0 (a,I,p,s)), PW = (p
+* (
while>0 (a,I)));
consider K be
Nat such that
A4: (
ExitsAtWhile>0 (a,I,p,s))
= K and
A5: ((SW
. K)
. a)
<=
0 and for i be
Nat st ((SW
. i)
. a)
<=
0 holds K
<= i and (
DataPart (
Comput ((p
+* (
while>0 (a,I))),(
Initialize s),(
LifeSpan ((p
+* (
while>0 (a,I))),(
Initialize s))))))
= (
DataPart ((
StepWhile>0 (a,I,p,s))
. K)) by
A2,
A3,
Def6;
consider g be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A6: for k be
Nat holds (g
. (SW
. (k
+ 1)))
< (g
. (SW
. k)) or ((SW
. k)
. a)
<=
0 by
A3;
defpred
P[
State of
SCM+FSA ,
set] means (ex k be
Nat st k
<= K & (
DataPart $1)
= (
DataPart (SW
. k)) & $2
= (g
. (SW
. k))) or not (ex k be
Nat st k
<= K & (
DataPart $1)
= (
DataPart (SW
. k))) & $2
=
0 ;
A7: for x be
Element of (
product (
the_Values_of
SCM+FSA )) holds ex y be
Element of
NAT st
P[x, y]
proof
let x be
Element of (
product (
the_Values_of
SCM+FSA ));
per cases ;
suppose ex k be
Nat st k
<= K & (
DataPart x)
= (
DataPart (SW
. k));
then
consider k be
Nat such that
A8: k
<= K & (
DataPart x)
= (
DataPart (SW
. k));
take (g
. (SW
. k));
thus thesis by
A8;
end;
suppose
A9: not ex k be
Nat st k
<= K & (
DataPart x)
= (
DataPart (SW
. k));
take
0 ;
thus thesis by
A9;
end;
end;
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A10: for x be
Element of (
product (
the_Values_of
SCM+FSA )) holds
P[x, (f
. x)] from
FUNCT_2:sch 3(
A7);
take f;
hereby
let s1, s2 such that
A11: (
DataPart s1)
= (
DataPart s2);
reconsider ss1 = s1, ss2 = s2 as
Element of (
product (
the_Values_of
SCM+FSA )) by
CARD_3: 107;
P[ss1, (f
. ss1)] &
P[ss2, (f
. ss2)] by
A10;
hence (f
. s1)
= (f
. s2) by
A1,
A2,
A3,
A4,
A11,
Th39;
end;
let k be
Nat;
per cases ;
suppose
A12: k
< K;
then
A13: (k
+ 1)
<= K by
NAT_1: 13;
then
consider kk1 be
Nat such that
A14: kk1
<= K & (
DataPart (SW
. (k
+ 1)))
= (
DataPart (SW
. kk1)) and
A15: (f
. (SW
. (k
+ 1)))
= (g
. (SW
. kk1)) by
A10;
A16: (k
+ 1)
= kk1 by
A1,
A2,
A3,
A4,
A13,
A14,
Th39;
consider kk be
Nat such that
A17: kk
<= K & (
DataPart (SW
. k))
= (
DataPart (SW
. kk)) and
A18: (f
. (SW
. k))
= (g
. (SW
. kk)) by
A10,
A12;
k
= kk by
A1,
A2,
A3,
A4,
A12,
A17,
Th39;
hence thesis by
A6,
A18,
A15,
A16;
end;
suppose K
<= k;
then (
DataPart (SW
. K))
= (
DataPart (SW
. k)) by
A5,
Th37;
hence thesis by
A5,
SCMFSA_M: 2;
end;
end;
theorem ::
SCMFSA9A:41
for Ig be
good
really-closed
MacroInstruction of
SCM+FSA holds (s1
. (
intloc
0 ))
= 1 & (
DataPart s1)
= (
DataPart s2) &
ProperBodyWhile>0 (a,Ig,s1,p1) &
WithVariantWhile>0 (a,Ig,s1,p1) implies
WithVariantWhile>0 (a,Ig,s2,p2)
proof
let Ig be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = Ig;
assume that
A1: (s1
. (
intloc
0 ))
= 1 and
A2: (
DataPart s1)
= (
DataPart s2) and
A3:
ProperBodyWhile>0 (a,I,s1,p1) and
A4:
WithVariantWhile>0 (a,I,s1,p1);
set SW1 = (
StepWhile>0 (a,I,p1,s1));
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A5: f is
on_data_only and
A6: for k be
Nat holds ((f
. (SW1
. (k
+ 1)))
< (f
. (SW1
. k)) or ((SW1
. k)
. a)
<=
0 ) by
A1,
A3,
A4,
Th40;
take f;
let k be
Nat;
set SW2 = (
StepWhile>0 (a,I,p2,s2));
(
DataPart (SW1
. (k
+ 1)))
= (
DataPart (SW2
. (k
+ 1))) by
A2,
A3,
Th34;
then
A7: (f
. (SW1
. (k
+ 1)))
= (f
. (SW2
. (k
+ 1))) by
A5;
A8: (
DataPart (SW1
. k))
= (
DataPart (SW2
. k)) by
A2,
A3,
Th34;
then
A9: ((SW1
. k)
. a)
= ((SW2
. k)
. a) by
SCMFSA_M: 2;
(f
. (SW1
. k))
= (f
. (SW2
. k)) by
A5,
A8;
hence thesis by
A6,
A9,
A7;
end;
begin
definition
let N,result be
Int-Location;
::
SCMFSA9A:def7
func
Fusc_macro (N,result) ->
MacroInstruction of
SCM+FSA equals ((((
SubFrom (result,result))
";" ((1
-stRWNotIn
{N, result})
:= (
intloc
0 )))
";" ((2
-ndRWNotIn
{N, result})
:= N))
";" (
while>0 ((2
-ndRWNotIn
{N, result}),((((3
-rdRWNotIn
{N, result})
:= 2)
";" (
Divide ((2
-ndRWNotIn
{N, result}),(3
-rdRWNotIn
{N, result}))))
";" (
if=0 ((3
-rdRWNotIn
{N, result}),(
Macro (
AddTo ((1
-stRWNotIn
{N, result}),result))),(
Macro (
AddTo (result,(1
-stRWNotIn
{N, result})))) qua
MacroInstruction of
SCM+FSA ))))));
correctness ;
end
registration
let N,R be
read-write
Int-Location;
cluster (
Fusc_macro (N,R)) ->
really-closed;
coherence ;
end
theorem ::
SCMFSA9A:42
for N,result be
read-write
Int-Location st N
<> result holds for n be
Element of
NAT st n
= (s
. N) holds ((
IExec ((
Fusc_macro (N,result)),p,s))
. result)
= (
Fusc n) & ((
IExec ((
Fusc_macro (N,result)),p,s))
. N)
= n
proof
let N,result be
read-write
Int-Location such that
A1: N
<> result;
set i0 = (
SubFrom (result,result));
set rem2 = (3
-rdRWNotIn
{N, result});
set aux = (2
-ndRWNotIn
{N, result});
set next = (1
-stRWNotIn
{N, result});
set I3i0 = (rem2
:= 2);
set I3i1 = (
Divide (aux,rem2));
set I3I2I0 = (
Macro (
AddTo (next,result)));
set I3I2I1 = (
Macro (
AddTo (result,next)));
reconsider I3I2 = (
if=0 (rem2,I3I2I0,I3I2I1)) as
really-closed
Program of
SCM+FSA ;
reconsider I = ((I3i0
";" I3i1)
";" I3I2) as
really-closed
MacroInstruction of
SCM+FSA ;
let n be
Element of
NAT such that
A2: n
= (s
. N);
A3: next
<> rem2 by
SCMFSA_M: 26;
A4: aux
<> next by
SCMFSA_M: 26;
set I3 = (
while>0 (aux,I));
deffunc
U(
Element of (
product (
the_Values_of
SCM+FSA ))) =
|.($1
. aux).|;
set i2 = (aux
:= N);
set i1 = (next
:= (
intloc
0 ));
set t = (
IExec (((i0
";" i1)
";" i2),p,s)), q = p;
set It = (
Initialized t);
set SWt = (
StepWhile>0 (aux,I,q,It)), PWt = (q
+* (
while>0 (aux,I)));
defpred
X[
Nat] means ex au,ne,re be
Nat st ((SWt
. $1)
. aux)
= au & ((SWt
. $1)
. next)
= ne & ((SWt
. $1)
. result)
= re & ((SWt
. $1)
. N)
= n & (
Fusc n)
= ((ne
* (
Fusc au))
+ (re
* (
Fusc (au
+ 1))));
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A5: for x be
Element of (
product (
the_Values_of
SCM+FSA )) holds (f
. x)
=
U(x) from
FUNCT_2:sch 4;
A6: N
in
{N, result} by
TARSKI:def 2;
then
A7: N
<> next by
SCMFSA_M: 25;
A8: result
in
{N, result} by
TARSKI:def 2;
then
A9: aux
<> result by
SCMFSA_M: 25;
A10: result
<> rem2 by
A8,
SCMFSA_M: 25;
A11: next
<> result by
A8,
SCMFSA_M: 25;
A12: N
<> rem2 by
A6,
SCMFSA_M: 25;
A13: N
<> aux by
A6,
SCMFSA_M: 25;
A14: aux
<> rem2 by
SCMFSA_M: 26;
A15: for u be
State of
SCM+FSA , h st ex au,ne,re be
Nat st (u
. aux)
= au & (u
. next)
= ne & (u
. result)
= re & (u
. N)
= n & (
Fusc n)
= ((ne
* (
Fusc au))
+ (re
* (
Fusc (au
+ 1)))) holds ex au1,ne1,re1 be
Nat st ((
IExec (I,h,u))
. aux)
= au1 & ((
IExec (I,h,u))
. next)
= ne1 & ((
IExec (I,h,u))
. result)
= re1 & ((
IExec (I,h,u))
. N)
= n & (
Fusc n)
= ((ne1
* (
Fusc au1))
+ (re1
* (
Fusc (au1
+ 1)))) & au1
= ((u
. aux)
div 2)
proof
let u be
State of
SCM+FSA , h;
given au,ne,re be
Nat such that
A16: (u
. aux)
= au and
A17: (u
. next)
= ne and
A18: (u
. result)
= re and
A19: (u
. N)
= n and
A20: (
Fusc n)
= ((ne
* (
Fusc au))
+ (re
* (
Fusc (au
+ 1))));
A21: ((
Initialized (
IExec ((I3i0
";" I3i1),h,u)))
. next)
= ((
IExec ((I3i0
";" I3i1),h,u))
. next) by
SCMFSA_M: 37
.= ((
Exec (I3i1,(
IExec (I3i0,h,u))))
. next) by
SCMFSA6C: 6
.= ((
IExec (I3i0,h,u))
. next) by
A4,
A3,
SCMFSA_2: 67
.= ne by
A17,
SCMFSA7B: 3,
SCMFSA_M: 26;
A22: ((
Initialized (
IExec ((I3i0
";" I3i1),h,u)))
. aux)
= ((
IExec ((I3i0
";" I3i1),h,u))
. aux) by
SCMFSA_M: 37
.= ((
Exec (I3i1,(
IExec (I3i0,h,u))))
. aux) by
SCMFSA6C: 6
.= (((
IExec (I3i0,h,u))
. aux)
div ((
IExec (I3i0,h,u))
. rem2)) by
A14,
SCMFSA_2: 67
.= ((u
. aux)
div ((
IExec (I3i0,h,u))
. rem2)) by
SCMFSA7B: 3,
SCMFSA_M: 26
.= ((u
. aux)
div 2) by
SCMFSA7B: 3;
A23: ((
Initialized (
IExec ((I3i0
";" I3i1),h,u)))
. result)
= ((
IExec ((I3i0
";" I3i1),h,u))
. result) by
SCMFSA_M: 37
.= ((
Exec (I3i1,(
IExec (I3i0,h,u))))
. result) by
SCMFSA6C: 6
.= ((
IExec (I3i0,h,u))
. result) by
A9,
A10,
SCMFSA_2: 67
.= re by
A10,
A18,
SCMFSA7B: 3;
A24: ((
Initialized (
IExec ((I3i0
";" I3i1),h,u)))
. N)
= ((
IExec ((I3i0
";" I3i1),h,u))
. N) by
SCMFSA_M: 37
.= ((
Exec (I3i1,(
IExec (I3i0,h,u))))
. N) by
SCMFSA6C: 6
.= ((
IExec (I3i0,h,u))
. N) by
A12,
A13,
SCMFSA_2: 67
.= n by
A12,
A19,
SCMFSA7B: 3;
A25: ((
IExec ((I3i0
";" I3i1),h,u))
. rem2)
= ((
Exec (I3i1,(
IExec (I3i0,h,u))))
. rem2) by
SCMFSA6C: 6
.= (((
IExec (I3i0,h,u))
. aux)
mod ((
IExec (I3i0,h,u))
. rem2)) by
SCMFSA_2: 67
.= ((u
. aux)
mod ((
IExec (I3i0,h,u))
. rem2)) by
SCMFSA7B: 3,
SCMFSA_M: 26
.= ((u
. aux)
mod 2) by
SCMFSA7B: 3;
per cases ;
suppose
A26: au is
even;
reconsider ne1 = (ne
+ re) as
Element of
NAT by
ORDINAL1:def 12;
reconsider au1 = ((u
. aux)
div 2) as
Element of
NAT by
A16,
INT_1: 3,
INT_1: 55;
take au1, ne1, re;
consider k be
Nat such that
A27: au
= (2
* k) by
A26,
ABIAN:def 2;
A28: ((u
. aux)
mod 2)
= (((2
* k)
+
0 )
mod 2) by
A16,
A27
.= (
0
mod 2) by
NAT_D: 21
.=
0 by
NAT_D: 26;
((
IExec (I,h,u))
. aux)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. aux) by
SCMFSA6C: 1
.= ((
IExec (I3I2I0,h,(
IExec ((I3i0
";" I3i1),h,u))))
. aux) by
A25,
A28,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (next,result)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. aux) by
SCMFSA6C: 5
.= ((u
. aux)
div 2) by
A4,
A22,
SCMFSA_2: 64;
hence ((
IExec (I,h,u))
. aux)
= au1;
thus ((
IExec (I,h,u))
. next)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. next) by
SCMFSA6C: 1
.= ((
IExec (I3I2I0,h,(
IExec ((I3i0
";" I3i1),h,u))))
. next) by
A25,
A28,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (next,result)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. next) by
SCMFSA6C: 5
.= ne1 by
A21,
A23,
SCMFSA_2: 64;
thus ((
IExec (I,h,u))
. result)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. result) by
SCMFSA6C: 1
.= ((
IExec (I3I2I0,h,(
IExec ((I3i0
";" I3i1),h,u))))
. result) by
A25,
A28,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (next,result)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. result) by
SCMFSA6C: 5
.= re by
A11,
A23,
SCMFSA_2: 64;
thus ((
IExec (I,h,u))
. N)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. N) by
SCMFSA6C: 1
.= ((
IExec (I3I2I0,h,(
IExec ((I3i0
";" I3i1),h,u))))
. N) by
A25,
A28,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (next,result)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. N) by
SCMFSA6C: 5
.= n by
A7,
A24,
SCMFSA_2: 64;
au1
= k by
A16,
A27,
NAT_D: 18;
hence (
Fusc n)
= ((ne1
* (
Fusc au1))
+ (re
* (
Fusc (au1
+ 1)))) by
A20,
A27,
PRE_FF: 20;
thus thesis;
end;
suppose
A29: au is
odd;
reconsider re1 = (ne
+ re) as
Element of
NAT by
ORDINAL1:def 12;
reconsider au1 = ((u
. aux)
div 2) as
Element of
NAT by
A16,
INT_1: 3,
INT_1: 55;
take au1, ne, re1;
consider k be
Nat such that
A30: au
= ((2
* k)
+ 1) by
A29,
ABIAN: 9;
A31: ((u
. aux)
mod 2)
= (1
mod 2) by
A16,
A30,
NAT_D: 21
.= 1 by
NAT_D: 24;
((
IExec (I,h,u))
. aux)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. aux) by
SCMFSA6C: 1
.= ((
IExec (I3I2I1,h,(
IExec ((I3i0
";" I3i1),h,u))))
. aux) by
A25,
A31,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (result,next)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. aux) by
SCMFSA6C: 5
.= ((u
. aux)
div 2) by
A9,
A22,
SCMFSA_2: 64;
hence ((
IExec (I,h,u))
. aux)
= au1;
thus ((
IExec (I,h,u))
. next)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. next) by
SCMFSA6C: 1
.= ((
IExec (I3I2I1,h,(
IExec ((I3i0
";" I3i1),h,u))))
. next) by
A25,
A31,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (result,next)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. next) by
SCMFSA6C: 5
.= ne by
A11,
A21,
SCMFSA_2: 64;
thus ((
IExec (I,h,u))
. result)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. result) by
SCMFSA6C: 1
.= ((
IExec (I3I2I1,h,(
IExec ((I3i0
";" I3i1),h,u))))
. result) by
A25,
A31,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (result,next)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. result) by
SCMFSA6C: 5
.= re1 by
A21,
A23,
SCMFSA_2: 64;
thus ((
IExec (I,h,u))
. N)
= ((
IExec (I3I2,h,(
IExec ((I3i0
";" I3i1),h,u))))
. N) by
SCMFSA6C: 1
.= ((
IExec (I3I2I1,h,(
IExec ((I3i0
";" I3i1),h,u))))
. N) by
A25,
A31,
SCMFSA8B: 18
.= ((
Exec ((
AddTo (result,next)),(
Initialized (
IExec ((I3i0
";" I3i1),h,u)))))
. N) by
SCMFSA6C: 5
.= n by
A1,
A24,
SCMFSA_2: 64;
au1
= ((2
* k)
div 2) by
A16,
A30,
NAT_2: 26
.= k by
NAT_D: 18;
hence (
Fusc n)
= ((ne
* (
Fusc au1))
+ (re1
* (
Fusc (au1
+ 1)))) by
A20,
A30,
PRE_FF: 19;
thus thesis;
end;
end;
A32: (It
. (
intloc
0 ))
= 1 by
SCMFSA_M: 9;
A33: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat;
given au,ne,re be
Nat such that
A34: ((SWt
. k)
. aux)
= au and
A35: ((SWt
. k)
. next)
= ne and
A36: ((SWt
. k)
. result)
= re and
A37: ((SWt
. k)
. N)
= n and
A38: (
Fusc n)
= ((ne
* (
Fusc au))
+ (re
* (
Fusc (au
+ 1))));
A39: ((SWt
. k)
. (
intloc
0 ))
= 1 by
A32,
Th33;
per cases ;
suppose
A40: ((SWt
. k)
. aux)
>
0 ;
consider au1,ne1,re1 be
Nat such that
A41: ((
IExec (I,PWt,(SWt
. k)))
. aux)
= au1 and
A42: ((
IExec (I,PWt,(SWt
. k)))
. next)
= ne1 and
A43: ((
IExec (I,PWt,(SWt
. k)))
. result)
= re1 and
A44: ((
IExec (I,PWt,(SWt
. k)))
. N)
= n and
A45: (
Fusc n)
= ((ne1
* (
Fusc au1))
+ (re1
* (
Fusc (au1
+ 1)))) and au1
= (((SWt
. k)
. aux)
div 2) by
A15,
A34,
A35,
A36,
A37,
A38;
take au1, ne1, re1;
A46: (
DataPart (SWt
. (k
+ 1)))
= (
DataPart (
IExec (I,PWt,(SWt
. k)))) by
A39,
A40,
Th32;
hence ((SWt
. (k
+ 1))
. aux)
= au1 by
A41,
SCMFSA_M: 2;
thus ((SWt
. (k
+ 1))
. next)
= ne1 by
A46,
A42,
SCMFSA_M: 2;
thus ((SWt
. (k
+ 1))
. result)
= re1 by
A46,
A43,
SCMFSA_M: 2;
thus ((SWt
. (k
+ 1))
. N)
= n by
A46,
A44,
SCMFSA_M: 2;
thus thesis by
A45;
end;
suppose
A47: ((SWt
. k)
. aux)
<=
0 ;
take au, ne, re;
A48: (
DataPart (SWt
. (k
+ 1)))
= (
DataPart (SWt
. k)) by
A47,
Th31;
hence ((SWt
. (k
+ 1))
. aux)
= au by
A34,
SCMFSA_M: 2;
thus ((SWt
. (k
+ 1))
. next)
= ne by
A35,
A48,
SCMFSA_M: 2;
thus ((SWt
. (k
+ 1))
. result)
= re by
A36,
A48,
SCMFSA_M: 2;
thus ((SWt
. (k
+ 1))
. N)
= n by
A37,
A48,
SCMFSA_M: 2;
thus thesis by
A38;
end;
end;
(t
. (
intloc
0 ))
= 1 by
SCMFSA6B: 11;
then
A49: (
DataPart t)
= (
DataPart It) by
SCMFSA_M: 19;
A50:
X[
0 ]
proof
take au = n;
take ne = 1;
take re =
0 ;
A51: (SWt
.
0 )
= It by
SCMFSA_9:def 5;
hence ((SWt
.
0 )
. aux)
= (t
. aux) by
A49,
SCMFSA_M: 2
.= ((
Exec (i2,(
IExec ((i0
";" i1),p,s))))
. aux) by
SCMFSA6C: 6
.= ((
IExec ((i0
";" i1),p,s))
. N) by
SCMFSA_2: 63
.= ((
Exec (i1,(
Exec (i0,(
Initialized s)))))
. N) by
SCMFSA6C: 8
.= ((
Exec (i0,(
Initialized s)))
. N) by
A7,
SCMFSA_2: 63
.= ((
Initialized s)
. N) by
A1,
SCMFSA_2: 65
.= au by
A2,
SCMFSA_M: 37;
thus ((SWt
.
0 )
. next)
= (t
. next) by
A49,
A51,
SCMFSA_M: 2
.= ((
Exec (i2,(
IExec ((i0
";" i1),p,s))))
. next) by
SCMFSA6C: 6
.= ((
IExec ((i0
";" i1),p,s))
. next) by
A4,
SCMFSA_2: 63
.= ((
Exec (i1,(
Exec (i0,(
Initialized s)))))
. next) by
SCMFSA6C: 8
.= ((
Exec (i0,(
Initialized s)))
. (
intloc
0 )) by
SCMFSA_2: 63
.= ((
Initialized s)
. (
intloc
0 )) by
SCMFSA_2: 65
.= ne by
SCMFSA_M: 9;
thus ((SWt
.
0 )
. result)
= (t
. result) by
A49,
A51,
SCMFSA_M: 2
.= ((
Exec (i2,(
IExec ((i0
";" i1),p,s))))
. result) by
SCMFSA6C: 6
.= ((
IExec ((i0
";" i1),p,s))
. result) by
A9,
SCMFSA_2: 63
.= ((
Exec (i1,(
Exec (i0,(
Initialized s)))))
. result) by
SCMFSA6C: 8
.= ((
Exec (i0,(
Initialized s)))
. result) by
A11,
SCMFSA_2: 63
.= (((
Initialized s)
. result)
- ((
Initialized s)
. result)) by
SCMFSA_2: 65
.= re;
thus ((SWt
.
0 )
. N)
= (t
. N) by
A49,
A51,
SCMFSA_M: 2
.= ((
Exec (i2,(
IExec ((i0
";" i1),p,s))))
. N) by
SCMFSA6C: 6
.= ((
IExec ((i0
";" i1),p,s))
. N) by
A13,
SCMFSA_2: 63
.= ((
Exec (i1,(
Exec (i0,(
Initialized s)))))
. N) by
SCMFSA6C: 8
.= ((
Exec (i0,(
Initialized s)))
. N) by
A7,
SCMFSA_2: 63
.= ((
Initialized s)
. N) by
A1,
SCMFSA_2: 65
.= n by
A2,
SCMFSA_M: 37;
thus thesis;
end;
A52: for k be
Nat holds
X[k] from
NAT_1:sch 2(
A50,
A33);
for k be
Nat holds (f
. (SWt
. (k
+ 1)))
< (f
. (SWt
. k)) or ((SWt
. k)
. aux)
<=
0
proof
let k be
Nat;
consider au,ne,re be
Nat such that
A53: ((SWt
. k)
. aux)
= au and
A54: ((SWt
. k)
. next)
= ne & ((SWt
. k)
. result)
= re & ((SWt
. k)
. N)
= n & (
Fusc n)
= ((ne
* (
Fusc au))
+ (re
* (
Fusc (au
+ 1)))) by
A52;
A55: (f
. (SWt
. k))
=
|.((SWt
. k)
. aux).| by
A5
.= au by
A53,
ABSVALUE:def 1;
now
consider au1,ne1,re1 be
Nat such that
A56: ((
IExec (I,PWt,(SWt
. k)))
. aux)
= au1 and ((
IExec (I,PWt,(SWt
. k)))
. next)
= ne1 and ((
IExec (I,PWt,(SWt
. k)))
. result)
= re1 and ((
IExec (I,PWt,(SWt
. k)))
. N)
= n and (
Fusc n)
= ((ne1
* (
Fusc au1))
+ (re1
* (
Fusc (au1
+ 1)))) and
A57: au1
= (((SWt
. k)
. aux)
div 2) by
A15,
A53,
A54;
assume
A58: au
>
0 ;
((SWt
. k)
. (
intloc
0 ))
= 1 by
A32,
Th33;
then (
DataPart (SWt
. (k
+ 1)))
= (
DataPart (
IExec (I,PWt,(SWt
. k)))) by
A53,
A58,
Th32;
then
A59: ((SWt
. (k
+ 1))
. aux)
= au1 by
A56,
SCMFSA_M: 2;
(f
. (SWt
. (k
+ 1)))
=
|.((SWt
. (k
+ 1))
. aux).| by
A5
.= au1 by
A59,
ABSVALUE:def 1;
hence (f
. (SWt
. (k
+ 1)))
< (f
. (SWt
. k)) by
A53,
A55,
A58,
A57,
INT_1: 56;
end;
hence thesis by
A53;
end;
then
A60:
WithVariantWhile>0 (aux,I,It,q);
then
consider k be
Nat such that
A61: (
ExitsAtWhile>0 (aux,I,q,It))
= k and
A62: (((
StepWhile>0 (aux,I,q,It))
. k)
. aux)
<=
0 and for i be
Nat st ((SWt
. i)
. aux)
<=
0 holds k
<= i and (
DataPart (
Comput ((q
+* (
while>0 (aux,I))),(
Initialize It),(
LifeSpan ((q
+* (
while>0 (aux,I))),(
Initialize It))))))
= (
DataPart ((
StepWhile>0 (aux,I,q,It))
. k)) by
Def6;
A63: (
DataPart (
IExec (I3,q,t)))
= (
DataPart (SWt
. k)) by
A60,
A61,
Th36;
consider au,ne,re be
Nat such that
A64: ((SWt
. k)
. aux)
= au and ((SWt
. k)
. next)
= ne and
A65: ((SWt
. k)
. result)
= re and
A66: ((SWt
. k)
. N)
= n and
A67: (
Fusc n)
= ((ne
* (
Fusc au))
+ (re
* (
Fusc (au
+ 1)))) by
A52;
A68: au
=
0 by
A62,
A64;
I3
is_halting_on (It,q) by
A60,
Th28;
then
A69: I3
is_halting_on (t,q) by
A49,
SCMFSA8B: 5;
hence ((
IExec ((
Fusc_macro (N,result)),p,s))
. result)
= ((
IExec (I3,q,t))
. result) by
SFMASTR1: 7
.= (
Fusc n) by
A65,
A67,
A68,
A63,
PRE_FF: 15,
SCMFSA_M: 2;
thus ((
IExec ((
Fusc_macro (N,result)),p,s))
. N)
= ((
IExec (I3,q,t))
. N) by
A69,
SFMASTR1: 7
.= n by
A66,
A63,
SCMFSA_M: 2;
end;
theorem ::
SCMFSA9A:43
for I,J be
MacroInstruction of
SCM+FSA , a be
Int-Location holds (
UsedILoc (
if=0 (a,I,J)))
= ((
{a}
\/ (
UsedILoc I))
\/ (
UsedILoc J)) & (
UsedILoc (
if>0 (a,I,J)))
= ((
{a}
\/ (
UsedILoc I))
\/ (
UsedILoc J))
proof
let I,J be
MacroInstruction of
SCM+FSA , a be
Int-Location;
set g1 = (a
=0_goto ((
card J)
+ 3)), g2 = (
Goto ((
card I)
+ 1)), g3 = (a
>0_goto ((
card J)
+ 3)), SS = (
Stop
SCM+FSA );
thus (
UsedILoc (
if=0 (a,I,J)))
= (
UsedILoc ((((g1
";" J)
";" g2)
";" I)
";" SS))
.= ((
UsedILoc (((g1
";" J)
";" g2)
";" I))
\/
{} ) by
Th3,
SF_MASTR: 27
.= ((
UsedILoc ((g1
";" J)
";" g2))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (g1
";" J))
\/ (
UsedILoc g2))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (g1
";" J))
\/
{} )
\/ (
UsedILoc I)) by
Th5
.= (((
UsedIntLoc g1)
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 29
.= ((
{a}
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 16
.= ((
{a}
\/ (
UsedILoc I))
\/ (
UsedILoc J)) by
XBOOLE_1: 4;
thus (
UsedILoc (
if>0 (a,I,J)))
= (
UsedILoc ((((g3
";" J)
";" g2)
";" I)
";" SS))
.= ((
UsedILoc (((g3
";" J)
";" g2)
";" I))
\/
{} ) by
Th3,
SF_MASTR: 27
.= ((
UsedILoc ((g3
";" J)
";" g2))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (g3
";" J))
\/ (
UsedILoc g2))
\/ (
UsedILoc I)) by
SF_MASTR: 27
.= (((
UsedILoc (g3
";" J))
\/
{} )
\/ (
UsedILoc I)) by
Th5
.= (((
UsedIntLoc g3)
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 29
.= ((
{a}
\/ (
UsedILoc J))
\/ (
UsedILoc I)) by
SF_MASTR: 16
.= ((
{a}
\/ (
UsedILoc I))
\/ (
UsedILoc J)) by
XBOOLE_1: 4;
end;
theorem ::
SCMFSA9A:44
(
UsedILoc (
Times (b,I)))
= (
{b, (
intloc
0 )}
\/ (
UsedILoc I))
proof
thus (
UsedILoc (
Times (b,I)))
= (
{b}
\/ (
UsedILoc (I
";" (
SubFrom (b,(
intloc
0 )))))) by
Th24
.= (
{b}
\/ ((
UsedILoc I)
\/ (
UsedIntLoc (
SubFrom (b,(
intloc
0 )))))) by
SF_MASTR: 30
.= (
{b}
\/ ((
UsedILoc I)
\/
{b, (
intloc
0 )})) by
SF_MASTR: 14
.= ((
{b}
\/
{b, (
intloc
0 )})
\/ (
UsedILoc I)) by
XBOOLE_1: 4
.= (
{b, (
intloc
0 )}
\/ (
UsedILoc I)) by
ZFMISC_1: 9;
end;
theorem ::
SCMFSA9A:45
(
UsedI*Loc (
Times (b,I)))
= (
UsedI*Loc I)
proof
thus (
UsedI*Loc (
Times (b,I)))
= (
UsedI*Loc (I
";" (
SubFrom (b,(
intloc
0 ))))) by
Th25
.= ((
UsedI*Loc I)
\/ (
UsedInt*Loc (
SubFrom (b,(
intloc
0 ))))) by
SF_MASTR: 46
.= ((
UsedI*Loc I)
\/
{} ) by
SF_MASTR: 32
.= (
UsedI*Loc I);
end;
begin
reserve s,s1,s2 for
State of
SCM+FSA ,
p,p1 for
Instruction-Sequence of
SCM+FSA ,
a,b for
Int-Location,
d for
read-write
Int-Location,
f for
FinSeq-Location,
I for
MacroInstruction of
SCM+FSA ,
J for
good
MacroInstruction of
SCM+FSA ,
k,m,n for
Nat;
set D = (
Data-Locations
SCM+FSA );
definition
let p;
let s be
State of
SCM+FSA , I be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location;
::
SCMFSA9A:def8
func
StepTimes (a,I,p,s) ->
sequence of (
product (
the_Values_of
SCM+FSA )) equals (
StepWhile>0 (a,(I
";" (
SubFrom (a,(
intloc
0 )))),p,(
Initialized s)));
correctness ;
end
reserve a for
read-write
Int-Location;
theorem ::
SCMFSA9A:46
(((
StepTimes (a,J,p,s))
.
0 )
. (
intloc
0 ))
= 1
proof
set I = J;
set ST = (
StepTimes (a,I,p,s));
set Is = (
Initialized s);
thus ((ST
.
0 )
. (
intloc
0 ))
= (Is
. (
intloc
0 )) by
SCMFSA_9:def 5
.= 1 by
SCMFSA_M: 9;
end;
theorem ::
SCMFSA9A:47
(((
StepTimes (a,J,p,s))
.
0 )
. a)
= (s
. a)
proof
set I = J;
set ST = (
StepTimes (a,I,p,s));
set Is = (
Initialized s);
thus ((ST
.
0 )
. a)
= (Is
. a) by
SCMFSA_9:def 5
.= (s
. a) by
SCMFSA_M: 37;
end;
registration
let I be
really-closed
MacroInstruction of
SCM+FSA , a be
Int-Location;
cluster (
Times (a,I)) ->
really-closed;
coherence ;
end
theorem ::
SCMFSA9A:48
Th48: for J be
good
really-closed
MacroInstruction of
SCM+FSA holds not J
destroys a & (((
StepTimes (a,J,p,s))
. k)
. (
intloc
0 ))
= 1 & J
is_halting_on (((
StepTimes (a,J,p,s))
. k),(p
+* (
Times (a,J)))) implies (((
StepTimes (a,J,p,s))
. (k
+ 1))
. (
intloc
0 ))
= 1 & ((((
StepTimes (a,J,p,s))
. k)
. a)
>
0 implies (((
StepTimes (a,J,p,s))
. (k
+ 1))
. a)
= ((((
StepTimes (a,J,p,s))
. k)
. a)
- 1))
proof
let J be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = J;
assume that
A1: not J
destroys a and
A2: (((
StepTimes (a,I,p,s))
. k)
. (
intloc
0 ))
= 1 and
A3: I
is_halting_on (((
StepTimes (a,I,p,s))
. k),(p
+* (
Times (a,I))));
set ST = (
StepTimes (a,I,p,s));
A4: I
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A2,
A3,
SCMFSA8B: 42;
set SW = (
StepWhile>0 (a,(I
";" (
SubFrom (a,(
intloc
0 )))),p,(
Initialized s)));
(
Macro (
SubFrom (a,(
intloc
0 ))))
is_halting_on ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k))),(p
+* (
Times (a,I)))) by
SCMFSA7B: 19;
then
A5: (I
";" (
SubFrom (a,(
intloc
0 ))))
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A4,
SFMASTR1: 3;
hereby
per cases ;
suppose ((SW
. k)
. a)
<=
0 ;
then (
DataPart (SW
. (k
+ 1)))
= (
DataPart (ST
. k)) by
Th31;
hence (((
StepTimes (a,I,p,s))
. (k
+ 1))
. (
intloc
0 ))
= 1 by
A2,
SCMFSA_M: 2;
end;
suppose ((SW
. k)
. a)
>
0 ;
then (
DataPart (SW
. (k
+ 1)))
= (
DataPart (
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),(p
+* (
Times (a,I))),(ST
. k)))) by
A2,
A5,
Th32;
hence ((ST
. (k
+ 1))
. (
intloc
0 ))
= ((
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),(p
+* (
Times (a,I))),(ST
. k)))
. (
intloc
0 )) by
SCMFSA_M: 2
.= ((
Exec ((
SubFrom (a,(
intloc
0 ))),(
IExec (I,(p
+* (
Times (a,I)) qua
good
Program of
SCM+FSA ),(ST
. k)))))
. (
intloc
0 )) by
A4,
SFMASTR1: 11
.= ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. (
intloc
0 )) by
SCMFSA_2: 65
.= 1 by
A4,
SCMFSA8C: 67;
end;
end;
assume ((ST
. k)
. a)
>
0 ;
then (
DataPart (SW
. (k
+ 1)))
= (
DataPart (
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),(p
+* (
Times (a,I))),(ST
. k)))) by
A2,
A5,
Th32;
hence ((ST
. (k
+ 1))
. a)
= ((
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),(p
+* (
Times (a,I))),(ST
. k)))
. a) by
SCMFSA_M: 2
.= ((
Exec ((
SubFrom (a,(
intloc
0 ))),(
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))))
. a) by
A4,
SFMASTR1: 11
.= (((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. a)
- ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. (
intloc
0 ))) by
SCMFSA_2: 65
.= (((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. a)
- 1) by
A4,
SCMFSA8C: 67
.= (((
Initialized (ST
. k))
. a)
- 1) by
A4,
A1,
SCMFSA8C: 95
.= (((ST
. k)
. a)
- 1) by
SCMFSA_M: 37;
end;
theorem ::
SCMFSA9A:49
(((
StepTimes (a,I,p,s))
.
0 )
. f)
= (s
. f)
proof
set ST = (
StepTimes (a,I,p,s));
set Is = (
Initialized s);
thus ((ST
.
0 )
. f)
= (Is
. f) by
SCMFSA_9:def 5
.= (s
. f) by
SCMFSA_M: 37;
end;
definition
let p;
let s be
State of
SCM+FSA , a be
read-write
Int-Location, I be
MacroInstruction of
SCM+FSA ;
::
SCMFSA9A:def9
pred
ProperTimesBody a,I,s,p means for k be
Nat st k
< (s
. a) holds I
is_halting_on (((
StepTimes (a,I,p,s))
. k),(p
+* (
Times (a,I))));
end
theorem ::
SCMFSA9A:50
Th50: I is
parahalting implies
ProperTimesBody (a,I,s,p) by
SCMFSA7B: 19;
theorem ::
SCMFSA9A:51
Th51: for J be
good
really-closed
MacroInstruction of
SCM+FSA holds not J
destroys a &
ProperTimesBody (a,J,s,p) implies for k st k
<= (s
. a) holds (((
StepTimes (a,J,p,s))
. k)
. (
intloc
0 ))
= 1
proof
let J be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = J;
set ST = (
StepTimes (a,I,p,s));
set Is = (
Initialized s);
defpred
X[
Nat] means $1
<= (s
. a) implies ((ST
. $1)
. (
intloc
0 ))
= 1;
assume
A1: not J
destroys a;
assume
A2:
ProperTimesBody (a,I,s,p);
A3: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat;
assume that
A4: k
<= (s
. a) implies ((ST
. k)
. (
intloc
0 ))
= 1 and
A5: (k
+ 1)
<= (s
. a);
reconsider sa = (s
. a) as
Element of
NAT by
A5,
INT_1: 3;
A6: k
< sa by
A5,
NAT_1: 13;
then I
is_halting_on ((ST
. k),(p
+* (
Times (a,I)))) by
A2;
hence thesis by
A4,
A6,
Th48,
A1;
end;
A7:
X[
0 ]
proof
assume
0
<= (s
. a);
thus ((ST
.
0 )
. (
intloc
0 ))
= (Is
. (
intloc
0 )) by
SCMFSA_9:def 5
.= 1 by
SCMFSA_M: 9;
end;
thus for k holds
X[k] from
NAT_1:sch 2(
A7,
A3);
end;
theorem ::
SCMFSA9A:52
Th52: for J be
good
really-closed
MacroInstruction of
SCM+FSA holds not J
destroys a &
ProperTimesBody (a,J,s,p) implies for k st k
<= (s
. a) holds ((((
StepTimes (a,J,p,s))
. k)
. a)
+ k)
= (s
. a)
proof
let J be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = J;
assume that
A1: not J
destroys a and
A2:
ProperTimesBody (a,I,s,p);
set Is = (
Initialized s);
set ST = (
StepTimes (a,I,p,s));
set SW = (
StepWhile>0 (a,(I
";" (
SubFrom (a,(
intloc
0 )))),p,Is));
defpred
X[
Nat] means $1
<= (s
. a) implies ((((
StepTimes (a,I,p,s))
. $1)
. a)
+ $1)
= (s
. a);
A3: for k be
Nat st
X[k] holds
X[(k
+ 1)]
proof
let k be
Nat such that
A4: k
<= (s
. a) implies (((ST
. k)
. a)
+ k)
= (s
. a) and
A5: (k
+ 1)
<= (s
. a);
reconsider sa = (s
. a) as
Element of
NAT by
A5,
INT_1: 3;
A6: k
< sa by
A5,
NAT_1: 13;
then
A7: ((ST
. k)
. (
intloc
0 ))
= 1 by
A1,
A2,
Th51;
A8:
now
assume ((SW
. k)
. a)
<=
0 ;
then (((SW
. k)
. a)
+ k)
< ((s
. a)
+
0 ) by
A6,
XREAL_1: 8;
hence contradiction by
A4,
A6;
end;
I
is_halting_on ((ST
. k),(p
+* (
Times (a,I)))) by
A2,
A6;
then
A9: I
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A7,
SCMFSA8B: 42;
(
Macro (
SubFrom (a,(
intloc
0 ))))
is_halting_on ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k))),(p
+* (
Times (a,I)))) by
SCMFSA7B: 19;
then (I
";" (
SubFrom (a,(
intloc
0 ))))
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A9,
SFMASTR1: 3;
then (
DataPart (SW
. (k
+ 1)))
= (
DataPart (
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),(p
+* (
Times (a,I))),(ST
. k)))) by
A7,
A8,
Th32;
then ((ST
. (k
+ 1))
. a)
= ((
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),(p
+* (
Times (a,I))),(ST
. k)))
. a) by
SCMFSA_M: 2
.= ((
Exec ((
SubFrom (a,(
intloc
0 ))),(
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))))
. a) by
A9,
SFMASTR1: 11
.= (((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. a)
- ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. (
intloc
0 ))) by
SCMFSA_2: 65
.= (((
IExec (I,(p
+* (
Times (a,I))),(ST
. k)))
. a)
- 1) by
A9,
SCMFSA8C: 67
.= (((
Initialized (ST
. k))
. a)
- 1) by
A9,
A1,
SCMFSA8C: 95
.= (((ST
. k)
. a)
- 1) by
SCMFSA_M: 37;
hence thesis by
A4,
A6;
end;
A10:
X[
0 ]
proof
assume
0
<= (s
. a);
thus (((ST
.
0 )
. a)
+
0 )
= (Is
. a) by
SCMFSA_9:def 5
.= (s
. a) by
SCMFSA_M: 37;
end;
thus for k holds
X[k] from
NAT_1:sch 2(
A10,
A3);
end;
theorem ::
SCMFSA9A:53
Th53: for J be
good
really-closed
MacroInstruction of
SCM+FSA holds not J
destroys a &
ProperTimesBody (a,J,s,p) &
0
<= (s
. a) implies for k st k
>= (s
. a) holds (((
StepTimes (a,J,p,s))
. k)
. a)
=
0 & (((
StepTimes (a,J,p,s))
. k)
. (
intloc
0 ))
= 1
proof
let J be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = J;
assume that
A1: not J
destroys a and
A2:
ProperTimesBody (a,I,s,p) and
A3:
0
<= (s
. a);
set ST = (
StepTimes (a,I,p,s));
set SW = (
StepWhile>0 (a,(I
";" (
SubFrom (a,(
intloc
0 )))),p,(
Initialized s)));
defpred
X[
Nat] means $1
>= (s
. a) implies ((ST
. $1)
. a)
=
0 & ((ST
. $1)
. (
intloc
0 ))
= 1;
A4: for k st
X[k] holds
X[(k
+ 1)]
proof
reconsider sa = (s
. a) as
Element of
NAT by
A3,
INT_1: 3;
let k such that
A5: k
>= (s
. a) implies ((ST
. k)
. a)
=
0 & ((ST
. k)
. (
intloc
0 ))
= 1 and
A6: (k
+ 1)
>= (s
. a);
per cases by
A6,
XXREAL_0: 1;
suppose
A7: (k
+ 1)
= sa;
then (((ST
. (k
+ 1))
. a)
+ (k
+ 1))
= (s
. a) by
A2,
Th52,
A1;
hence ((ST
. (k
+ 1))
. a)
=
0 by
A7;
thus thesis by
A2,
A7,
Th51,
A1;
end;
suppose
A8: (k
+ 1)
> sa;
then
A9: (
DataPart (SW
. (k
+ 1)))
= (
DataPart (SW
. k)) by
A5,
NAT_1: 13,
Th31;
hence ((ST
. (k
+ 1))
. a)
=
0 by
A5,
A8,
NAT_1: 13,
SCMFSA_M: 2;
thus thesis by
A5,
A8,
A9,
NAT_1: 13,
SCMFSA_M: 2;
end;
end;
A10:
X[
0 ]
proof
assume
A11:
0
>= (s
. a);
thus ((ST
.
0 )
. a)
= (((ST
.
0 )
. a)
+
0 )
.=
0 by
A2,
A3,
A11,
Th52,
A1;
thus thesis by
A2,
A3,
Th51,
A1;
end;
thus for k holds
X[k] from
NAT_1:sch 2(
A10,
A4);
end;
theorem ::
SCMFSA9A:54
for J be
good
really-closed
MacroInstruction of
SCM+FSA holds not J
destroys a & (s
. a)
= k & (
ProperTimesBody (a,J,s,p) or J is
parahalting) implies (
DataPart (
IExec ((
Times (a,J)),p,s)))
= (
DataPart ((
StepTimes (a,J,p,s))
. k))
proof
let J be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = J;
assume
A1: not J
destroys a;
assume
A2: (s
. a)
= k;
set ST = (
StepTimes (a,I,p,s));
reconsider ISu = (I
";" (
SubFrom (a,(
intloc
0 )))) as
really-closed
MacroInstruction of
SCM+FSA ;
set s1 = (
Initialized s);
set Is1 = (
Initialized s1);
set SW = (
StepWhile>0 (a,ISu,p,s1));
set ISW = (
StepWhile>0 (a,ISu,p,Is1));
set WH = (
while>0 (a,ISu));
assume
A3:
ProperTimesBody (a,I,s,p) or I is
parahalting;
then
A4:
ProperTimesBody (a,I,s,p) by
Th50;
A5:
ProperBodyWhile>0 (a,ISu,s1,p)
proof
let k be
Nat;
assume ((SW
. k)
. a)
>
0 ;
then
A6: k
< (s
. a) by
A2,
A4,
Th53,
A1;
then
A7: ((ST
. k)
. (
intloc
0 ))
= 1 by
A3,
Th50,
Th51,
A1;
then
A8: (
DataPart (ST
. k))
= (
DataPart (
Initialized (ST
. k))) by
SCMFSA_M: 19;
I
is_halting_on ((ST
. k),(p
+* (
Times (a,I)))) by
A4,
A6;
then
A9: I
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A7,
SCMFSA8B: 42;
(
Macro (
SubFrom (a,(
intloc
0 ))))
is_halting_on ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k))),(p
+* (
Times (a,I)))) by
SCMFSA7B: 19;
then ISu
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A9,
SFMASTR1: 3;
hence thesis by
A8,
SCMFSA8B: 5;
end;
A10:
WithVariantWhile>0 (a,ISu,Is1,p)
proof
reconsider sa = (s
. a) as
Element of
NAT by
A2,
ORDINAL1:def 12;
deffunc
U(
State of
SCM+FSA ) =
|.($1
. a).|;
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A11: for x be
Element of (
product (
the_Values_of
SCM+FSA )) holds (f
. x)
=
U(x) from
FUNCT_2:sch 4;
A12: for x be
State of
SCM+FSA holds (f
. x)
=
U(x)
proof
let x be
State of
SCM+FSA ;
reconsider x as
Element of (
product (
the_Values_of
SCM+FSA )) by
CARD_3: 107;
(f
. x)
=
U(x) by
A11;
hence thesis;
end;
take f;
let k be
Nat;
per cases ;
suppose
A13: k
< (s
. a);
then
A14: (k
- k)
< ((s
. a)
- k) by
XREAL_1: 9;
A15: (((ST
. k)
. a)
+ k)
= (s
. a) by
A4,
A13,
Th52,
A1;
A16: (k
+ 1)
<= sa by
A13,
NAT_1: 13;
then
A17: ((k
+ 1)
- (k
+ 1))
<= ((s
. a)
- (k
+ 1)) by
XREAL_1: 9;
A18: (((ST
. (k
+ 1))
. a)
+ (k
+ 1))
= (s
. a) by
A4,
A16,
Th52,
A1;
then
A19: (s
. a)
= ((((ST
. (k
+ 1))
. a)
+ 1)
+ k);
A20: (f
. (ISW
. (k
+ 1)))
=
|.((ISW
. (k
+ 1))
. a).| by
A12
.= ((SW
. (k
+ 1))
. a) by
A18,
A17,
ABSVALUE:def 1;
(f
. (ISW
. k))
=
|.((ISW
. k)
. a).| by
A12
.= ((SW
. k)
. a) by
A15,
A14,
ABSVALUE:def 1;
hence thesis by
A15,
A19,
A20,
NAT_1: 13;
end;
suppose k
>= (s
. a);
hence thesis by
A2,
A4,
Th53,
A1;
end;
end;
A21:
ProperBodyWhile>0 (a,ISu,Is1,p) by
A5;
then
consider K be
Nat such that
A22: (
ExitsAtWhile>0 (a,ISu,p,Is1))
= K and
A23: ((ISW
. K)
. a)
<=
0 and
A24: for i be
Nat st ((ISW
. i)
. a)
<=
0 holds K
<= i and (
DataPart (
Comput ((p
+* WH),(
Initialize Is1),(
LifeSpan ((p
+* WH),(
Initialize Is1))))))
= (
DataPart (ISW
. K)) by
A10,
Def6;
A25: (
DataPart (
IExec (WH,p,s1)))
= (
DataPart (ISW
. (
ExitsAtWhile>0 (a,ISu,p,Is1)))) by
A21,
A10,
Th36;
((SW
. k)
. a)
=
0 by
A2,
A4,
Th53,
A1;
then ((ISW
. k)
. a)
=
0 ;
then
A26: K
<= k by
A24;
then
A27: (((SW
. K)
. a)
+ K)
= k by
A2,
A4,
Th52,
A1;
(K
- K)
<= (k
- K) by
A26,
XREAL_1: 9;
then
A28: ((ISW
. K)
. a)
=
0 by
A23,
A27;
A29: (((ISW
. K)
. a)
+ K)
= k by
A27;
A30:
now
let x be
Int-Location;
thus ((
IExec ((
Times (a,I)),p,s))
. x)
= ((
IExec (WH,p,s1))
. x) by
SCMFSA8C: 3
.= ((ST
. k)
. x) by
A25,
A22,
A29,
A28,
SCMFSA_M: 2;
end;
now
let x be
FinSeq-Location;
thus ((
IExec ((
Times (a,I)),p,s))
. x)
= ((
IExec (WH,p,s1))
. x) by
SCMFSA8C: 3
.= ((ST
. k)
. x) by
A25,
A22,
A29,
A28,
SCMFSA_M: 2;
end;
hence thesis by
A30,
SCMFSA_M: 2;
end;
theorem ::
SCMFSA9A:55
Th55: for J be
good
really-closed
MacroInstruction of
SCM+FSA holds not J
destroys a & (s
. (
intloc
0 ))
= 1 & (
ProperTimesBody (a,J,s,p) or J is
parahalting) implies (
Times (a,J))
is_halting_on (s,p)
proof
let J be
good
really-closed
MacroInstruction of
SCM+FSA ;
set I = J;
assume
A1: not J
destroys a;
assume
A2: (s
. (
intloc
0 ))
= 1;
set taI = (
Times (a,I));
set ST = (
StepTimes (a,I,p,s));
set ISu = (I
";" (
SubFrom (a,(
intloc
0 ))));
set WH = (
while>0 (a,ISu));
set s1 = (
Initialized s);
set Is1 = (
Initialized s1);
set SW = (
StepWhile>0 (a,ISu,p,s1));
set ISW = (
StepWhile>0 (a,ISu,p,Is1));
assume
A3:
ProperTimesBody (a,I,s,p) or I is
parahalting;
then
A4:
ProperTimesBody (a,I,s,p) by
Th50;
per cases ;
suppose
A5: (s
. a)
<
0 ;
A6: (s1
. a)
= (s
. a) by
SCMFSA_M: 37;
WH
is_halting_on (s1,p) by
A5,
A6,
SCMFSA_9: 38;
then taI
is_halting_on ((
Initialized s),p);
hence thesis by
A2,
SCMFSA8B: 42;
end;
suppose
A7:
0
<= (s
. a);
A8:
ProperBodyWhile>0 (a,ISu,s1,p)
proof
let k be
Nat;
assume ((SW
. k)
. a)
>
0 ;
then
A9: k
< (s
. a) by
A4,
A7,
Th53,
A1;
then
A10: ((ST
. k)
. (
intloc
0 ))
= 1 by
A3,
Th50,
Th51,
A1;
then
A11: (
DataPart (ST
. k))
= (
DataPart (
Initialized (ST
. k))) by
SCMFSA_M: 19;
I
is_halting_on ((ST
. k),(p
+* (
Times (a,I)))) by
A4,
A9;
then
A12: I
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A10,
SCMFSA8B: 42;
(
Macro (
SubFrom (a,(
intloc
0 ))))
is_halting_on ((
IExec (I,(p
+* (
Times (a,I))),(ST
. k))),(p
+* (
Times (a,I)))) by
SCMFSA7B: 19;
then ISu
is_halting_on ((
Initialized (ST
. k)),(p
+* (
Times (a,I)))) by
A12,
SFMASTR1: 3;
hence thesis by
A11,
SCMFSA8B: 5;
end;
A13:
WithVariantWhile>0 (a,ISu,Is1,p)
proof
reconsider sa = (s
. a) as
Element of
NAT by
A7,
INT_1: 3;
deffunc
U(
State of
SCM+FSA ) =
|.($1
. a).|;
consider f be
Function of (
product (
the_Values_of
SCM+FSA )),
NAT such that
A14: for x be
Element of (
product (
the_Values_of
SCM+FSA )) holds (f
. x)
=
U(x) from
FUNCT_2:sch 4;
A15: for x be
State of
SCM+FSA holds (f
. x)
=
U(x)
proof
let x be
State of
SCM+FSA ;
reconsider x as
Element of (
product (
the_Values_of
SCM+FSA )) by
CARD_3: 107;
(f
. x)
=
U(x) by
A14;
hence thesis;
end;
take f;
let k be
Nat;
per cases ;
suppose
A16: k
< (s
. a);
then
A17: (k
- k)
< ((s
. a)
- k) by
XREAL_1: 9;
A18: (((ST
. k)
. a)
+ k)
= (s
. a) by
A4,
A16,
Th52,
A1;
A19: (k
+ 1)
<= sa by
A16,
NAT_1: 13;
then
A20: ((k
+ 1)
- (k
+ 1))
<= ((s
. a)
- (k
+ 1)) by
XREAL_1: 9;
A21: (((ST
. (k
+ 1))
. a)
+ (k
+ 1))
= (s
. a) by
A4,
A19,
Th52,
A1;
then
A22: (s
. a)
= ((((ST
. (k
+ 1))
. a)
+ 1)
+ k);
A23: (f
. (ISW
. (k
+ 1)))
=
|.((ISW
. (k
+ 1))
. a).| by
A15
.= ((SW
. (k
+ 1))
. a) by
A21,
A20,
ABSVALUE:def 1;
(f
. (ISW
. k))
=
|.((ISW
. k)
. a).| by
A15
.= ((SW
. k)
. a) by
A18,
A17,
ABSVALUE:def 1;
hence thesis by
A18,
A22,
A23,
NAT_1: 13;
end;
suppose k
>= (s
. a);
hence thesis by
A4,
A7,
Th53,
A1;
end;
end;
A24:
ProperBodyWhile>0 (a,ISu,Is1,p) by
A8;
WH
is_halting_on (Is1,p) by
A24,
A13,
Th27;
then WH
is_halting_on (s1,p);
then taI
is_halting_on ((
Initialized s),p);
hence thesis by
A2,
SCMFSA8B: 42;
end;
end;
reserve P for
Instruction-Sequence of
SCM+FSA ;
theorem ::
SCMFSA9A:56
Th56: for s be
State of
SCM+FSA , I be
good
parahalting
really-closed
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st not I
destroys a & (s
. (
intloc
0 ))
= 1 holds (
Times (a,I))
is_halting_on (s,P) by
Th55;
theorem ::
SCMFSA9A:57
for I be
good
parahalting
really-closed
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st not I
destroys a holds (
Initialize ((
intloc
0 )
.--> 1)) is (
Times (a,I))
-halted
proof
let I be
good
parahalting
really-closed
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
assume
A1: not I
destroys a;
now
let s be
State of
SCM+FSA ;
let P be
Instruction-Sequence of
SCM+FSA ;
((
Initialized s)
. (
intloc
0 ))
= 1 by
SCMFSA_M: 5;
hence (
Times (a,I))
is_halting_on ((
Initialized s),P) by
A1,
Th56;
end;
hence thesis by
SCMFSA8C: 5;
end;
theorem ::
SCMFSA9A:58
for s be
State of
SCM+FSA , I be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. (
intloc
0 ))
= 1 & (s
. a)
<=
0 holds (
DataPart (
IExec ((
Times (a,I)),P,s)))
= (
DataPart s) by
Th35;