scmfsa8c.miz
begin
reserve m for
Nat;
reserve P,PP,P1,P2 for
Instruction-Sequence of
SCM+FSA ;
set SA0 = (
Start-At (
0 ,
SCM+FSA ));
set Q = ((
intloc
0 )
.--> 1);
theorem ::
SCMFSA8C:1
for s be
State of
SCM+FSA , I be
initial
Program of
SCM+FSA st I
is_pseudo-closed_on (s,P) holds for k be
Nat st for n be
Nat st n
<= k holds (
IC (
Comput ((P
+* I),(
Initialize s),n)))
in (
dom I) holds k
< (
pseudo-LifeSpan (s,P,I))
proof
let s be
State of
SCM+FSA ;
let I be
initial
Program of
SCM+FSA ;
assume I
is_pseudo-closed_on (s,P);
then (
IC (
Comput ((P
+* I),(
Initialize s),(
pseudo-LifeSpan (s,P,I)))))
= (
card I) by
SCMFSA8A:def 4;
then
A1: not (
IC (
Comput ((P
+* I),(
Initialize s),(
pseudo-LifeSpan (s,P,I)))))
in (
dom I);
let k be
Nat;
assume for n be
Nat st n
<= k holds (
IC (
Comput ((P
+* I),(
Initialize s),n)))
in (
dom I);
hence (
pseudo-LifeSpan (s,P,I))
> k by
A1;
end;
theorem ::
SCMFSA8C:2
Th2: for I,J be
Program of
SCM+FSA , k be
Nat st (
card I)
<= k & k
< ((
card I)
+ (
card J)) holds for i be
Instruction of
SCM+FSA st i
= (J
. (k
-' (
card I))) holds ((I
";" J)
. k)
= (
IncAddr (i,(
card I)))
proof
let I,J be
Program of
SCM+FSA ;
let k be
Nat;
assume
A1: (
card I)
<= k;
assume k
< ((
card I)
+ (
card J));
then
A2: (k
+
0 )
< ((
card J)
+ (
card I));
(k
-' (
card I))
= (k
- (
card I)) by
A1,
XREAL_1: 233;
then (k
-' (
card I))
< ((
card J)
-
0 ) by
A2,
XREAL_1: 21;
then
A3: (k
-' (
card I))
in (
dom J) by
AFINSQ_1: 66;
let i be
Instruction of
SCM+FSA ;
assume
A4: i
= (J
. (k
-' (
card I)));
A5: ((k
-' (
card I))
+ (
card I))
= ((k
- (
card I))
+ (
card I)) by
A1,
XREAL_1: 233
.= k;
then k
in { (m
+ (
card I)) where m be
Nat : m
in (
dom J) } by
A3;
then k
in (
dom (
Reloc (J,(
card I)))) by
COMPOS_1: 33;
hence ((I
";" J)
. k)
= ((
Reloc (J,(
card I)))
. k) by
SCMFSA6A: 40
.= (
IncAddr (i,(
card I))) by
A4,
A3,
A5,
COMPOS_1: 35;
end;
theorem ::
SCMFSA8C:3
for s be
State of
SCM+FSA , I be
Program of
SCM+FSA holds (
IExec (I,P,s))
= (
IExec (I,P,(
Initialized s)));
::$Canceled
theorem ::
SCMFSA8C:5
Th4: for I be
Program of
SCM+FSA st for s be
State of
SCM+FSA , P holds I
is_halting_on ((
Initialized s),P) holds (
Initialize ((
intloc
0 )
.--> 1)) is I
-halted
proof
let I be
Program of
SCM+FSA ;
assume
A1: for s be
State of
SCM+FSA , P holds I
is_halting_on ((
Initialized s),P);
let s be
State of
SCM+FSA ;
assume (
Initialize ((
intloc
0 )
.--> 1))
c= s;
then (
Initialize ((
intloc
0 )
.--> 1))
c= s;
then
A2: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s by
FUNCT_4: 98;
let P be
Instruction-Sequence of
SCM+FSA such that
A3: I
c= P;
A4: (P
+* I)
= P by
A3,
FUNCT_4: 98;
I
is_halting_on ((
Initialized s),P) by
A1;
then (P
+* I)
halts_on (
Initialize (
Initialized s));
hence P
halts_on s by
A2,
A4,
MEMSTR_0: 44;
end;
theorem ::
SCMFSA8C:6
for I be
Program of
SCM+FSA holds (for s be
State of
SCM+FSA , P holds I
is_halting_on ((
Initialized s),P)) implies (
Initialize ((
intloc
0 )
.--> 1)) is I
-halted by
Th4;
::$Canceled
theorem ::
SCMFSA8C:12
Th6: for s be
State of
SCM+FSA , i be
Instruction of
SCM+FSA st (
InsCode i)
in
{
0 , 6, 7, 8} holds (
DataPart (
Exec (i,s)))
= (
DataPart s)
proof
let s be
State of
SCM+FSA ;
let i be
Instruction of
SCM+FSA ;
assume
A1: (
InsCode i)
in
{
0 , 6, 7, 8};
now
let a be
Int-Location;
let f be
FinSeq-Location;
per cases by
A1,
ENUMSET1:def 2;
suppose (
InsCode i)
=
0 ;
then i
= (
halt
SCM+FSA ) by
SCMFSA_2: 95;
hence ((
Exec (i,s))
. a)
= (s
. a) & ((
Exec (i,s))
. f)
= (s
. f) by
EXTPRO_1:def 3;
end;
suppose (
InsCode i)
= 6;
then ex lb be
Nat st i
= (
goto lb) by
SCMFSA_2: 35;
hence ((
Exec (i,s))
. a)
= (s
. a) & ((
Exec (i,s))
. f)
= (s
. f) by
SCMFSA_2: 69;
end;
suppose (
InsCode i)
= 7;
then ex lb be
Nat, b be
Int-Location st i
= (b
=0_goto lb) by
SCMFSA_2: 36;
hence ((
Exec (i,s))
. a)
= (s
. a) & ((
Exec (i,s))
. f)
= (s
. f) by
SCMFSA_2: 70;
end;
suppose (
InsCode i)
= 8;
then ex lb be
Nat, b be
Int-Location st i
= (b
>0_goto lb) by
SCMFSA_2: 37;
hence ((
Exec (i,s))
. a)
= (s
. a) & ((
Exec (i,s))
. f)
= (s
. f) by
SCMFSA_2: 71;
end;
end;
hence thesis by
SCMFSA_M: 2;
end;
::$Canceled
theorem ::
SCMFSA8C:14
for s be
State of
SCM+FSA holds (
IExec ((
Stop
SCM+FSA ),P,s))
= (
Initialized s)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
set s1 = (
Initialize (
Initialized s)), P1 = (P
+* (
Stop
SCM+FSA ));
A1: (
Stop
SCM+FSA )
c= P1 by
FUNCT_4: 25;
A2: s1
= (
Comput (P1,s1,
0 ));
A3: (P1
/. (
IC s1))
= (P1
. (
IC s1)) by
PBOOLE: 143;
A4:
0
in (
dom (
Stop
SCM+FSA )) by
COMPOS_1: 3;
A5: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s1 by
MEMSTR_0: 44;
A6: (
CurInstr (P1,s1))
= (P1
.
0 ) by
A3,
MEMSTR_0: 28
.= ((
Stop
SCM+FSA )
.
0 ) by
A4,
A1,
GRFUNC_1: 2;
then P1
halts_on s1 by
A2,
EXTPRO_1: 29;
then
A7: (
IExec ((
Stop
SCM+FSA ),P,s))
= s1 by
A5,
A6,
A2,
EXTPRO_1:def 9;
then
A8: (
DataPart (
IExec ((
Stop
SCM+FSA ),P,s)))
= (
DataPart s1)
.= (
DataPart (
Initialized s)) by
MEMSTR_0: 79;
hereby
A9:
now
let x be
object;
assume
A10: x
in (
dom (
IExec ((
Stop
SCM+FSA ),P,s)));
per cases by
A10,
SCMFSA_M: 1;
suppose
A11: x is
Int-Location;
((
IExec ((
Stop
SCM+FSA ),P,s))
. x)
= ((
Initialized s)
. x) by
A8,
A11,
SCMFSA_M: 2;
hence ((
IExec ((
Stop
SCM+FSA ),P,s))
. x)
= ((
Initialized s)
. x);
end;
suppose
A12: x is
FinSeq-Location;
((
IExec ((
Stop
SCM+FSA ),P,s))
. x)
= ((
Initialized s)
. x) by
A8,
A12,
SCMFSA_M: 2;
hence ((
IExec ((
Stop
SCM+FSA ),P,s))
. x)
= ((
Initialized s)
. x);
end;
suppose
A13: x
= (
IC
SCM+FSA );
then x
in
{(
IC
SCM+FSA )} by
TARSKI:def 1;
then
A14: x
in (
dom SA0);
thus ((
IExec ((
Stop
SCM+FSA ),P,s))
. x)
= (s1
. (
IC
SCM+FSA )) by
A7,
A13
.= (SA0
. (
IC
SCM+FSA )) by
A13,
A14,
FUNCT_4: 13
.= (((s
+* ((
intloc
0 )
.--> 1))
+* SA0)
. x) by
A13,
A14,
FUNCT_4: 13
.= ((s
+* (
Initialize ((
intloc
0 )
.--> 1)))
. x) by
FUNCT_4: 14
.= ((
Initialized s)
. x);
end;
end;
(
dom (
IExec ((
Stop
SCM+FSA ),P,s)))
= the
carrier of
SCM+FSA by
PARTFUN1:def 2
.= (
dom (
Initialized s)) by
PARTFUN1:def 2;
hence thesis by
A9,
FUNCT_1: 2;
end;
end;
::$Canceled
theorem ::
SCMFSA8C:16
Th8: for s1 be
0
-started
State of
SCM+FSA , s2 be
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st I
c= P1 holds for n be
Nat st (
Reloc (I,n))
c= P2 & (
IC s2)
= n & (
DataPart s1)
= (
DataPart s2) holds for i be
Nat holds ((
IC (
Comput (P1,s1,i)))
+ n)
= (
IC (
Comput (P2,s2,i))) & (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,i)))),n))
= (
CurInstr (P2,(
Comput (P2,s2,i)))) & (
DataPart (
Comput (P1,s1,i)))
= (
DataPart (
Comput (P2,s2,i)))
proof
let s1 be
0
-started
State of
SCM+FSA , s2 be
State of
SCM+FSA ;
let J be
really-closed
Program of
SCM+FSA ;
set JAt = (
Start-At (
0 ,
SCM+FSA ));
A1:
0
in (
dom J) by
AFINSQ_1: 65;
A2: (
Start-At (
0 ,
SCM+FSA ))
c= s1 by
MEMSTR_0: 29;
assume that
A3: J
c= P1;
SA0
c= s1 by
A2;
then
A4: (
Initialize s1)
= s1 by
FUNCT_4: 98;
A5: (
IC
SCM+FSA )
in (
dom JAt) by
MEMSTR_0: 15;
A6: (P1
. (
IC s1))
= (P1
.
0 ) by
A4,
MEMSTR_0: 16
.= (J
.
0 ) by
A1,
A3,
GRFUNC_1: 2;
A7: (
IC (
Comput (P1,s1,
0 )))
= (
IC s1)
.= (
IC JAt) by
A2,
A5,
GRFUNC_1: 2
.=
0 by
FUNCOP_1: 72;
A8:
0
in (
dom J) by
AFINSQ_1: 65;
let n be
Nat;
defpred
P[
Nat] means ((
IC (
Comput (P1,s1,$1)))
+ n)
= (
IC (
Comput (P2,s2,$1))) & (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,$1)))),n))
= (
CurInstr (P2,(
Comput (P2,s2,$1)))) & (
DataPart (
Comput (P1,s1,$1)))
= (
DataPart (
Comput (P2,s2,$1)));
assume that
A9: (
Reloc (J,n))
c= P2 and
A10: (
IC s2)
= n and
A11: (
DataPart s1)
= (
DataPart s2);
let i be
Nat;
A12: (
DataPart (
Comput (P1,s1,
0 )))
= (
DataPart s2) by
A11
.= (
DataPart (
Comput (P2,s2,
0 )));
A13: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
A14: (
Comput (P1,s1,(k
+ 1)))
= (
Following (P1,(
Comput (P1,s1,k)))) by
EXTPRO_1: 3;
reconsider l = (
IC (
Comput (P1,s1,(k
+ 1)))) as
Element of
NAT ;
reconsider j = (
CurInstr (P1,(
Comput (P1,s1,(k
+ 1))))) as
Instruction of
SCM+FSA ;
A15: (
Comput (P2,s2,(k
+ 1)))
= (
Following (P2,(
Comput (P2,s2,k)))) by
EXTPRO_1: 3;
(
IC s1)
=
0 by
MEMSTR_0:def 11;
then (
IC s1)
in (
dom J) by
AFINSQ_1: 65;
then
A16: (
IC (
Comput (P1,s1,(k
+ 1))))
in (
dom J) by
AMISTD_1: 21,
A3;
assume
A17:
P[k];
hence
A18: ((
IC (
Comput (P1,s1,(k
+ 1))))
+ n)
= (
IC (
Comput (P2,s2,(k
+ 1)))) by
A14,
A15,
SCMFSA6A: 8;
then
A19: (
IC (
Comput (P2,s2,(k
+ 1))))
in (
dom (
Reloc (J,n))) by
A16,
COMPOS_1: 46;
A20: l
in (
dom J) by
A16;
j
= (P1
. (
IC (
Comput (P1,s1,(k
+ 1))))) by
PBOOLE: 143
.= (J
. l) by
A16,
A3,
GRFUNC_1: 2;
hence (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,(k
+ 1))))),n))
= ((
Reloc (J,n))
. (l
+ n)) by
A20,
COMPOS_1: 35
.= (P2
. (
IC (
Comput (P2,s2,(k
+ 1))))) by
A9,
A18,
A19,
GRFUNC_1: 2
.= (
CurInstr (P2,(
Comput (P2,s2,(k
+ 1))))) by
PBOOLE: 143;
thus thesis by
A17,
A14,
A15,
SCMFSA6A: 8;
end;
0
in (
dom J) by
AFINSQ_1: 65;
then
A21: (
0
+ n)
in (
dom (
Reloc (J,n))) by
COMPOS_1: 46;
A22: (P1
/. (
IC s1))
= (P1
. (
IC s1)) by
PBOOLE: 143;
A23: (P2
/. (
IC s2))
= (P2
. (
IC s2)) by
PBOOLE: 143;
(
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,
0 )))),n))
= ((
Reloc (J,n))
. (
0
+ n)) by
A8,
A22,
A6,
COMPOS_1: 35
.= (
CurInstr (P2,(
Comput (P2,s2,
0 )))) by
A9,
A10,
A21,
A23,
GRFUNC_1: 2;
then
A24:
P[
0 ] by
A10,
A7,
A12;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A24,
A13);
hence thesis;
end;
theorem ::
SCMFSA8C:17
Th9: for s1,s2 be
0
-started
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st I
c= P1 & I
c= P2 & (
DataPart s1)
= (
DataPart s2) holds for i be
Nat holds (
IC (
Comput (P1,s1,i)))
= (
IC (
Comput (P2,s2,i))) & (
CurInstr (P1,(
Comput (P1,s1,i))))
= (
CurInstr (P2,(
Comput (P2,s2,i)))) & (
DataPart (
Comput (P1,s1,i)))
= (
DataPart (
Comput (P2,s2,i)))
proof
let s1,s2 be
0
-started
State of
SCM+FSA ;
let J be
really-closed
Program of
SCM+FSA ;
assume that
A1: J
c= P1 and
A2: J
c= P2 and
A3: (
DataPart s1)
= (
DataPart s2);
A4: (
Start-At (
0 ,
SCM+FSA ))
c= s2 by
MEMSTR_0: 29;
A5: (
Reloc (J,
0 ))
= J;
let i be
Nat;
A6: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A7: ((
IC (
Comput (P1,s1,i)))
+
0 )
= (
IC (
Comput (P1,s1,i)));
A8: (
IC s2)
= (
IC (
Initialize s2)) by
A4,
FUNCT_4: 98
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A6,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
(
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,i)))),
0 ))
= (
CurInstr (P1,(
Comput (P1,s1,i)))) by
COMPOS_0: 3;
hence thesis by
A3,
A7,
A8,
Th8,
A1,
A2,
A5;
end;
theorem ::
SCMFSA8C:18
Th10: for s1,s2 be
0
-started
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st I
is_halting_on (s1,P1) & I
c= P1 & I
c= P2 & (
DataPart s1)
= (
DataPart s2) holds (
LifeSpan (P1,s1))
= (
LifeSpan (P2,s2))
proof
let s1,s2 be
0
-started
State of
SCM+FSA ;
let J be
really-closed
Program of
SCM+FSA ;
assume that
A1: J
is_halting_on (s1,P1) and
A2: J
c= P1 and
A3: J
c= P2 and
A4: (
DataPart s1)
= (
DataPart s2);
A5: P1
= (P1
+* J) by
A2,
FUNCT_4: 98;
s1
= (
Initialize s1) by
MEMSTR_0: 44;
then
A6: P1
halts_on s1 by
A1,
A5;
A7:
now
let k be
Nat;
assume (
CurInstr (P2,(
Comput (P2,s2,k))))
= (
halt
SCM+FSA );
then (
CurInstr (P1,(
Comput (P1,s1,k))))
= (
halt
SCM+FSA ) by
A4,
Th9,
A2,
A3;
hence (
LifeSpan (P1,s1))
<= k by
A6,
EXTPRO_1:def 15;
end;
(
CurInstr (P1,(
Comput (P1,s1,(
LifeSpan (P1,s1))))))
= (
halt
SCM+FSA ) by
A6,
EXTPRO_1:def 15;
then
A8: (
CurInstr (P2,(
Comput (P2,s2,(
LifeSpan (P1,s1))))))
= (
halt
SCM+FSA ) by
A4,
Th9,
A2,
A3;
then P2
halts_on s2 by
EXTPRO_1: 29;
hence thesis by
A8,
A7,
EXTPRO_1:def 15;
end;
theorem ::
SCMFSA8C:19
for s1,s2 be
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st (s1
. (
intloc
0 ))
= 1 & I
is_halting_on (s1,P1) & ((for a be
read-write
Int-Location holds (s1
. a)
= (s2
. a)) & for f be
FinSeq-Location holds (s1
. f)
= (s2
. f)) holds (
DataPart (
IExec (I,P1,s1)))
= (
DataPart (
IExec (I,P2,s2)))
proof
let s1,s2 be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
really-closed
Program of
SCM+FSA ;
set s11 = (
Initialized s1), P11 = (P1
+* I);
set s21 = (
Initialized s2), P21 = (P2
+* I);
assume (s1
. (
intloc
0 ))
= 1;
then
A1: s11
= (
Initialize s1) by
SCMFSA_M: 18;
then
A2: (
DataPart s11)
= (
DataPart s1) by
MEMSTR_0: 79;
assume that
A3: I
is_halting_on (s1,P1);
assume
A4: for a be
read-write
Int-Location holds (s1
. a)
= (s2
. a);
A5:
now
let a be
read-write
Int-Location;
a
<> (
intloc
0 ) & a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
then
A6: not a
in (
dom (
Initialize ((
intloc
0 )
.--> 1))) by
SCMFSA_M: 11,
TARSKI:def 2;
hence (s11
. a)
= (s1
. a) by
FUNCT_4: 11
.= (s2
. a) by
A4
.= (s21
. a) by
A6,
FUNCT_4: 11;
end;
assume
A7: for f be
FinSeq-Location holds (s1
. f)
= (s2
. f);
A8:
now
let f be
FinSeq-Location;
f
<> (
intloc
0 ) & f
<> (
IC
SCM+FSA ) by
SCMFSA_2: 57,
SCMFSA_2: 58;
then
A9: not f
in (
dom (
Initialize ((
intloc
0 )
.--> 1))) by
SCMFSA_M: 11,
TARSKI:def 2;
hence (s11
. f)
= (s1
. f) by
FUNCT_4: 11
.= (s2
. f) by
A7
.= (s21
. f) by
A9,
FUNCT_4: 11;
end;
A10: (
intloc
0 )
in (
dom (
Initialize ((
intloc
0 )
.--> 1))) by
SCMFSA_M: 10;
then (s11
. (
intloc
0 ))
= ((
Initialize ((
intloc
0 )
.--> 1))
. (
intloc
0 )) by
FUNCT_4: 13
.= (s21
. (
intloc
0 )) by
A10,
FUNCT_4: 13;
then
A11: (
DataPart s11)
= (
DataPart s21) by
A5,
A8,
SCMFSA_M: 20;
A12: I
c= P21 by
FUNCT_4: 25;
A13: I
c= P11 by
FUNCT_4: 25;
A14: P11
halts_on s11 by
A3,
A1;
then (
CurInstr (P11,(
Comput (P11,s11,(
LifeSpan (P11,s11))))))
= (
halt
SCM+FSA ) by
EXTPRO_1:def 15;
then (
CurInstr (P21,(
Comput (P21,s21,(
LifeSpan (P11,s11))))))
= (
halt
SCM+FSA ) by
A11,
Th9,
A13,
A12;
then
A15: P21
halts_on s21 by
EXTPRO_1: 29;
I
is_halting_on (s11,P11) by
A3,
A2,
SCMFSA8B: 5;
then
A16: (
LifeSpan (P11,s11))
= (
LifeSpan (P21,s21)) by
A11,
Th10,
A13,
A12;
thus (
DataPart (
IExec (I,P1,s1)))
= (
DataPart (
Result (P11,s11)))
.= (
DataPart (
Comput (P11,s11,(
LifeSpan (P11,s11))))) by
A14,
EXTPRO_1: 23
.= (
DataPart (
Comput (P21,s21,(
LifeSpan (P11,s11))))) by
A11,
Th9,
A13,
A12
.= (
DataPart (
Result (P21,s21))) by
A16,
A15,
EXTPRO_1: 23
.= (
DataPart (
IExec (I,P2,s2)));
end;
theorem ::
SCMFSA8C:20
for s1,s2 be
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st (s1
. (
intloc
0 ))
= 1 & I
is_halting_on (s1,P1) & (
DataPart s1)
= (
DataPart s2) holds (
DataPart (
IExec (I,P1,s1)))
= (
DataPart (
IExec (I,P2,s2)))
proof
let s1,s2 be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
really-closed
Program of
SCM+FSA ;
set s11 = (
Initialized s1), P11 = (P1
+* I);
set s21 = (
Initialized s2), P21 = (P2
+* I);
A1: I
c= P11 by
FUNCT_4: 25;
A2: I
c= P21 by
FUNCT_4: 25;
assume that
A3: (s1
. (
intloc
0 ))
= 1 and
A4: I
is_halting_on (s1,P1) and
A5: (
DataPart s1)
= (
DataPart s2);
A6: s11
= (
Initialize s1) by
A3,
SCMFSA_M: 18;
then
A7: (
DataPart s11)
= (
DataPart s1) by
MEMSTR_0: 79;
(s2
. (
intloc
0 ))
= 1 by
A3,
A5,
SCMFSA_M: 2;
then s21
= (
Initialize s2) by
SCMFSA_M: 18;
then
A8: (
DataPart s11)
= (
DataPart s21) by
A5,
A7,
MEMSTR_0: 79;
A9: P11
halts_on s11 by
A4,
A6;
then (
CurInstr (P11,(
Comput (P11,s11,(
LifeSpan (P11,s11))))))
= (
halt
SCM+FSA ) by
EXTPRO_1:def 15;
then (
CurInstr (P21,(
Comput (P21,s21,(
LifeSpan (P11,s11))))))
= (
halt
SCM+FSA ) by
A8,
Th9,
A1,
A2;
then
A10: P21
halts_on s21 by
EXTPRO_1: 29;
I
is_halting_on (s11,P11) by
A4,
A7,
SCMFSA8B: 5;
then
A11: (
LifeSpan (P11,s11))
= (
LifeSpan (P21,s21)) by
A8,
Th10,
A1,
A2;
thus (
DataPart (
IExec (I,P1,s1)))
= (
DataPart (
Result (P11,s11)))
.= (
DataPart (
Comput (P11,s11,(
LifeSpan (P11,s11))))) by
A9,
EXTPRO_1: 23
.= (
DataPart (
Comput (P21,s21,(
LifeSpan (P11,s11))))) by
A8,
Th9,
A1,
A2
.= (
DataPart (
Result (P21,s21))) by
A11,
A10,
EXTPRO_1: 23
.= (
DataPart (
IExec (I,P2,s2)));
end;
theorem ::
SCMFSA8C:21
Th13: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA st I
is_pseudo-closed_on (s,P) holds I
is_pseudo-closed_on ((
Initialize s),(P
+* I)) & (
pseudo-LifeSpan (s,P,I))
= (
pseudo-LifeSpan ((
Initialize s),(P
+* I),I))
proof
let s be
State of
SCM+FSA ;
let I be
Program of
SCM+FSA ;
set s2 = (
Initialize (
Initialize s)), P2 = ((P
+* I)
+* I);
assume
A1: I
is_pseudo-closed_on (s,P);
then
A2: for n be
Nat st not (
IC (
Comput (P2,s2,n)))
in (
dom I) holds (
pseudo-LifeSpan (s,P,I))
<= n by
SCMFSA8A:def 4;
A3: for n be
Nat st n
< (
pseudo-LifeSpan (s,P,I)) holds (
IC (
Comput (P2,s2,n)))
in (
dom I) by
A1,
SCMFSA8A:def 4;
(
IC (
Comput (P2,s2,(
pseudo-LifeSpan (s,P,I)))))
= (
card I) by
A1,
SCMFSA8A:def 4;
hence
A4: I
is_pseudo-closed_on ((
Initialize s),(P
+* I)) by
A3;
(
IC (
Comput (P2,s2,(
pseudo-LifeSpan (s,P,I)))))
= (
card I) by
A1,
SCMFSA8A:def 4;
hence thesis by
A2,
A4,
SCMFSA8A:def 4;
end;
theorem ::
SCMFSA8C:22
Th14: for s1 be
0
-started
State of
SCM+FSA , s2 be
State of
SCM+FSA , I be
Program of
SCM+FSA st I
c= P1 & I
is_pseudo-closed_on (s1,P1) holds for n be
Nat st (
Reloc (I,n))
c= P2 & (
IC s2)
= n & (
DataPart s1)
= (
DataPart s2) holds ((for i be
Nat st i
< (
pseudo-LifeSpan (s1,P1,I)) holds (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,i)))),n))
= (
CurInstr (P2,(
Comput (P2,s2,i))))) & for i be
Nat st i
<= (
pseudo-LifeSpan (s1,P1,I)) holds ((
IC (
Comput (P1,s1,i)))
+ n)
= (
IC (
Comput (P2,s2,i))) & (
DataPart (
Comput (P1,s1,i)))
= (
DataPart (
Comput (P2,s2,i))))
proof
let s1 be
0
-started
State of
SCM+FSA , s2 be
State of
SCM+FSA ;
let I be
Program of
SCM+FSA ;
A1: (
Start-At (
0 ,
SCM+FSA ))
c= s1 by
MEMSTR_0: 29;
assume
A2: I
c= P1;
then
A3: P1
= (P1
+* I) by
FUNCT_4: 98;
assume
A4: I
is_pseudo-closed_on (s1,P1);
let n be
Nat;
assume
A5: (
Reloc (I,n))
c= P2;
defpred
P[
Nat] means $1
<= (
pseudo-LifeSpan (s1,P1,I)) implies ((
IC (
Comput (P1,s1,$1)))
+ n)
= (
IC (
Comput (P2,s2,$1))) & (
DataPart (
Comput (P1,s1,$1)))
= (
DataPart (
Comput (P2,s2,$1)));
assume
A6: (
IC s2)
= n;
assume
A7: (
DataPart s1)
= (
DataPart s2);
now
defpred
P[
Nat] means $1
< (
pseudo-LifeSpan (s1,P1,I)) implies ((
IC (
Comput (P1,s1,$1)))
+ n)
= (
IC (
Comput (P2,s2,$1))) & (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,$1)))),n))
= (
CurInstr (P2,(
Comput (P2,s2,$1)))) & (
DataPart (
Comput (P1,s1,$1)))
= (
DataPart (
Comput (P2,s2,$1)));
let i be
Nat;
assume
A9: i
< (
pseudo-LifeSpan (s1,P1,I));
A10: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A11:
P[k];
reconsider l = (
IC (
Comput (P1,s1,(k
+ 1)))) as
Element of
NAT ;
reconsider j = (
CurInstr (P1,(
Comput (P1,s1,(k
+ 1))))) as
Instruction of
SCM+FSA ;
assume
A12: (k
+ 1)
< (
pseudo-LifeSpan (s1,P1,I));
A13: (
Comput (P1,s1,(k
+ 1)))
= (
Following (P1,(
Comput (P1,s1,k)))) by
EXTPRO_1: 3;
A14: (
Initialize s1)
= s1 by
A1,
FUNCT_4: 98;
then
A15: (
IC (
Comput (P1,s1,(k
+ 1))))
in (
dom I) by
A4,
A12,
A3,
SCMFSA8A:def 4;
A16: l
in (
dom I) by
A14,
A4,
A12,
A3,
SCMFSA8A:def 4;
A17: (
Comput (P2,s2,(k
+ 1)))
= (
Following (P2,(
Comput (P2,s2,k)))) by
EXTPRO_1: 3;
A18: (k
+
0 )
< (k
+ 1) by
XREAL_1: 6;
hence
A19: ((
IC (
Comput (P1,s1,(k
+ 1))))
+ n)
= (
IC (
Comput (P2,s2,(k
+ 1)))) by
A11,
A12,
A13,
A17,
SCMFSA6A: 8,
XXREAL_0: 2;
then
A20: (
IC (
Comput (P2,s2,(k
+ 1))))
in (
dom (
Reloc (I,n))) by
A15,
COMPOS_1: 46;
j
= (P1
. (
IC (
Comput (P1,s1,(k
+ 1))))) by
PBOOLE: 143
.= (I
. l) by
A15,
A2,
GRFUNC_1: 2;
hence (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,(k
+ 1))))),n))
= ((
Reloc (I,n))
. (l
+ n)) by
A16,
COMPOS_1: 35
.= (P2
. (
IC (
Comput (P2,s2,(k
+ 1))))) by
A20,
A19,
A5,
GRFUNC_1: 2
.= (
CurInstr (P2,(
Comput (P2,s2,(k
+ 1))))) by
PBOOLE: 143;
thus thesis by
A11,
A12,
A18,
A13,
A17,
SCMFSA6A: 8,
XXREAL_0: 2;
end;
A21:
P[
0 ]
proof
A22: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A23: (
IC (
Comput ((P1
+* I),(
Initialize s1),
0 )))
= (
IC (
Initialize s1))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A22,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
assume
0
< (
pseudo-LifeSpan (s1,P1,I));
then
A24:
0
in (
dom I) by
A4,
A23,
SCMFSA8A:def 4;
A25: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
(
IC (
Comput (P1,s1,
0 )))
= (s1
. (
IC
SCM+FSA ))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A1,
A25,
GRFUNC_1: 2
.=
0 by
FUNCOP_1: 72;
hence ((
IC (
Comput (P1,s1,
0 )))
+ n)
= (
IC (
Comput (P2,s2,
0 ))) by
A6;
A26: (
0
+ n)
in (
dom (
Reloc (I,n))) by
A24,
COMPOS_1: 46;
A27: (P1
. (
IC s1))
= (P1
. (
IC (
Start-At (
0 ,
SCM+FSA )))) by
A1,
A25,
GRFUNC_1: 2
.= (P1
.
0 ) by
FUNCOP_1: 72
.= (I
.
0 ) by
A24,
A2,
GRFUNC_1: 2;
A28: (P1
/. (
IC s1))
= (P1
. (
IC s1)) by
PBOOLE: 143;
A29: (P2
/. (
IC s2))
= (P2
. (
IC s2)) by
PBOOLE: 143;
thus (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,
0 )))),n))
= ((
Reloc (I,n))
. (
0
+ n)) by
A24,
A28,
A27,
COMPOS_1: 35
.= (
CurInstr (P2,(
Comput (P2,s2,
0 )))) by
A6,
A26,
A29,
A5,
GRFUNC_1: 2;
thus (
DataPart (
Comput (P1,s1,
0 )))
= (
DataPart s2) by
A7
.= (
DataPart (
Comput (P2,s2,
0 )));
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A21,
A10);
hence (
IncAddr ((
CurInstr (P1,(
Comput (P1,s1,i)))),n))
= (
CurInstr (P2,(
Comput (P2,s2,i)))) by
A9;
end;
A30: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A31:
P[k];
set i = (
CurInstr (P1,(
Comput (P1,s1,k))));
A32: (
Comput (P2,s2,(k
+ 1)))
= (
Following (P2,(
Comput (P2,s2,k)))) by
EXTPRO_1: 3;
assume
A33: (k
+ 1)
<= (
pseudo-LifeSpan (s1,P1,I));
then
A34: (k
+ 1)
<= ((
pseudo-LifeSpan (s1,P1,I))
+ 1) by
NAT_1: 12;
A35: k
< (
pseudo-LifeSpan (s1,P1,I)) by
A33,
NAT_1: 13;
A36: (
Comput (P1,s1,(k
+ 1)))
= (
Following (P1,(
Comput (P1,s1,k)))) by
EXTPRO_1: 3;
hence ((
IC (
Comput (P1,s1,(k
+ 1))))
+ n)
= (
IC (
Exec ((
IncAddr (i,n)),(
Comput (P2,s2,k))))) by
A31,
A34,
SCMFSA6A: 8,
XREAL_1: 6
.= (
IC (
Comput (P2,s2,(k
+ 1)))) by
A8,
A35,
A32;
thus (
DataPart (
Comput (P1,s1,(k
+ 1))))
= (
DataPart (
Exec ((
IncAddr (i,n)),(
Comput (P2,s2,k))))) by
A31,
A34,
A36,
SCMFSA6A: 8,
XREAL_1: 6
.= (
DataPart (
Comput (P2,s2,(k
+ 1)))) by
A8,
A35,
A32;
end;
let i be
Nat;
assume
A37: i
<= (
pseudo-LifeSpan (s1,P1,I));
A38:
P[
0 ]
proof
assume
0
<= (
pseudo-LifeSpan (s1,P1,I));
A39: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
(
IC (
Comput (P1,s1,
0 )))
= (s1
. (
IC
SCM+FSA ))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A1,
A39,
GRFUNC_1: 2
.=
0 by
FUNCOP_1: 72;
hence ((
IC (
Comput (P1,s1,
0 )))
+ n)
= (
IC (
Comput (P2,s2,
0 ))) by
A6;
thus (
DataPart (
Comput (P1,s1,
0 )))
= (
DataPart s2) by
A7
.= (
DataPart (
Comput (P2,s2,
0 )));
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A38,
A30);
hence thesis by
A37;
end;
theorem ::
SCMFSA8C:23
Th15: for s1,s2 be
State of
SCM+FSA , I be
Program of
SCM+FSA st (
DataPart s1)
= (
DataPart s2) holds I
is_pseudo-closed_on (s1,P1) implies I
is_pseudo-closed_on (s2,P2)
proof
let s1,s2 be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
Program of
SCM+FSA ;
set S1 = (
Initialize s1), Q1 = (P1
+* I), S2 = (
Initialize s2), Q2 = (P2
+* I);
A1: I
c= Q1 by
FUNCT_4: 25;
A2: (
Reloc (I,
0 ))
= I;
A3: (
IC (
Initialize s2))
= (
IC (s2
+* (
Start-At (
0 ,
SCM+FSA ))))
.=
0 by
FUNCT_4: 113;
A4: I
c= Q2 by
FUNCT_4: 25;
assume (
DataPart s1)
= (
DataPart s2);
then
A5: (
DataPart S1)
= (
DataPart s2) by
MEMSTR_0: 79
.= (
DataPart S2) by
MEMSTR_0: 79;
assume
A6: I
is_pseudo-closed_on (s1,P1);
then
A7: (
IC (
Comput (Q1,S1,(
pseudo-LifeSpan (s1,P1,I)))))
= (
card I) by
SCMFSA8A:def 4;
A8: I
is_pseudo-closed_on (S1,Q1) by
A6;
A9:
now
let k be
Nat;
assume
A10: k
< (
pseudo-LifeSpan (s1,P1,I));
then k
<= (
pseudo-LifeSpan ((
Initialize s1),(P1
+* I),I)) by
A6,
Th13;
then (
IC (
Comput (Q2,S2,k)))
= ((
IC (
Comput (Q1,S1,k)))
+
0 ) by
A5,
A8,
A4,
A3,
Th14,
A1,
A2
.= (
IC (
Comput (Q1,S1,k)));
hence (
IC (
Comput (Q2,S2,k)))
in (
dom I) by
A6,
A10,
SCMFSA8A:def 4;
end;
(
IC (
Comput (Q2,S2,(
pseudo-LifeSpan (s1,P1,I)))))
= (
IC (
Comput (Q2,S2,(
pseudo-LifeSpan ((
Initialize s1),(P1
+* I),I))))) by
A6,
Th13
.= ((
IC (
Comput (Q1,S1,(
pseudo-LifeSpan ((
Initialize s1),(P1
+* I),I)))))
+
0 ) by
A5,
A8,
A4,
A3,
Th14,
A1,
A2
.= (
IC (
Comput (Q1,S1,(
pseudo-LifeSpan (s1,P1,I))))) by
A6,
Th13;
hence thesis by
A7,
A9;
end;
theorem ::
SCMFSA8C:24
Th16: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA st (s
. (
intloc
0 ))
= 1 holds I
is_pseudo-closed_on (s,P) iff I
is_pseudo-closed_on ((
Initialized s),P)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
Program of
SCM+FSA ;
assume (s
. (
intloc
0 ))
= 1;
then (
DataPart s)
= (
DataPart (
Initialized s)) by
SCMFSA_M: 19;
hence thesis by
Th15;
end;
theorem ::
SCMFSA8C:25
Th17: for a be
Int-Location, I,J be
MacroInstruction of
SCM+FSA holds 1
in (
dom (
if=0 (a,I,J))) & 1
in (
dom (
if>0 (a,I,J)))
proof
let a be
Int-Location;
let I,J be
MacroInstruction of
SCM+FSA ;
set i = (a
=0_goto ((
card J)
+ 3));
(
if=0 (a,I,J))
= ((((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I)
";" (
Stop
SCM+FSA ))
.= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25
.= ((i
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25
.= (i
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 29
.= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))));
then
A1: (
dom (
Macro i))
c= (
dom (
if=0 (a,I,J))) by
SCMFSA6A: 17;
(
dom (
Macro i))
=
{
0 , 1} by
COMPOS_1: 61;
then
A2: 1
in (
dom (
Macro i)) by
TARSKI:def 2;
thus 1
in (
dom (
if=0 (a,I,J))) by
A1,
A2;
set i = (a
>0_goto ((
card J)
+ 3));
(
if>0 (a,I,J))
= ((((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I)
";" (
Stop
SCM+FSA ))
.= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25
.= ((i
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25
.= (i
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 29
.= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))));
then
A3: (
dom (
Macro i))
c= (
dom (
if>0 (a,I,J))) by
SCMFSA6A: 17;
(
dom (
Macro i))
=
{
0 , 1} by
COMPOS_1: 61;
then
A4: 1
in (
dom (
Macro i)) by
TARSKI:def 2;
thus thesis by
A3,
A4;
end;
theorem ::
SCMFSA8C:26
Th18: for a be
Int-Location, I,J be
MacroInstruction of
SCM+FSA holds ((
if=0 (a,I,J))
.
0 )
= (a
=0_goto ((
card J)
+ 3)) & ((
if=0 (a,I,J))
. 1)
= (
goto 2) & ((
if>0 (a,I,J))
.
0 )
= (a
>0_goto ((
card J)
+ 3)) & ((
if>0 (a,I,J))
. 1)
= (
goto 2)
proof
let a be
Int-Location;
let I,J be
MacroInstruction of
SCM+FSA ;
set i = (a
=0_goto ((
card J)
+ 3));
A1: (
if=0 (a,I,J))
= ((((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I)
";" (
Stop
SCM+FSA ))
.= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25
.= ((i
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25
.= (i
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 29
.= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))));
A2: (
dom (
Macro i))
=
{
0 , 1} by
COMPOS_1: 61;
then
0
in (
dom (
Macro i)) by
TARSKI:def 2;
hence ((
if=0 (a,I,J))
.
0 )
= ((
Directed (
Macro i))
.
0 ) by
A1,
SCMFSA8A: 14
.= i by
SCMFSA7B: 1;
1
in (
dom (
Macro i)) by
A2,
TARSKI:def 2;
hence ((
if=0 (a,I,J))
. 1)
= ((
Directed (
Macro i))
. 1) by
A1,
SCMFSA8A: 14
.= (
goto 2) by
SCMFSA7B: 2;
set i = (a
>0_goto ((
card J)
+ 3));
A3: (
if>0 (a,I,J))
= ((((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I)
";" (
Stop
SCM+FSA ))
.= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25
.= ((i
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25
.= (i
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 29
.= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))));
A4: (
dom (
Macro i))
=
{
0 , 1} by
COMPOS_1: 61;
then
0
in (
dom (
Macro i)) by
TARSKI:def 2;
hence ((
if>0 (a,I,J))
.
0 )
= ((
Directed (
Macro i))
.
0 ) by
A3,
SCMFSA8A: 14
.= i by
SCMFSA7B: 1;
1
in (
dom (
Macro i)) by
A4,
TARSKI:def 2;
hence ((
if>0 (a,I,J))
. 1)
= ((
Directed (
Macro i))
. 1) by
A3,
SCMFSA8A: 14
.= (
goto 2) by
SCMFSA7B: 2;
end;
theorem ::
SCMFSA8C:27
Th19: for a be
Int-Location, I,J be
MacroInstruction of
SCM+FSA , n be
Element of
NAT st n
< (((
card I)
+ (
card J))
+ 3) holds n
in (
dom (
if=0 (a,I,J))) & ((
if=0 (a,I,J))
. n)
<> (
halt
SCM+FSA )
proof
let a be
Int-Location;
let I,J be
MacroInstruction of
SCM+FSA ;
let n be
Element of
NAT ;
set J1 = ((((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
A1: (
card J1)
= ((
card (((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
=0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
assume n
< (((
card I)
+ (
card J))
+ 3);
then n
in (
dom J1) by
A1,
AFINSQ_1: 66;
then
A2: n
in (
dom (
Directed J1)) by
FUNCT_4: 99;
then
A3: ((
Directed J1)
. n)
in (
rng (
Directed J1)) by
FUNCT_1:def 3;
A4: (
Directed J1)
c= (
if=0 (a,I,J)) by
SCMFSA6A: 16;
then (
dom (
Directed J1))
c= (
dom (
if=0 (a,I,J))) by
GRFUNC_1: 2;
hence n
in (
dom (
if=0 (a,I,J))) by
A2;
((
if=0 (a,I,J))
. n)
= ((
Directed J1)
. n) by
A2,
A4,
GRFUNC_1: 2;
hence thesis by
A3,
COMPOS_1:def 11;
end;
theorem ::
SCMFSA8C:28
Th20: for a be
Int-Location, I,J be
MacroInstruction of
SCM+FSA , n be
Element of
NAT st n
< (((
card I)
+ (
card J))
+ 3) holds n
in (
dom (
if>0 (a,I,J))) & ((
if>0 (a,I,J))
. n)
<> (
halt
SCM+FSA )
proof
let a be
Int-Location;
let I,J be
MacroInstruction of
SCM+FSA ;
let n be
Element of
NAT ;
set J1 = ((((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
A1: (
card J1)
= ((
card (((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
>0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
assume n
< (((
card I)
+ (
card J))
+ 3);
then n
in (
dom J1) by
A1,
AFINSQ_1: 66;
then
A2: n
in (
dom (
Directed J1)) by
FUNCT_4: 99;
then
A3: ((
Directed J1)
. n)
in (
rng (
Directed J1)) by
FUNCT_1:def 3;
A4: (
Directed J1)
c= (
if>0 (a,I,J)) by
SCMFSA6A: 16;
then (
dom (
Directed J1))
c= (
dom (
if>0 (a,I,J))) by
GRFUNC_1: 2;
hence n
in (
dom (
if>0 (a,I,J))) by
A2;
((
if>0 (a,I,J))
. n)
= ((
Directed J1)
. n) by
A2,
A4,
GRFUNC_1: 2;
hence thesis by
A3,
COMPOS_1:def 11;
end;
theorem ::
SCMFSA8C:29
Th21: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA st (
Directed I)
is_pseudo-closed_on (s,P) holds (I
";" (
Stop
SCM+FSA ))
is_halting_on (s,P) & (
LifeSpan ((P
+* (I
";" (
Stop
SCM+FSA ))),(
Initialize s)))
= (
pseudo-LifeSpan (s,P,(
Directed I))) & (for n be
Nat st n
< (
pseudo-LifeSpan (s,P,(
Directed I))) holds (
IC (
Comput ((P
+* I),(
Initialize s),n)))
= (
IC (
Comput ((P
+* (I
";" (
Stop
SCM+FSA ))),(
Initialize s),n)))) & for n be
Nat st n
<= (
pseudo-LifeSpan (s,P,(
Directed I))) holds (
DataPart (
Comput ((P
+* I),(
Initialize s),n)))
= (
DataPart (
Comput ((P
+* (I
";" (
Stop
SCM+FSA ))),(
Initialize s),n)))
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
Program of
SCM+FSA ;
set I0 = (
Directed I);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s00 = (
Initialize s), P00 = (P
+* I0);
set s10 = (
Initialize s), P10 = (P
+* I1);
reconsider k = (
pseudo-LifeSpan (s00,P00,I0)) as
Element of
NAT by
ORDINAL1:def 12;
((
Stop
SCM+FSA )
.
0 )
= (
halt
SCM+FSA );
then
A1: (
halt
SCM+FSA )
= ((
Stop
SCM+FSA )
. ((
card I)
-' (
card I))) by
XREAL_1: 232;
A2: (
DataPart s00)
= (
DataPart s10);
assume
A3: I0
is_pseudo-closed_on (s,P);
then
A4: I0
is_pseudo-closed_on (s00,P00);
defpred
P[
Nat] means k
<= $1 implies (
IC (
Comput (P10,s10,$1)))
= (
card I) & (
CurInstr (P10,(
Comput (P10,s10,$1))))
= (
halt
SCM+FSA );
A5: I1
c= P10 by
FUNCT_4: 25;
A6: I1
c= P10 by
FUNCT_4: 25;
A7: I0
c= I1 by
SCMFSA6A: 16;
A8: I0
c= P10 by
A7,
A5,
XBOOLE_1: 1;
(
Reloc (I0,
0 ))
c= I1 by
A7;
then
A9: (
Reloc (I0,
0 ))
c= P10 by
A6,
XBOOLE_1: 1;
A10: (
IC s10)
=
0 by
FUNCT_4: 113;
A11: I0
c= P00 by
FUNCT_4: 25;
A12:
now
let n be
Nat;
assume
A13: n
<= (
pseudo-LifeSpan (s00,P00,I0));
then ((
IC (
Comput (P00,s00,n)))
+
0 )
= (
IC (
Comput (P10,s10,n))) by
A4,
A9,
A10,
A2,
Th14,
A11;
hence (
IC (
Comput (P00,s00,n)))
= (
IC (
Comput (P10,s10,n)));
thus (
DataPart (
Comput (P00,s00,n)))
= (
DataPart (
Comput (P10,s10,n))) by
A4,
A9,
A10,
A2,
A13,
Th14,
A11;
end;
A14: k
= (
pseudo-LifeSpan (s,P,I0)) by
A3,
Th13;
A15:
now
let n be
Nat;
assume
A16: n
< (
pseudo-LifeSpan (s00,P00,I0));
then (
IncAddr ((
CurInstr (P00,(
Comput (P00,s00,n)))),
0 ))
= (
CurInstr (P10,(
Comput (P10,s10,n)))) by
A4,
A9,
A10,
A2,
Th14,
A11;
hence (
CurInstr (P00,(
Comput (P00,s00,n))))
= (
CurInstr (P10,(
Comput (P10,s10,n)))) by
COMPOS_0: 3;
thus (
IC (
Comput (P00,s00,n)))
in (
dom I0) by
A4,
A16,
SCMFSA8A: 17;
thus (
CurInstr (P00,(
Comput (P00,s00,n))))
<> (
halt
SCM+FSA ) by
A4,
A16,
SCMFSA8A: 17;
end;
A17:
now
let n be
Nat;
assume
A18: (
CurInstr (P10,(
Comput (P10,s10,n))))
= (
halt
SCM+FSA );
reconsider l = (
IC (
Comput (P00,s00,n))) as
Element of
NAT ;
assume
A19: k
> n;
then
A20: l
in (
dom I0) by
A3,
A14,
SCMFSA8A:def 4;
(
CurInstr (P10,(
Comput (P10,s10,n))))
= (
CurInstr (P00,(
Comput (P00,s00,n)))) by
A15,
A19
.= (P00
. l) by
PBOOLE: 143
.= (I0
. l) by
A20,
A11,
GRFUNC_1: 2;
then (
halt
SCM+FSA )
in (
rng I0) by
A18,
A20,
FUNCT_1:def 3;
hence contradiction by
COMPOS_1:def 11;
end;
A21: (
card (
Stop
SCM+FSA ))
= 1 by
AFINSQ_1: 34;
then (
card I1)
= ((
card I)
+ 1) by
SCMFSA6A: 21;
then (
card I)
< (
card I1) by
NAT_1: 13;
then
A22: (
card I)
in (
dom I1) by
AFINSQ_1: 66;
(
card I)
< ((
card I)
+ (
card (
Stop
SCM+FSA ))) by
A21,
NAT_1: 13;
then
A23: (I1
. (
card I))
= (
IncAddr ((
halt
SCM+FSA ),(
card I))) by
A1,
Th2
.= (
halt
SCM+FSA ) by
COMPOS_0: 4;
then
A24: (P10
. (
card I))
= (
halt
SCM+FSA ) by
A22,
A5,
GRFUNC_1: 2;
A25: for n be
Nat st
P[n] holds
P[(n
+ 1)]
proof
let n be
Nat;
assume
A26:
P[n];
assume
A27: k
<= (n
+ 1);
hereby
per cases by
A27,
NAT_1: 8;
suppose k
= (n
+ 1);
hence (
IC (
Comput (P10,s10,(n
+ 1))))
= (
IC (
Comput (P00,s00,k))) by
A12
.= (
card I0) by
A3,
A14,
SCMFSA8A:def 4
.= (
card I) by
SCMFSA6A: 36;
end;
suppose
A28: k
<= n;
(
Comput (P10,s10,(n
+ 1)))
= (
Following (P10,(
Comput (P10,s10,n)))) by
EXTPRO_1: 3;
hence (
IC (
Comput (P10,s10,(n
+ 1))))
= (
card I) by
A26,
A28,
EXTPRO_1:def 3;
end;
end;
hence thesis by
A24,
PBOOLE: 143;
end;
A29:
P[
0 ]
proof
assume k
<=
0 ;
then k
=
0 ;
hence (
IC (
Comput (P10,s10,
0 )))
= (
IC (
Comput (P00,s00,k)))
.= (
card I0) by
A3,
A14,
SCMFSA8A:def 4
.= (
card I) by
SCMFSA6A: 36;
hence (
CurInstr (P10,(
Comput (P10,s10,
0 ))))
= (P10
. (
card I)) by
PBOOLE: 143
.= (
halt
SCM+FSA ) by
A23,
A22,
A5,
GRFUNC_1: 2;
end;
A30: for n be
Nat holds
P[n] from
NAT_1:sch 2(
A29,
A25);
set s1 = (
Initialize s), P1 = (P
+* I);
A31: I
c= P1 by
FUNCT_4: 25;
A32: (
card I0)
= (
card I) by
SCMFSA6A: 36;
P[k] by
A30;
then
A33: P10
halts_on s10 by
EXTPRO_1: 29;
hence I1
is_halting_on (s,P);
(
CurInstr (P10,(
Comput (P10,s10,k))))
= (
halt
SCM+FSA ) by
A30;
then
A34: (
LifeSpan (P10,s10))
= k by
A33,
A17,
EXTPRO_1:def 15;
defpred
P[
Nat] means $1
< (
pseudo-LifeSpan (s,P,I0)) implies (
IC (
Comput (P1,s1,$1)))
in (
dom I) & (
IC (
Comput (P1,s1,$1)))
= (
IC (
Comput (P10,s10,$1))) & (
DataPart (
Comput (P1,s1,$1)))
= (
DataPart (
Comput (P10,s10,$1)));
A35: for n be
Nat st
P[n] holds
P[(n
+ 1)]
proof
let n be
Nat;
set l = (
IC (
Comput (P1,s1,n)));
set l0 = (
IC (
Comput (P10,s10,n)));
assume
A36:
P[n];
assume
A37: (n
+ 1)
< (
pseudo-LifeSpan (s,P,I0));
then
A38: l0
in (
dom I0) by
A36,
FUNCT_4: 99,
NAT_1: 12;
A39: for f be
FinSeq-Location holds ((
Comput (P1,s1,n))
. f)
= ((
Comput (P10,s10,n))
. f) by
A36,
A37,
NAT_1: 12,
SCMFSA_M: 2;
for a be
Int-Location holds ((
Comput (P1,s1,n))
. a)
= ((
Comput (P10,s10,n))
. a) by
A36,
A37,
NAT_1: 12,
SCMFSA_M: 2;
then
A40: (
Comput (P1,s1,n))
= (
Comput (P10,s10,n)) by
A36,
A37,
A39,
NAT_1: 12,
SCMFSA_2: 61;
A41:
now
assume
A42: (I
. l)
= (
halt
SCM+FSA );
A43: (P00
/. (
IC (
Comput (P00,s00,n))))
= (P00
. (
IC (
Comput (P00,s00,n)))) by
PBOOLE: 143;
n
< k by
A14,
A37,
NAT_1: 12;
then
A44: (
CurInstr (P00,(
Comput (P00,s00,n))))
= (P00
. l0) by
A12,
A43
.= (I0
. l0) by
A38,
A11,
GRFUNC_1: 2
.= (
goto (
card I)) by
A36,
A37,
A42,
NAT_1: 12,
SCMFSA8A: 16;
A45: (
IC (
Comput (P00,s00,(n
+ 1))))
= (
IC (
Following (P00,(
Comput (P00,s00,n))))) by
EXTPRO_1: 3
.= (
card I) by
A44,
SCMFSA_2: 69
.= (
card I0) by
SCMFSA6A: 36;
(
IC (
Comput (P00,s00,(n
+ 1))))
in (
dom I0) by
A3,
A37,
SCMFSA8A: 17;
hence contradiction by
A45;
end;
A46: (
CurInstr (P1,(
Comput (P1,s1,n))))
= (P1
. l) by
PBOOLE: 143
.= (I
. l) by
A31,
A36,
A37,
GRFUNC_1: 2,
NAT_1: 12
.= (I0
. l0) by
A36,
A37,
A41,
NAT_1: 12,
SCMFSA8A: 16
.= (P10
. l0) by
A38,
A8,
GRFUNC_1: 2
.= (
CurInstr (P10,(
Comput (P10,s10,n)))) by
PBOOLE: 143;
A47: (
Comput (P10,s10,(n
+ 1)))
= (
Following (P10,(
Comput (P10,s10,n)))) by
EXTPRO_1: 3
.= (
Exec ((
CurInstr (P1,(
Comput (P1,s1,n)))),(
Comput (P10,s10,n)))) by
A46;
(
pseudo-LifeSpan (s,P,I0))
= k by
A3,
Th13;
then
A48: (
IC (
Comput (P00,s00,(n
+ 1))))
= (
IC (
Comput (P10,s10,(n
+ 1)))) by
A12,
A37;
A49: (
dom I0)
= (
dom I) by
FUNCT_4: 99;
(
Comput (P1,s1,(n
+ 1)))
= (
Following (P1,(
Comput (P1,s1,n)))) by
EXTPRO_1: 3;
then
A50: (
Comput (P1,s1,(n
+ 1)))
= (
Comput (P10,s10,(n
+ 1))) by
A47,
A40;
A51: for f be
FinSeq-Location holds ((
Comput (P1,s1,(n
+ 1)))
. f)
= ((
Comput (P10,s10,(n
+ 1)))
. f) by
A50;
(
IC (
Comput (P00,s00,(n
+ 1))))
in (
dom I0) by
A3,
A37,
SCMFSA8A: 17;
hence (
IC (
Comput (P1,s1,(n
+ 1))))
in (
dom I) by
A48,
A49,
A50;
thus (
IC (
Comput (P1,s1,(n
+ 1))))
= (
IC (
Comput (P10,s10,(n
+ 1)))) by
A50;
for a be
Int-Location holds ((
Comput (P1,s1,(n
+ 1)))
. a)
= ((
Comput (P10,s10,(n
+ 1)))
. a) by
A50;
hence thesis by
A51,
SCMFSA_M: 2;
end;
(
IC (
Comput (P10,s10,k)))
= (
card I) by
A30;
then
A52: (
IC (
Comput (P00,s00,(
LifeSpan (P10,s10)))))
= (
card I) by
A12,
A34;
for n be
Nat st not (
IC (
Comput (P00,s00,n)))
in (
dom I0) holds (
LifeSpan (P10,s10))
<= n by
A15,
A34;
hence (
LifeSpan (P10,s10))
= (
pseudo-LifeSpan (s,P,I0)) by
A3,
A52,
A32,
SCMFSA8A:def 4;
A53:
P[
0 ]
proof
A54: (
IC (
Comput (P1,s1,
0 )))
= (
IC s1)
.= (
IC (
Initialize s))
.=
0 by
FUNCT_4: 113;
assume
0
< (
pseudo-LifeSpan (s,P,I0));
then (
IC (
Comput ((P
+* I0),(
Initialize s),
0 )))
in (
dom I0) by
A3,
SCMFSA8A: 17;
then (
IC (
Initialize s))
in (
dom I0);
then
0
in (
dom I0) by
MEMSTR_0: 16;
hence (
IC (
Comput (P1,s1,
0 )))
in (
dom I) by
A54,
FUNCT_4: 99;
thus (
IC (
Comput (P1,s1,
0 )))
= (
IC (
Comput (P10,s10,
0 )));
thus (
DataPart (
Comput (P1,s1,
0 )))
= (
DataPart s1)
.= (
DataPart s10)
.= (
DataPart (
Comput (P10,s10,
0 )));
end;
A55: for n be
Nat holds
P[n] from
NAT_1:sch 2(
A53,
A35);
hence for n be
Nat st n
< (
pseudo-LifeSpan (s,P,I0)) holds (
IC (
Comput (P1,s1,n)))
= (
IC (
Comput (P10,s10,n)));
let n be
Nat;
assume
A56: n
<= (
pseudo-LifeSpan (s,P,(
Directed I)));
per cases by
A56,
XXREAL_0: 1;
suppose n
< (
pseudo-LifeSpan (s,P,I0));
hence thesis by
A55;
end;
suppose
A57: n
= (
pseudo-LifeSpan (s,P,I0));
per cases by
NAT_1: 6;
suppose
A58: n
=
0 ;
hence (
DataPart (
Comput (P1,s1,n)))
= (
DataPart s1)
.= (
DataPart s10)
.= (
DataPart (
Comput (P10,s10,n))) by
A58;
end;
suppose ex m be
Nat st n
= (m
+ 1);
then
consider m be
Nat such that
A59: n
= (m
+ 1);
reconsider m as
Element of
NAT by
ORDINAL1:def 12;
A60: (
Comput (P10,s10,n))
= (
Following (P10,(
Comput (P10,s10,m)))) by
A59,
EXTPRO_1: 3;
set i = (
CurInstr (P1,(
Comput (P1,s1,m))));
A61: (
Comput (P1,s1,n))
= (
Following (P1,(
Comput (P1,s1,m)))) by
A59,
EXTPRO_1: 3;
set l0 = (
IC (
Comput (P10,s10,m)));
set l = (
IC (
Comput (P1,s1,m)));
A62: (m
+
0 )
< (
pseudo-LifeSpan (s,P,I0)) by
A57,
A59,
XREAL_1: 6;
then
A63: l
= l0 by
A55;
A64: l
in (
dom I) by
A55,
A62;
then
A65: l0
in (
dom I0) by
A63,
FUNCT_4: 99;
A66: i
= (P1
. l) by
PBOOLE: 143
.= (I
. l) by
A31,
A64,
GRFUNC_1: 2;
A67: I0
c= I1 by
SCMFSA6A: 16;
then
A68: (
dom I0)
c= (
dom I1) by
RELAT_1: 11;
A69: (I0
. l0)
= (I1
. l0) by
A65,
A67,
GRFUNC_1: 2
.= (P10
. l0) by
A5,
A68,
A65,
GRFUNC_1: 2
.= (
CurInstr (P10,(
Comput (P10,s10,m)))) by
PBOOLE: 143;
A70: (
DataPart (
Comput (P1,s1,m)))
= (
DataPart (
Comput (P10,s10,m))) by
A55,
A62;
per cases ;
suppose
A71: i
= (
halt
SCM+FSA );
then (
CurInstr (P10,(
Comput (P10,s10,m))))
= (
goto (
card I)) by
A64,
A63,
A66,
A69,
SCMFSA8A: 16;
then (
InsCode (
CurInstr (P10,(
Comput (P10,s10,m)))))
= 6 by
SCMFSA_2: 23;
then
A72: (
InsCode (
CurInstr (P10,(
Comput (P10,s10,m)))))
in
{
0 , 6, 7, 8} by
ENUMSET1:def 2;
thus (
DataPart (
Comput (P1,s1,n)))
= (
DataPart (
Comput (P1,s1,m))) by
A61,
A71,
EXTPRO_1:def 3
.= (
DataPart (
Comput (P10,s10,m))) by
A55,
A62
.= (
DataPart (
Comput (P10,s10,n))) by
A60,
A72,
Th6;
end;
suppose i
<> (
halt
SCM+FSA );
then (
CurInstr (P10,(
Comput (P10,s10,m))))
= i by
A64,
A63,
A66,
A69,
SCMFSA8A: 16;
hence thesis by
A61,
A60,
A70,
SCMFSA6C: 4;
end;
end;
end;
end;
theorem ::
SCMFSA8C:30
Th22: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA st (
Directed I)
is_pseudo-closed_on (s,P) holds (
DataPart (
Result ((P
+* (I
";" (
Stop
SCM+FSA ))),(
Initialize s))))
= (
DataPart (
Comput ((P
+* I),(
Initialize s),(
pseudo-LifeSpan (s,P,(
Directed I))))))
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
Program of
SCM+FSA ;
set I0 = (
Directed I);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s2 = (
Initialize s), P2 = (P
+* I);
set s10 = (
Initialize s), P10 = (P
+* I1);
set k = (
pseudo-LifeSpan (s,P,I0));
assume
A1: I0
is_pseudo-closed_on (s,P);
then
A2: (
DataPart (
Comput (P2,s2,k)))
= (
DataPart (
Comput (P10,s10,k))) by
Th21;
I1
is_halting_on (s,P) by
A1,
Th21;
then
A3: P10
halts_on s10;
(
LifeSpan (P10,s10))
= k by
A1,
Th21;
hence thesis by
A2,
A3,
EXTPRO_1: 23;
end;
theorem ::
SCMFSA8C:31
for s be
State of
SCM+FSA , I be
Program of
SCM+FSA st (s
. (
intloc
0 ))
= 1 & (
Directed I)
is_pseudo-closed_on (s,P) holds (
DataPart (
IExec ((I
";" (
Stop
SCM+FSA )),P,s)))
= (
DataPart (
Comput ((P
+* I),(
Initialize s),(
pseudo-LifeSpan (s,P,(
Directed I))))))
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
Program of
SCM+FSA ;
set I0 = (
Directed I);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s2 = (
Initialize s), P2 = (P
+* I);
set s10 = (
Initialize s), P10 = (P
+* I1);
set k = (
pseudo-LifeSpan (s,P,I0));
assume
A1: (s
. (
intloc
0 ))
= 1;
assume
A2: I0
is_pseudo-closed_on (s,P);
A3: s10
= (
Initialized s) by
A1,
SCMFSA_M: 18;
thus (
DataPart (
IExec (I1,P,s)))
= (
DataPart (
Result (P10,s10))) by
A3
.= (
DataPart (
Comput (P2,s2,k))) by
A2,
Th22;
end;
theorem ::
SCMFSA8C:32
Th24: for I,J be
MacroInstruction of
SCM+FSA , a be
Int-Location holds ((
if=0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3))
= (
halt
SCM+FSA )
proof
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
Int-Location;
set II = ((((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
A1: (
card II)
= ((
card (((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
=0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
then
A2: ((((
card I)
+ (
card J))
+ 3)
-' (
card II))
=
0 by
XREAL_1: 232;
A3: ((
Stop
SCM+FSA )
.
0 )
= (
halt
SCM+FSA );
(
card (
Stop
SCM+FSA ))
= 1 by
AFINSQ_1: 34;
then (((
card I)
+ (
card J))
+ 3)
< ((
card II)
+ (
card (
Stop
SCM+FSA ))) by
A1,
NAT_1: 13;
hence ((
if=0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3))
= (
IncAddr ((
halt
SCM+FSA ),(
card II))) by
A1,
A2,
Th2,
A3
.= (
halt
SCM+FSA ) by
COMPOS_0: 4;
end;
theorem ::
SCMFSA8C:33
Th25: for I,J be
MacroInstruction of
SCM+FSA , a be
Int-Location holds ((
if>0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3))
= (
halt
SCM+FSA )
proof
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
Int-Location;
set II = ((((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
A1: (
card II)
= ((
card (((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
>0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
then
A2: ((((
card I)
+ (
card J))
+ 3)
-' (
card II))
=
0 by
XREAL_1: 232;
A3: ((
Stop
SCM+FSA )
.
0 )
= (
halt
SCM+FSA );
(
card (
Stop
SCM+FSA ))
= 1 by
AFINSQ_1: 34;
then (((
card I)
+ (
card J))
+ 3)
< ((
card II)
+ (
card (
Stop
SCM+FSA ))) by
A1,
NAT_1: 13;
hence ((
if>0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3))
= (
IncAddr ((
halt
SCM+FSA ),(
card II))) by
A1,
A2,
Th2,
A3
.= (
halt
SCM+FSA ) by
COMPOS_0: 4;
end;
theorem ::
SCMFSA8C:34
Th26: for I,J be
MacroInstruction of
SCM+FSA , a be
Int-Location holds ((
if=0 (a,I,J))
. ((
card J)
+ 2))
= (
goto (((
card I)
+ (
card J))
+ 3))
proof
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
Int-Location;
set JJ = ((a
=0_goto ((
card J)
+ 3))
";" J);
set J3 = (((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)));
A1: (
card JJ)
= ((
card (
Macro (a
=0_goto ((
card J)
+ 3))))
+ (
card J)) by
SCMFSA6A: 21
.= (2
+ (
card J)) by
COMPOS_1: 56;
then (((
card J)
+ 2)
-' (
card JJ))
=
0 by
XREAL_1: 232;
then
A2: (
goto ((
card I)
+ 1))
= ((
Goto ((
card I)
+ 1))
. (((
card J)
+ 2)
-' (
card JJ)));
(
card (
Goto ((
card I)
+ 1)))
= 1 by
SCMFSA8A: 15;
then ((
card J)
+ 2)
< ((
card JJ)
+ (
card (
Goto ((
card I)
+ 1)))) by
A1,
NAT_1: 13;
then
A3: (J3
. ((
card J)
+ 2))
= (
IncAddr ((
goto ((
card I)
+ 1)),(
card JJ))) by
A1,
A2,
Th2
.= (
goto (((
card I)
+ 1)
+ ((
card J)
+ 2))) by
A1,
SCMFSA_4: 1
.= (
goto (((
card I)
+ (
card J))
+ (1
+ 2)));
(
card (
Goto ((
card I)
+ 1)))
= 1 by
SCMFSA8A: 15;
then (
card J3)
= (((
card J)
+ 2)
+ 1) by
A1,
SCMFSA6A: 21
.= ((
card J)
+ (2
+ 1));
then (
card J3)
= (((
card J)
+ 2)
+ 1);
then ((
card J)
+ 2)
< (
card J3) by
NAT_1: 13;
then
A4: ((
card J)
+ 2)
in (
dom J3) by
AFINSQ_1: 66;
then ((J3
";" (I
";" (
Stop
SCM+FSA )))
. ((
card J)
+ 2))
= ((
Directed J3)
. ((
card J)
+ 2)) by
SCMFSA8A: 14
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
A3,
A4,
SCMFSA8A: 16;
hence thesis by
SCMFSA6A: 25;
end;
theorem ::
SCMFSA8C:35
Th27: for I,J be
MacroInstruction of
SCM+FSA , a be
Int-Location holds ((
if>0 (a,I,J))
. ((
card J)
+ 2))
= (
goto (((
card I)
+ (
card J))
+ 3))
proof
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
Int-Location;
set JJ = ((a
>0_goto ((
card J)
+ 3))
";" J);
set J3 = (((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)));
A1: (
card JJ)
= ((
card (
Macro (a
>0_goto ((
card J)
+ 3))))
+ (
card J)) by
SCMFSA6A: 21
.= (2
+ (
card J)) by
COMPOS_1: 56;
then (((
card J)
+ 2)
-' (
card JJ))
=
0 by
XREAL_1: 232;
then
A2: (
goto ((
card I)
+ 1))
= ((
Goto ((
card I)
+ 1))
. (((
card J)
+ 2)
-' (
card JJ)));
(
card (
Goto ((
card I)
+ 1)))
= 1 by
SCMFSA8A: 15;
then ((
card J)
+ 2)
< ((
card JJ)
+ (
card (
Goto ((
card I)
+ 1)))) by
A1,
NAT_1: 13;
then
A3: (J3
. ((
card J)
+ 2))
= (
IncAddr ((
goto ((
card I)
+ 1)),(
card JJ))) by
A1,
A2,
Th2
.= (
goto (((
card I)
+ 1)
+ ((
card J)
+ 2))) by
A1,
SCMFSA_4: 1
.= (
goto (((
card I)
+ (
card J))
+ (1
+ 2)));
(
card (
Goto ((
card I)
+ 1)))
= 1 by
SCMFSA8A: 15;
then (
card J3)
= (((
card J)
+ 2)
+ 1) by
A1,
SCMFSA6A: 21
.= ((
card J)
+ (2
+ 1));
then (
card J3)
= (((
card J)
+ 2)
+ 1);
then ((
card J)
+ 2)
< (
card J3) by
NAT_1: 13;
then
A4: ((
card J)
+ 2)
in (
dom J3) by
AFINSQ_1: 66;
then ((J3
";" (I
";" (
Stop
SCM+FSA )))
. ((
card J)
+ 2))
= ((
Directed J3)
. ((
card J)
+ 2)) by
SCMFSA8A: 14
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
A3,
A4,
SCMFSA8A: 16;
hence thesis by
SCMFSA6A: 25;
end;
::$Canceled
theorem ::
SCMFSA8C:37
Th28: for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. a)
=
0 & (
Directed I)
is_pseudo-closed_on (s,P) holds (
if=0 (a,I,J))
is_halting_on (s,P) & (
LifeSpan ((P
+* (
if=0 (a,I,J))),(
Initialize s)))
= ((
LifeSpan ((P
+* (I
";" (
Stop
SCM+FSA ))),(
Initialize s)))
+ 1)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set I0 = (
Directed I);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s00 = (
Initialize s), P00 = (P
+* I0);
set s3 = (
Initialize s), P3 = (P
+* (
if=0 (a,I,J)));
A1: (
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
set s4 = (
Comput (P3,s3,1));
set i = (a
=0_goto ((
card J)
+ 3));
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 11
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if=0 (a,I,J))) by
NAT_1: 13;
then
A2: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 66;
A3: (
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
A4:
0
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 65;
A5: (P3
.
0 )
= ((
if=0 (a,I,J))
.
0 ) by
A4,
A1,
GRFUNC_1: 2
.= i by
Th18;
A6: (
card ((i
";" J)
";" (
Goto ((
card I)
+ 1))))
= ((
card ((
Macro i)
";" J))
+ (
card (
Goto ((
card I)
+ 1)))) by
SCMFSA6A: 21
.= ((
card ((
Macro i)
";" J))
+ 1) by
SCMFSA8A: 15
.= (((
card (
Macro i))
+ (
card J))
+ 1) by
SCMFSA6A: 21
.= (((
card J)
+ 2)
+ 1) by
COMPOS_1: 56
.= ((
card J)
+ (2
+ 1));
A7: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A8: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A7,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
A9: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A8,
A5,
PBOOLE: 143;
(
if=0 (a,I,J))
= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I1) by
SCMFSA6A: 25;
then (
Reloc (I1,((
card J)
+ 3)))
c= (
if=0 (a,I,J)) by
A6,
SCMFSA6A: 38;
then
A10: (
Reloc (I1,((
card J)
+ 3)))
c= P3 by
A3,
XBOOLE_1: 1;
(
Reloc (I0,((
card J)
+ 3)))
c= (
Reloc (I1,((
card J)
+ 3))) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A11: (
Reloc (I0,((
card J)
+ 3)))
c= P3 by
A10,
XBOOLE_1: 1;
A12: for f be
FinSeq-Location holds (s00
. f)
= (s4
. f) by
A9,
SCMFSA_2: 70;
for a be
Int-Location holds (s00
. a)
= (s4
. a) by
A9,
SCMFSA_2: 70;
then
A13: (
DataPart s00)
= (
DataPart s4) by
A12,
SCMFSA_M: 2;
A14: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A14,
TARSKI:def 1;
then
A15: not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
assume (s
. a)
=
0 ;
then (s3
. a)
=
0 by
A15,
FUNCT_4: 11;
then
A16: (
IC (
Comput (P3,s3,1)))
= ((
card J)
+ 3) by
A9,
SCMFSA_2: 70;
assume
A17: I0
is_pseudo-closed_on (s,P);
then
A18: (
pseudo-LifeSpan (s,P,I0))
= (
LifeSpan ((P
+* I1),(
Initialize s))) by
Th21;
A19: I0
is_pseudo-closed_on (s00,P00) by
A17;
A20: I0
c= P00 by
FUNCT_4: 25;
(
IC (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1))))
= (
IC (
Comput (P3,s4,(
pseudo-LifeSpan (s00,P00,I0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,I0)))))
+ ((
card J)
+ 3)) by
A19,
A11,
A16,
A13,
Th14,
A20
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,I0)))))
+ ((
card J)
+ 3)) by
A17,
Th13
.= ((
card I0)
+ ((
card J)
+ 3)) by
A17,
SCMFSA8A:def 4
.= ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36
.= (((
card I)
+ (
card J))
+ 3);
then
A21: (
CurInstr (P3,(
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A2,
A1,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th24;
then
A22: P3
halts_on s3 by
EXTPRO_1: 29;
hence (
if=0 (a,I,J))
is_halting_on (s,P);
now
set J1 = ((((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
let k be
Nat;
assume
A23: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
assume not ((
pseudo-LifeSpan (s00,P00,I0))
+ 1)
<= k;
then
A24: k
<= (
pseudo-LifeSpan (s00,P00,I0)) by
NAT_1: 13;
A25:
0
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 65;
A26: (P3
/. (
IC s3))
= (P3
. (
IC s3)) by
PBOOLE: 143;
(
CurInstr (P3,(
Comput (P3,s3,
0 ))))
= (P3
.
0 ) by
A26,
MEMSTR_0: 16
.= ((
if=0 (a,I,J))
.
0 ) by
A25,
A1,
GRFUNC_1: 2
.= (a
=0_goto ((
card J)
+ 3)) by
Th18;
then
consider k1 be
Nat such that
A27: (k1
+ 1)
= k by
A23,
NAT_1: 6;
reconsider k1 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k1))) as
Element of
NAT ;
k1
< k by
A27,
XREAL_1: 29;
then
A28: k1
< (
pseudo-LifeSpan (s00,P00,I0)) by
A24,
XXREAL_0: 2;
then k1
< (
pseudo-LifeSpan (s,P,I0)) by
A17,
Th13;
then n
in (
dom I0) by
A17,
SCMFSA8A: 17;
then n
< (
card I0) by
AFINSQ_1: 66;
then (n
+ ((
card J)
+ 3))
< ((
card I0)
+ ((
card J)
+ 3)) by
XREAL_1: 6;
then
A29: (n
+ ((
card J)
+ 3))
< ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36;
A30: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s4,k1))) by
A27,
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,k1)))
+ ((
card J)
+ 3)) by
A19,
A11,
A16,
A13,
A28,
Th14,
A20;
(
card J1)
= ((
card (((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
=0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
then (
IC (
Comput (P3,s3,k)))
in (
dom J1) by
A30,
A29,
AFINSQ_1: 66;
then
A31: (
IC (
Comput (P3,s3,k)))
in (
dom (
Directed J1)) by
FUNCT_4: 99;
then
A32: ((
Directed J1)
. (
IC (
Comput (P3,s3,k))))
in (
rng (
Directed J1)) by
FUNCT_1:def 3;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 11
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if=0 (a,I,J))) by
XREAL_1: 29;
then (n
+ ((
card J)
+ 3))
< (
card (
if=0 (a,I,J))) by
A29,
XXREAL_0: 2;
then
A33: (
IC (
Comput (P3,s3,k)))
in (
dom (
if=0 (a,I,J))) by
A30,
AFINSQ_1: 66;
A34: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A33,
A1,
GRFUNC_1: 2;
(
Directed J1)
c= (
if=0 (a,I,J)) by
SCMFSA6A: 16;
then ((
if=0 (a,I,J))
. (
IC (
Comput (P3,s3,k))))
= ((
Directed J1)
. (
IC (
Comput (P3,s3,k)))) by
A31,
GRFUNC_1: 2;
hence contradiction by
A23,
A32,
A34,
COMPOS_1:def 11;
end;
then (
LifeSpan (P3,s3))
= ((
pseudo-LifeSpan (s00,P00,I0))
+ 1) by
A21,
A22,
EXTPRO_1:def 15;
hence thesis by
A17,
A18,
Th13;
end;
theorem ::
SCMFSA8C:38
for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. (
intloc
0 ))
= 1 & (s
. a)
=
0 & (
Directed I)
is_pseudo-closed_on (s,P) holds (
DataPart (
IExec ((
if=0 (a,I,J)),P,s)))
= (
DataPart (
IExec ((I
";" (
Stop
SCM+FSA )),P,s)))
proof
let ss be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set I0 = (
Directed I);
set s = (
Initialized ss);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s00 = (
Initialize s), P00 = (P
+* I0);
set s3 = (
Initialize s), P3 = (P
+* (
if=0 (a,I,J)));
A1: (
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
set s4 = (
Comput (P3,s3,1));
set i = (a
=0_goto ((
card J)
+ 3));
A2: I0
c= P00 by
FUNCT_4: 25;
assume
A3: (ss
. (
intloc
0 ))
= 1;
set s1 = (
Initialize s), P1 = (P
+* I1);
assume (ss
. a)
=
0 ;
then
A4: (s
. a)
=
0 by
SCMFSA_M: 37;
A5: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A6: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A5,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
A7:
0
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 65;
A8: (P3
.
0 )
= ((
if=0 (a,I,J))
.
0 ) by
A7,
FUNCT_4: 13
.= i by
Th18;
A9: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A6,
A8,
PBOOLE: 143;
A10: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A10,
TARSKI:def 1;
then
A11: not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
(s3
. a)
=
0 by
A11,
A4,
FUNCT_4: 11;
then
A12: (
IC (
Comput (P3,s3,1)))
= ((
card J)
+ 3) by
A9,
SCMFSA_2: 70;
assume I0
is_pseudo-closed_on (ss,P);
then
A13: I0
is_pseudo-closed_on (s,P) by
A3,
Th16;
then
A14: (
LifeSpan (P1,s1))
= (
pseudo-LifeSpan (s,P,I0)) by
Th21;
A15: I0
is_pseudo-closed_on (s00,P00) by
A13;
A16: for f be
FinSeq-Location holds (s00
. f)
= (s4
. f) by
A9,
SCMFSA_2: 70;
for a be
Int-Location holds (s00
. a)
= (s4
. a) by
A9,
SCMFSA_2: 70;
then
A17: (
DataPart s00)
= (
DataPart s4) by
A16,
SCMFSA_M: 2;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 11
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if=0 (a,I,J))) by
NAT_1: 13;
then
A18: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 66;
A19: (
card ((i
";" J)
";" (
Goto ((
card I)
+ 1))))
= ((
card ((
Macro i)
";" J))
+ (
card (
Goto ((
card I)
+ 1)))) by
SCMFSA6A: 21
.= ((
card ((
Macro i)
";" J))
+ 1) by
SCMFSA8A: 15
.= (((
card (
Macro i))
+ (
card J))
+ 1) by
SCMFSA6A: 21
.= (((
card J)
+ 2)
+ 1) by
COMPOS_1: 56
.= ((
card J)
+ (2
+ 1));
A20: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
A21: (
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
(
if=0 (a,I,J))
= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I1) by
SCMFSA6A: 25;
then (
Reloc (I1,((
card J)
+ 3)))
c= (
if=0 (a,I,J)) by
A19,
SCMFSA6A: 38;
then
A22: (
Reloc (I1,((
card J)
+ 3)))
c= P3 by
A21,
XBOOLE_1: 1;
(
Reloc (I0,((
card J)
+ 3)))
c= (
Reloc (I1,((
card J)
+ 3))) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A23: (
Reloc (I0,((
card J)
+ 3)))
c= P3 by
A22,
XBOOLE_1: 1;
(
IC (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1))))
= (
IC (
Comput (P3,s4,(
pseudo-LifeSpan (s00,P00,I0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,I0)))))
+ ((
card J)
+ 3)) by
A15,
A23,
A12,
A17,
Th14,
A2
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,I0)))))
+ ((
card J)
+ 3)) by
A13,
Th13
.= ((
card I0)
+ ((
card J)
+ 3)) by
A13,
SCMFSA8A:def 4
.= ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36
.= (((
card I)
+ (
card J))
+ 3);
then
A24: (
CurInstr (P3,(
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A18,
A1,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th24;
then
A25: P3
halts_on s3 by
EXTPRO_1: 29;
now
set J1 = ((((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
let k be
Nat;
assume
A26: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
assume not ((
pseudo-LifeSpan (s00,P00,I0))
+ 1)
<= k;
then
A27: k
<= (
pseudo-LifeSpan (s00,P00,I0)) by
NAT_1: 13;
A28:
0
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 65;
A29: (P3
/. (
IC s3))
= (P3
. (
IC s3)) by
PBOOLE: 143;
(
CurInstr (P3,(
Comput (P3,s3,
0 ))))
= (P3
.
0 ) by
A29,
MEMSTR_0: 16
.= ((
if=0 (a,I,J))
.
0 ) by
A28,
A1,
GRFUNC_1: 2
.= (a
=0_goto ((
card J)
+ 3)) by
Th18;
then
consider k1 be
Nat such that
A30: (k1
+ 1)
= k by
A26,
NAT_1: 6;
reconsider k1 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k1))) as
Element of
NAT ;
k1
< k by
A30,
XREAL_1: 29;
then
A31: k1
< (
pseudo-LifeSpan (s00,P00,I0)) by
A27,
XXREAL_0: 2;
then k1
< (
pseudo-LifeSpan (s,P,I0)) by
A13,
Th13;
then n
in (
dom I0) by
A13,
SCMFSA8A: 17;
then n
< (
card I0) by
AFINSQ_1: 66;
then (n
+ ((
card J)
+ 3))
< ((
card I0)
+ ((
card J)
+ 3)) by
XREAL_1: 6;
then
A32: (n
+ ((
card J)
+ 3))
< ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36;
A33: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s4,k1))) by
A30,
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,k1)))
+ ((
card J)
+ 3)) by
A15,
A23,
A12,
A17,
A31,
Th14,
A2;
(
card J1)
= ((
card (((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
=0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
=0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
then (
IC (
Comput (P3,s3,k)))
in (
dom J1) by
A33,
A32,
AFINSQ_1: 66;
then
A34: (
IC (
Comput (P3,s3,k)))
in (
dom (
Directed J1)) by
FUNCT_4: 99;
then
A35: ((
Directed J1)
. (
IC (
Comput (P3,s3,k))))
in (
rng (
Directed J1)) by
FUNCT_1:def 3;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 11
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if=0 (a,I,J))) by
XREAL_1: 29;
then (n
+ ((
card J)
+ 3))
< (
card (
if=0 (a,I,J))) by
A32,
XXREAL_0: 2;
then
A36: (
IC (
Comput (P3,s3,k)))
in (
dom (
if=0 (a,I,J))) by
A33,
AFINSQ_1: 66;
A37: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A36,
A1,
GRFUNC_1: 2;
(
Directed J1)
c= (
if=0 (a,I,J)) by
SCMFSA6A: 16;
then ((
if=0 (a,I,J))
. (
IC (
Comput (P3,s3,k))))
= ((
Directed J1)
. (
IC (
Comput (P3,s3,k)))) by
A34,
GRFUNC_1: 2;
hence contradiction by
A26,
A35,
A37,
COMPOS_1:def 11;
end;
then
A38: (
LifeSpan (P3,s3))
= ((
pseudo-LifeSpan (s00,P00,I0))
+ 1) by
A24,
A25,
EXTPRO_1:def 15;
A39: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
A40: (I0
";" (
Stop
SCM+FSA ))
= I1;
A41: (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,I0)))))
= (
DataPart (
Comput (P1,s1,(
pseudo-LifeSpan (s,P,I0))))) by
A13,
A40,
Th21;
I1
is_halting_on (s,P) by
A13,
Th21;
then
A42: P1
halts_on s1;
thus (
DataPart (
IExec ((
if=0 (a,I,J)),P,ss)))
= (
DataPart (
IExec ((
if=0 (a,I,J)),P,s)))
.= (
DataPart (
Result (P3,s3))) by
A20
.= (
DataPart (
Comput (P3,s3,(
LifeSpan (P3,s3))))) by
A25,
EXTPRO_1: 23
.= (
DataPart (
Comput (P3,s4,(
pseudo-LifeSpan (s00,P00,I0))))) by
A38,
EXTPRO_1: 4
.= (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,I0))))) by
A15,
A23,
A12,
A17,
Th14,
A2
.= (
DataPart (
Comput (P1,s1,(
LifeSpan (P1,s1))))) by
A13,
A14,
A41,
Th13
.= (
DataPart (
Result (P1,s1))) by
A42,
EXTPRO_1: 23
.= (
DataPart (
IExec (I1,P,s))) by
A39
.= (
DataPart (
IExec (I1,P,ss)));
end;
theorem ::
SCMFSA8C:39
Th30: for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. a)
>
0 & (
Directed I)
is_pseudo-closed_on (s,P) holds (
if>0 (a,I,J))
is_halting_on (s,P) & (
LifeSpan ((P
+* (
if>0 (a,I,J))),(
Initialize s)))
= ((
LifeSpan ((P
+* (I
";" (
Stop
SCM+FSA ))),(
Initialize s)))
+ 1)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set I0 = (
Directed I);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s00 = (
Initialize s), P00 = (P
+* I0);
set s3 = (
Initialize s), P3 = (P
+* (
if>0 (a,I,J)));
set s4 = (
Comput (P3,s3,1));
set i = (a
>0_goto ((
card J)
+ 3));
A1: I0
c= P00 by
FUNCT_4: 25;
A2: (
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 12
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if>0 (a,I,J))) by
NAT_1: 13;
then
A3: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 66;
A4: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A5: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A4,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
A6:
0
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 65;
A7: (P3
.
0 )
= ((
if>0 (a,I,J))
.
0 ) by
A6,
FUNCT_4: 13
.= i by
Th18;
A8: (
card ((i
";" J)
";" (
Goto ((
card I)
+ 1))))
= ((
card ((
Macro i)
";" J))
+ (
card (
Goto ((
card I)
+ 1)))) by
SCMFSA6A: 21
.= ((
card ((
Macro i)
";" J))
+ 1) by
SCMFSA8A: 15
.= (((
card (
Macro i))
+ (
card J))
+ 1) by
SCMFSA6A: 21
.= (((
card J)
+ 2)
+ 1) by
COMPOS_1: 56
.= ((
card J)
+ (2
+ 1));
A9: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A5,
A7,
PBOOLE: 143;
A10: (
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
(
if>0 (a,I,J))
= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I1) by
SCMFSA6A: 25;
then (
Reloc (I1,((
card J)
+ 3)))
c= (
if>0 (a,I,J)) by
A8,
SCMFSA6A: 38;
then
A11: (
Reloc (I1,((
card J)
+ 3)))
c= P3 by
A10,
XBOOLE_1: 1;
(
Reloc (I0,((
card J)
+ 3)))
c= (
Reloc (I1,((
card J)
+ 3))) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A12: (
Reloc (I0,((
card J)
+ 3)))
c= P3 by
A11,
XBOOLE_1: 1;
A13: for f be
FinSeq-Location holds (s00
. f)
= (s4
. f) by
A9,
SCMFSA_2: 71;
for a be
Int-Location holds (s00
. a)
= (s4
. a) by
A9,
SCMFSA_2: 71;
then
A14: (
DataPart s00)
= (
DataPart s4) by
A13,
SCMFSA_M: 2;
A15: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A15,
TARSKI:def 1;
then not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
then
A16: (s3
. a)
= (s
. a) by
FUNCT_4: 11;
assume (s
. a)
>
0 ;
then
A17: (
IC (
Comput (P3,s3,1)))
= ((
card J)
+ 3) by
A9,
A16,
SCMFSA_2: 71;
assume
A18: I0
is_pseudo-closed_on (s,P);
then
A19: (
pseudo-LifeSpan (s,P,I0))
= (
LifeSpan ((P
+* I1),(
Initialize s))) by
Th21;
A20: I0
is_pseudo-closed_on (s00,P00) by
A18;
(
IC (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1))))
= (
IC (
Comput (P3,s4,(
pseudo-LifeSpan (s00,P00,I0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,I0)))))
+ ((
card J)
+ 3)) by
A20,
A12,
A17,
A14,
Th14,
A1
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,I0)))))
+ ((
card J)
+ 3)) by
A18,
Th13
.= ((
card I0)
+ ((
card J)
+ 3)) by
A18,
SCMFSA8A:def 4
.= ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36
.= (((
card I)
+ (
card J))
+ 3);
then
A21: (
CurInstr (P3,(
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A3,
A2,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th25;
then
A22: P3
halts_on s3 by
EXTPRO_1: 29;
hence (
if>0 (a,I,J))
is_halting_on (s,P);
now
set J1 = ((((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
let k be
Nat;
assume
A23: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
assume not ((
pseudo-LifeSpan (s00,P00,I0))
+ 1)
<= k;
then
A24: k
<= (
pseudo-LifeSpan (s00,P00,I0)) by
NAT_1: 13;
A25:
0
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 65;
A26: (P3
/. (
IC s3))
= (P3
. (
IC s3)) by
PBOOLE: 143;
(
CurInstr (P3,(
Comput (P3,s3,
0 ))))
= (P3
.
0 ) by
A26,
MEMSTR_0: 16
.= ((
if>0 (a,I,J))
.
0 ) by
A25,
A2,
GRFUNC_1: 2
.= (a
>0_goto ((
card J)
+ 3)) by
Th18;
then
consider k1 be
Nat such that
A27: (k1
+ 1)
= k by
A23,
NAT_1: 6;
reconsider k1 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k1))) as
Element of
NAT ;
k1
< k by
A27,
XREAL_1: 29;
then
A28: k1
< (
pseudo-LifeSpan (s00,P00,I0)) by
A24,
XXREAL_0: 2;
then k1
< (
pseudo-LifeSpan (s,P,I0)) by
A18,
Th13;
then n
in (
dom I0) by
A18,
SCMFSA8A: 17;
then n
< (
card I0) by
AFINSQ_1: 66;
then (n
+ ((
card J)
+ 3))
< ((
card I0)
+ ((
card J)
+ 3)) by
XREAL_1: 6;
then
A29: (n
+ ((
card J)
+ 3))
< ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36;
A30: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s4,k1))) by
A27,
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,k1)))
+ ((
card J)
+ 3)) by
A20,
A12,
A17,
A14,
A28,
Th14,
A1;
(
card J1)
= ((
card (((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
>0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
then (
IC (
Comput (P3,s3,k)))
in (
dom J1) by
A30,
A29,
AFINSQ_1: 66;
then
A31: (
IC (
Comput (P3,s3,k)))
in (
dom (
Directed J1)) by
FUNCT_4: 99;
then
A32: ((
Directed J1)
. (
IC (
Comput (P3,s3,k))))
in (
rng (
Directed J1)) by
FUNCT_1:def 3;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 12
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if>0 (a,I,J))) by
XREAL_1: 29;
then (n
+ ((
card J)
+ 3))
< (
card (
if>0 (a,I,J))) by
A29,
XXREAL_0: 2;
then
A33: (
IC (
Comput (P3,s3,k)))
in (
dom (
if>0 (a,I,J))) by
A30,
AFINSQ_1: 66;
A34: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A33,
A2,
GRFUNC_1: 2;
(
Directed J1)
c= (
if>0 (a,I,J)) by
SCMFSA6A: 16;
then ((
if>0 (a,I,J))
. (
IC (
Comput (P3,s3,k))))
= ((
Directed J1)
. (
IC (
Comput (P3,s3,k)))) by
A31,
GRFUNC_1: 2;
hence contradiction by
A23,
A32,
A34,
COMPOS_1:def 11;
end;
then (
LifeSpan (P3,s3))
= ((
pseudo-LifeSpan (s00,P00,I0))
+ 1) by
A21,
A22,
EXTPRO_1:def 15;
hence thesis by
A18,
A19,
Th13;
end;
theorem ::
SCMFSA8C:40
for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. (
intloc
0 ))
= 1 & (s
. a)
>
0 & (
Directed I)
is_pseudo-closed_on (s,P) holds (
DataPart (
IExec ((
if>0 (a,I,J)),P,s)))
= (
DataPart (
IExec ((I
";" (
Stop
SCM+FSA )),P,s)))
proof
let ss be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set I0 = (
Directed I);
set s = (
Initialized ss);
set I1 = (I
";" (
Stop
SCM+FSA ));
set s00 = (
Initialize s), P00 = (P
+* I0);
set s3 = (
Initialize s), P3 = (P
+* (
if>0 (a,I,J)));
set s4 = (
Comput (P3,s3,1));
set i = (a
>0_goto ((
card J)
+ 3));
A1: I0
c= P00 by
FUNCT_4: 25;
A2: (
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
assume
A3: (ss
. (
intloc
0 ))
= 1;
set s1 = (
Initialize s), P1 = (P
+* I1);
assume (ss
. a)
>
0 ;
then
A4: (s
. a)
>
0 by
SCMFSA_M: 37;
A5: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A6: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A5,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
A7:
0
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 65;
A8: (P3
.
0 )
= ((
if>0 (a,I,J))
.
0 ) by
A7,
FUNCT_4: 13
.= i by
Th18;
A9: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A6,
A8,
PBOOLE: 143;
A10: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A10,
TARSKI:def 1;
then not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
then (s3
. a)
= (s
. a) by
FUNCT_4: 11;
then
A11: (
IC (
Comput (P3,s3,1)))
= ((
card J)
+ 3) by
A4,
A9,
SCMFSA_2: 71;
assume I0
is_pseudo-closed_on (ss,P);
then
A12: I0
is_pseudo-closed_on (s,P) by
A3,
Th16;
then
A13: (
LifeSpan (P1,s1))
= (
pseudo-LifeSpan (s,P,I0)) by
Th21;
A14: I0
is_pseudo-closed_on (s00,P00) by
A12;
A15: for f be
FinSeq-Location holds (s00
. f)
= (s4
. f) by
A9,
SCMFSA_2: 71;
for a be
Int-Location holds (s00
. a)
= (s4
. a) by
A9,
SCMFSA_2: 71;
then
A16: (
DataPart s00)
= (
DataPart s4) by
A15,
SCMFSA_M: 2;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 12
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if>0 (a,I,J))) by
NAT_1: 13;
then
A17: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 66;
A18: (
card ((i
";" J)
";" (
Goto ((
card I)
+ 1))))
= ((
card ((
Macro i)
";" J))
+ (
card (
Goto ((
card I)
+ 1)))) by
SCMFSA6A: 21
.= ((
card ((
Macro i)
";" J))
+ 1) by
SCMFSA8A: 15
.= (((
card (
Macro i))
+ (
card J))
+ 1) by
SCMFSA6A: 21
.= (((
card J)
+ 2)
+ 1) by
COMPOS_1: 56
.= ((
card J)
+ (2
+ 1));
(s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
then
A19: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s3;
A20: (
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
(
if>0 (a,I,J))
= (((i
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I1) by
SCMFSA6A: 25;
then (
Reloc (I1,((
card J)
+ 3)))
c= (
if>0 (a,I,J)) by
A18,
SCMFSA6A: 38;
then
A21: (
Reloc (I1,((
card J)
+ 3)))
c= P3 by
A20,
XBOOLE_1: 1;
(
Reloc (I0,((
card J)
+ 3)))
c= (
Reloc (I1,((
card J)
+ 3))) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A22: (
Reloc (I0,((
card J)
+ 3)))
c= P3 by
A21,
XBOOLE_1: 1;
(
IC (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1))))
= (
IC (
Comput (P3,s4,(
pseudo-LifeSpan (s00,P00,I0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,I0)))))
+ ((
card J)
+ 3)) by
A14,
A22,
A11,
A16,
Th14,
A1
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,I0)))))
+ ((
card J)
+ 3)) by
A12,
Th13
.= ((
card I0)
+ ((
card J)
+ 3)) by
A12,
SCMFSA8A:def 4
.= ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36
.= (((
card I)
+ (
card J))
+ 3);
then
A23: (
CurInstr (P3,(
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,I0))
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A17,
A2,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th25;
then
A24: P3
halts_on s3 by
EXTPRO_1: 29;
now
set J1 = ((((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I);
let k be
Nat;
assume
A25: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
assume not ((
pseudo-LifeSpan (s00,P00,I0))
+ 1)
<= k;
then
A26: k
<= (
pseudo-LifeSpan (s00,P00,I0)) by
NAT_1: 13;
A27:
0
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 65;
A28: (P3
/. (
IC s3))
= (P3
. (
IC s3)) by
PBOOLE: 143;
(
CurInstr (P3,(
Comput (P3,s3,
0 ))))
= (P3
.
0 ) by
A28,
MEMSTR_0: 16
.= ((
if>0 (a,I,J))
.
0 ) by
A27,
A2,
GRFUNC_1: 2
.= (a
>0_goto ((
card J)
+ 3)) by
Th18;
then
consider k1 be
Nat such that
A29: (k1
+ 1)
= k by
A25,
NAT_1: 6;
reconsider k1 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k1))) as
Element of
NAT ;
k1
< k by
A29,
XREAL_1: 29;
then
A30: k1
< (
pseudo-LifeSpan (s00,P00,I0)) by
A26,
XXREAL_0: 2;
then k1
< (
pseudo-LifeSpan (s,P,I0)) by
A12,
Th13;
then n
in (
dom I0) by
A12,
SCMFSA8A: 17;
then n
< (
card I0) by
AFINSQ_1: 66;
then (n
+ ((
card J)
+ 3))
< ((
card I0)
+ ((
card J)
+ 3)) by
XREAL_1: 6;
then
A31: (n
+ ((
card J)
+ 3))
< ((
card I)
+ ((
card J)
+ 3)) by
SCMFSA6A: 36;
A32: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s4,k1))) by
A29,
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,k1)))
+ ((
card J)
+ 3)) by
A14,
A22,
A11,
A16,
A30,
Th14,
A1;
(
card J1)
= ((
card (((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J)
";" (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ (
card (
Goto ((
card I)
+ 1))))
+ (
card I)) by
SCMFSA6A: 21
.= (((
card ((
Macro (a
>0_goto ((
card J)
+ 3)))
";" J))
+ 1)
+ (
card I)) by
SCMFSA8A: 15
.= ((((
card (
Macro (a
>0_goto ((
card J)
+ 3))))
+ (
card J))
+ 1)
+ (
card I)) by
SCMFSA6A: 21
.= (((2
+ (
card J))
+ 1)
+ (
card I)) by
COMPOS_1: 56
.= (((
card I)
+ (
card J))
+ 3);
then (
IC (
Comput (P3,s3,k)))
in (
dom J1) by
A32,
A31,
AFINSQ_1: 66;
then
A33: (
IC (
Comput (P3,s3,k)))
in (
dom (
Directed J1)) by
FUNCT_4: 99;
then
A34: ((
Directed J1)
. (
IC (
Comput (P3,s3,k))))
in (
rng (
Directed J1)) by
FUNCT_1:def 3;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 12
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if>0 (a,I,J))) by
XREAL_1: 29;
then (n
+ ((
card J)
+ 3))
< (
card (
if>0 (a,I,J))) by
A31,
XXREAL_0: 2;
then
A35: (
IC (
Comput (P3,s3,k)))
in (
dom (
if>0 (a,I,J))) by
A32,
AFINSQ_1: 66;
A36: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A35,
A2,
GRFUNC_1: 2;
(
Directed J1)
c= (
if>0 (a,I,J)) by
SCMFSA6A: 16;
then ((
if>0 (a,I,J))
. (
IC (
Comput (P3,s3,k))))
= ((
Directed J1)
. (
IC (
Comput (P3,s3,k)))) by
A33,
GRFUNC_1: 2;
hence contradiction by
A25,
A34,
A36,
COMPOS_1:def 11;
end;
then
A37: (
LifeSpan (P3,s3))
= ((
pseudo-LifeSpan (s00,P00,I0))
+ 1) by
A23,
A24,
EXTPRO_1:def 15;
A38: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
A39: (I0
";" (
Stop
SCM+FSA ))
= I1;
A40: (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,I0)))))
= (
DataPart (
Comput (P1,s1,(
pseudo-LifeSpan (s,P,I0))))) by
A12,
A39,
Th21;
I1
is_halting_on (s,P) by
A12,
Th21;
then
A41: P1
halts_on s1;
thus (
DataPart (
IExec ((
if>0 (a,I,J)),P,ss)))
= (
DataPart (
IExec ((
if>0 (a,I,J)),P,s)))
.= (
DataPart (
Result (P3,s3))) by
A19
.= (
DataPart (
Comput (P3,s3,(
LifeSpan (P3,s3))))) by
A24,
EXTPRO_1: 23
.= (
DataPart (
Comput (P3,s4,(
pseudo-LifeSpan (s00,P00,I0))))) by
A37,
EXTPRO_1: 4
.= (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,I0))))) by
A14,
A22,
A11,
A16,
Th14,
A1
.= (
DataPart (
Comput (P1,s1,(
LifeSpan (P1,s1))))) by
A12,
A13,
A40,
Th13
.= (
DataPart (
Result ((P
+* I1),(s
+* (
Initialize ((
intloc
0 )
.--> 1)))))) by
A38,
A41,
EXTPRO_1: 23
.= (
DataPart (
IExec (I1,P,s)))
.= (
DataPart (
IExec (I1,P,ss)));
end;
theorem ::
SCMFSA8C:41
Th32: for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. a)
<>
0 & (
Directed J)
is_pseudo-closed_on (s,P) holds (
if=0 (a,I,J))
is_halting_on (s,P) & (
LifeSpan ((P
+* (
if=0 (a,I,J))),(
Initialize s)))
= ((
LifeSpan ((P
+* (J
";" (
Stop
SCM+FSA ))),(
Initialize s)))
+ 3)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set J0 = (
Directed J);
set s0 = (
Initialized s);
set J9 = (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))));
set s00 = (
Initialize s), P00 = (P
+* J0);
set s3 = (
Initialize s), P3 = (P
+* (
if=0 (a,I,J)));
set s4 = (
Comput (P3,s3,1));
set s5 = (
Comput (P3,s3,2));
set i = (a
=0_goto ((
card J)
+ 3));
A1: (
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
A2: J0
c= P00 by
FUNCT_4: 25;
(
if=0 (a,I,J))
= ((((
Macro i)
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25;
then (
if=0 (a,I,J))
= (((
Macro i)
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25;
then
A3: (
if=0 (a,I,J))
= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 25;
(
card (
Macro i))
= 2 by
COMPOS_1: 56;
then
A4: (
Reloc (J9,2))
c= (
if=0 (a,I,J)) by
A3,
SCMFSA6A: 38;
A5:
0
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 65;
A6: (P3
.
0 )
= ((
if=0 (a,I,J))
.
0 ) by
A5,
FUNCT_4: 13
.= i by
Th18;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (2
+ 2)) by
SCMFSA8B: 11
.= (((
card J)
+ 2)
+ ((
card I)
+ 2));
then (((
card J)
+ 2)
+
0 )
< (
card (
if=0 (a,I,J))) by
XREAL_1: 8;
then
A7: ((
card J)
+ 2)
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 66;
A8: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A9: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A8,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
set ss = (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,J0))
+ 2))), PP = P3;
(
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
then
A10: (
Reloc (J9,2))
c= P3 by
A4,
XBOOLE_1: 1;
(
Reloc (J0,2))
c= (
Reloc (J9,2)) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A11: (
Reloc (J0,2))
c= P3 by
A10,
XBOOLE_1: 1;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 11
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if=0 (a,I,J))) by
NAT_1: 13;
then
A12: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 66;
assume (s
. a)
<>
0 ;
then
A13: (s0
. a)
<>
0 by
SCMFSA_M: 37;
A14: 1
in (
dom (
if=0 (a,I,J))) by
Th17;
assume
A15: J0
is_pseudo-closed_on (s,P);
then
A16: (
pseudo-LifeSpan (s,P,J0))
= (
LifeSpan ((P
+* (J
";" (
Stop
SCM+FSA ))),(
Initialize s))) by
Th21;
A17: (P3
. 1)
= ((
if=0 (a,I,J))
. 1) by
A14,
FUNCT_4: 13
.= (
goto 2) by
Th18;
A18: J0
is_pseudo-closed_on (s00,P00) by
A15;
A19: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A9,
A6,
PBOOLE: 143;
A20: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A20,
TARSKI:def 1;
then not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
then (s3
. a)
= (s
. a) by
FUNCT_4: 11
.= (s0
. a) by
SCMFSA_M: 37;
then
A21: (
IC s4)
= ((
IC s3)
+ 1) by
A13,
A19,
SCMFSA_2: 70
.= (
0
+ 1) by
A9;
A22: (
Comput (P3,s3,(1
+ 1)))
= (
Following (P3,s4)) by
EXTPRO_1: 3
.= (
Exec ((
goto 2),s4)) by
A21,
A17,
PBOOLE: 143;
then
A23: (
IC s5)
= 2 by
SCMFSA_2: 69;
A24:
now
let f be
FinSeq-Location;
thus (s00
. f)
= (s4
. f) by
A19,
SCMFSA_2: 70
.= (s5
. f) by
A22,
SCMFSA_2: 69;
end;
now
let a be
Int-Location;
thus (s00
. a)
= (s4
. a) by
A19,
SCMFSA_2: 70
.= (s5
. a) by
A22,
SCMFSA_2: 69;
end;
then
A25: (
DataPart s00)
= (
DataPart s5) by
A24,
SCMFSA_M: 2;
(
IC ss)
= (
IC (
Comput (P3,s5,(
pseudo-LifeSpan (s00,P00,J0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,J0)))))
+ 2) by
A18,
A11,
A23,
A25,
Th14,
A2
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0)))))
+ 2) by
A15,
Th13
.= ((
card J0)
+ 2) by
A15,
SCMFSA8A:def 4
.= ((
card J)
+ 2) by
SCMFSA6A: 36;
then
A26: (
CurInstr (P3,ss))
= (P3
. ((
card J)
+ 2)) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. ((
card J)
+ 2)) by
A7,
A1,
GRFUNC_1: 2
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
Th26;
(
IC (
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1))))
= (
IC (
Following (P3,ss))) by
EXTPRO_1: 3
.= (((
card I)
+ (
card J))
+ 3) by
A26,
SCMFSA_2: 69;
then
A27: (
CurInstr (P3,(
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A12,
A1,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th24;
then
A28: P3
halts_on s3 by
EXTPRO_1: 29;
hence (
if=0 (a,I,J))
is_halting_on (s,P);
A29: (
CurInstr (P3,s3))
= i by
A9,
A6,
PBOOLE: 143;
now
A30: (
0
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
XREAL_1: 8;
then
A31: 2
in (
dom (
if=0 (a,I,J))) by
Th19;
A32: (
CurInstr (P3,(
Comput (P3,s3,2))))
= (P3
. 2) by
A23,
PBOOLE: 143
.= ((
if=0 (a,I,J))
. 2) by
A31,
A1,
GRFUNC_1: 2;
let k be
Nat;
assume
A33: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
A34: k
<>
0 by
A33,
A29;
A35: k
<> 1 by
A21,
A33,
A17,
PBOOLE: 143;
k
<> 2 by
A33,
A30,
Th19,
A32;
then k
<>
0 & ... & k
<> 2 by
A34,
A35;
then 2
< k;
then
consider k2 be
Nat such that
A36: (2
+ k2)
= k by
NAT_1: 10;
reconsider k2 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k2))) as
Element of
NAT ;
assume not ((
pseudo-LifeSpan (s00,P00,J0))
+ (1
+ 2))
<= k;
then k
< (((
pseudo-LifeSpan (s00,P00,J0))
+ 1)
+ 2);
then k2
< ((
pseudo-LifeSpan (s00,P00,J0))
+ 1) by
A36,
XREAL_1: 6;
then
A37: k2
<= (
pseudo-LifeSpan (s00,P00,J0)) by
NAT_1: 13;
then
A38: k2
<= (
pseudo-LifeSpan (s,P,J0)) by
A15,
Th13;
A39:
now
per cases by
A38,
XXREAL_0: 1;
suppose
A40: k2
= (
pseudo-LifeSpan (s,P,J0));
(((
card I)
+ (
card J))
+ (2
+ 1))
= ((((
card J)
+ 2)
+ 1)
+ (
card I));
then
A41: (((
card J)
+ 2)
+ 1)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
(
IC (
Comput (P00,s00,k2)))
= (
card J0) by
A15,
A40,
SCMFSA8A:def 4;
then n
= (
card J) by
SCMFSA6A: 36;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A41,
NAT_1: 13;
end;
suppose k2
< (
pseudo-LifeSpan (s,P,J0));
then n
in (
dom J0) by
A15,
SCMFSA8A: 17;
then n
< (
card J0) by
AFINSQ_1: 66;
then (n
+ 2)
< ((
card J0)
+ 2) by
XREAL_1: 6;
then
A42: (n
+ 2)
< ((
card J)
+ 2) by
SCMFSA6A: 36;
(((
card I)
+ (
card J))
+ (1
+ 2))
= (((
card J)
+ 2)
+ ((
card I)
+ 1));
then ((
card J)
+ 2)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A42,
XXREAL_0: 2;
end;
end;
then
A43: (n
+ 2)
in (
dom (
if=0 (a,I,J))) by
Th19;
A44: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s5,k2))) by
A36,
EXTPRO_1: 4
.= (n
+ 2) by
A18,
A11,
A23,
A25,
A37,
Th14,
A2;
(
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A44,
A43,
A1,
GRFUNC_1: 2;
hence contradiction by
A33,
A44,
A39,
Th19;
end;
then (
LifeSpan (P3,s3))
= ((
pseudo-LifeSpan (s00,P00,J0))
+ 3) by
A27,
A28,
EXTPRO_1:def 15;
hence thesis by
A15,
A16,
Th13;
end;
theorem ::
SCMFSA8C:42
for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. (
intloc
0 ))
= 1 & (s
. a)
<>
0 & (
Directed J)
is_pseudo-closed_on (s,P) holds (
DataPart (
IExec ((
if=0 (a,I,J)),P,s)))
= (
DataPart (
IExec ((J
";" (
Stop
SCM+FSA )),P,s)))
proof
let ss be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set J0 = (
Directed J);
set s = (
Initialized ss);
set s0 = (
Initialized s);
set J9 = (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))));
set s00 = (
Initialize s), P00 = (P
+* J0);
set s3 = (
Initialize s), P3 = (P
+* (
if=0 (a,I,J)));
set s4 = (
Comput (P3,s3,1));
set s5 = (
Comput (P3,s3,2));
set i = (a
=0_goto ((
card J)
+ 3));
A1: J0
c= P00 by
FUNCT_4: 25;
A2: (
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
assume
A3: (ss
. (
intloc
0 ))
= 1;
set s1 = (
Initialize s), P1 = (P
+* (J
";" (
Stop
SCM+FSA )));
assume (ss
. a)
<>
0 ;
then
A4: (s0
. a)
<>
0 by
SCMFSA_M: 37;
A5:
0
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 65;
A6: (P3
.
0 )
= ((
if=0 (a,I,J))
.
0 ) by
A5,
FUNCT_4: 13
.= i by
Th18;
(s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
then
A7: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s3;
A8: (J0
";" (
Stop
SCM+FSA ))
= (J
";" (
Stop
SCM+FSA ));
A9: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A10: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A9,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
(
if=0 (a,I,J))
= ((((
Macro i)
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25;
then (
if=0 (a,I,J))
= (((
Macro i)
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25;
then
A11: (
if=0 (a,I,J))
= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 25;
(
card (
Macro i))
= 2 by
COMPOS_1: 56;
then
A12: (
Reloc (J9,2))
c= (
if=0 (a,I,J)) by
A11,
SCMFSA6A: 38;
(
if=0 (a,I,J))
c= P3 by
FUNCT_4: 25;
then
A13: (
Reloc (J9,2))
c= P3 by
A12,
XBOOLE_1: 1;
(
Reloc (J0,2))
c= (
Reloc (J9,2)) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A14: (
Reloc (J0,2))
c= P3 by
A13,
XBOOLE_1: 1;
A15: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A10,
A6,
PBOOLE: 143;
assume J0
is_pseudo-closed_on (ss,P);
then
A16: J0
is_pseudo-closed_on (s,P) by
A3,
Th16;
then (J
";" (
Stop
SCM+FSA ))
is_halting_on (s,P) by
Th21;
then
A17: P1
halts_on s1;
A18: J0
is_pseudo-closed_on (s00,P00) by
A16;
(s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
then
A19: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s1;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (2
+ 2)) by
SCMFSA8B: 11
.= (((
card J)
+ 2)
+ ((
card I)
+ 2));
then (((
card J)
+ 2)
+
0 )
< (
card (
if=0 (a,I,J))) by
XREAL_1: 8;
then
A20: ((
card J)
+ 2)
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 66;
(
card (
if=0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 11
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if=0 (a,I,J))) by
NAT_1: 13;
then
A21: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if=0 (a,I,J))) by
AFINSQ_1: 66;
set s9 = (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,J0))
+ 2)));
(
LifeSpan (P1,s1))
= (
pseudo-LifeSpan (s,P,J0)) by
A16,
Th21;
then
A22: (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0)))))
= (
DataPart (
Comput (P1,s1,(
LifeSpan (P1,s1))))) by
A16,
A8,
Th21;
A23: 1
in (
dom (
if=0 (a,I,J))) by
Th17;
A24: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A24,
TARSKI:def 1;
then not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
then (s3
. a)
= (s0
. a) by
FUNCT_4: 11;
then
A25: (
IC s4)
= ((
IC s3)
+ 1) by
A4,
A15,
SCMFSA_2: 70
.= (
0
+ 1) by
A10;
A26: (P3
. 1)
= ((
if=0 (a,I,J))
. 1) by
A23,
FUNCT_4: 13
.= (
goto 2) by
Th18;
A27: (
Comput (P3,s3,(1
+ 1)))
= (
Following (P3,s4)) by
EXTPRO_1: 3
.= (
Exec ((
goto 2),s4)) by
A25,
A26,
PBOOLE: 143;
then
A28: (
IC s5)
= 2 by
SCMFSA_2: 69;
A29:
now
let f be
FinSeq-Location;
thus (s00
. f)
= (s4
. f) by
A15,
SCMFSA_2: 70
.= (s5
. f) by
A27,
SCMFSA_2: 69;
end;
now
let a be
Int-Location;
thus (s00
. a)
= (s4
. a) by
A15,
SCMFSA_2: 70
.= (s5
. a) by
A27,
SCMFSA_2: 69;
end;
then
A30: (
DataPart s00)
= (
DataPart s5) by
A29,
SCMFSA_M: 2;
A31: (
IC s9)
= (
IC (
Comput (P3,s5,(
pseudo-LifeSpan (s00,P00,J0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,J0)))))
+ 2) by
A18,
A14,
A28,
A30,
Th14,
A1
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0)))))
+ 2) by
A16,
Th13
.= ((
card J0)
+ 2) by
A16,
SCMFSA8A:def 4
.= ((
card J)
+ 2) by
SCMFSA6A: 36;
then
A32: (
CurInstr (P3,s9))
= (P3
. ((
card J)
+ 2)) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. ((
card J)
+ 2)) by
A20,
A2,
GRFUNC_1: 2
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
Th26;
(
IC (
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1))))
= (
IC (
Following (P3,s9))) by
EXTPRO_1: 3
.= (((
card I)
+ (
card J))
+ 3) by
A32,
SCMFSA_2: 69;
then
A33: (
CurInstr (P3,(
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A21,
A2,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th24;
then
A34: P3
halts_on s3 by
EXTPRO_1: 29;
A35: (
CurInstr (P3,s3))
= i by
A10,
A6,
PBOOLE: 143;
now
A36: (
0
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
XREAL_1: 8;
then
A37: 2
in (
dom (
if=0 (a,I,J))) by
Th19;
A38: ((
if=0 (a,I,J))
. 2)
<> (
halt
SCM+FSA ) by
A36,
Th19;
A39: (
CurInstr (P3,(
Comput (P3,s3,2))))
= (P3
. 2) by
A28,
PBOOLE: 143
.= ((
if=0 (a,I,J))
. 2) by
A37,
A2,
GRFUNC_1: 2;
let k be
Nat;
assume
A40: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
A41: k
<>
0 by
A40,
A35;
A42: k
<> 1 by
A25,
A26,
A40,
PBOOLE: 143;
k
<> 2 by
A40,
A38,
A39;
then k
<>
0 & ... & k
<> 2 by
A41,
A42;
then 2
< k;
then
consider k2 be
Nat such that
A43: (2
+ k2)
= k by
NAT_1: 10;
reconsider k2 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k2))) as
Element of
NAT ;
assume not ((
pseudo-LifeSpan (s00,P00,J0))
+ (1
+ 2))
<= k;
then k
< (((
pseudo-LifeSpan (s00,P00,J0))
+ 1)
+ 2);
then k2
< ((
pseudo-LifeSpan (s00,P00,J0))
+ 1) by
A43,
XREAL_1: 6;
then
A44: k2
<= (
pseudo-LifeSpan (s00,P00,J0)) by
NAT_1: 13;
then
A45: k2
<= (
pseudo-LifeSpan (s,P,J0)) by
A16,
Th13;
A46:
now
per cases by
A45,
XXREAL_0: 1;
suppose
A47: k2
= (
pseudo-LifeSpan (s,P,J0));
(((
card I)
+ (
card J))
+ (2
+ 1))
= ((((
card J)
+ 2)
+ 1)
+ (
card I));
then
A48: (((
card J)
+ 2)
+ 1)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
(
IC (
Comput (P00,s00,k2)))
= (
card J0) by
A16,
A47,
SCMFSA8A:def 4;
then n
= (
card J) by
SCMFSA6A: 36;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A48,
NAT_1: 13;
end;
suppose k2
< (
pseudo-LifeSpan (s,P,J0));
then n
in (
dom J0) by
A16,
SCMFSA8A: 17;
then n
< (
card J0) by
AFINSQ_1: 66;
then (n
+ 2)
< ((
card J0)
+ 2) by
XREAL_1: 6;
then
A49: (n
+ 2)
< ((
card J)
+ 2) by
SCMFSA6A: 36;
(((
card I)
+ (
card J))
+ (1
+ 2))
= (((
card J)
+ 2)
+ ((
card I)
+ 1));
then ((
card J)
+ 2)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A49,
XXREAL_0: 2;
end;
end;
then
A50: (n
+ 2)
in (
dom (
if=0 (a,I,J))) by
Th19;
A51: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s5,k2))) by
A43,
EXTPRO_1: 4
.= (n
+ 2) by
A18,
A14,
A28,
A30,
A44,
Th14,
A1;
(
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if=0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A51,
A50,
A2,
GRFUNC_1: 2;
hence contradiction by
A40,
A51,
A46,
Th19;
end;
then
A52: (
LifeSpan (P3,s3))
= (((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1) by
A33,
A34,
EXTPRO_1:def 15;
(
CurInstr (P3,s9))
= (P3
. ((
card J)
+ 2)) by
A31,
PBOOLE: 143
.= ((
if=0 (a,I,J))
. ((
card J)
+ 2)) by
A20,
A2,
GRFUNC_1: 2
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
Th26;
then (
InsCode (
CurInstr (P3,s9)))
= 6 by
SCMFSA_2: 23;
then (
InsCode (
CurInstr (P3,s9)))
in
{
0 , 6, 7, 8} by
ENUMSET1:def 2;
then
A53: (
DataPart s9)
= (
DataPart (
Following (P3,s9))) by
Th6;
A54: (
DataPart s9)
= (
DataPart (
Comput (P3,s5,(
pseudo-LifeSpan (s00,P00,J0))))) by
EXTPRO_1: 4
.= (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,J0))))) by
A18,
A14,
A28,
A30,
Th14,
A1;
thus (
DataPart (
IExec ((
if=0 (a,I,J)),P,ss)))
= (
DataPart (
IExec ((
if=0 (a,I,J)),P,s)))
.= (
DataPart (
Result (P3,s3))) by
A7
.= (
DataPart (
Comput (P3,s3,(
LifeSpan (P3,s3))))) by
A34,
EXTPRO_1: 23
.= (
DataPart (
Following (P3,s9))) by
A52,
EXTPRO_1: 3
.= (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0))))) by
A16,
A54,
A53,
Th13
.= (
DataPart (
Result (P1,s1))) by
A17,
A22,
EXTPRO_1: 23
.= (
DataPart (
IExec ((J
";" (
Stop
SCM+FSA )),P,s))) by
A19
.= (
DataPart (
IExec ((J
";" (
Stop
SCM+FSA )),P,ss)));
end;
theorem ::
SCMFSA8C:43
Th34: for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. a)
<=
0 & (
Directed J)
is_pseudo-closed_on (s,P) holds (
if>0 (a,I,J))
is_halting_on (s,P) & (
LifeSpan ((P
+* (
if>0 (a,I,J))),(s
+* (
Start-At (
0 ,
SCM+FSA )))))
= ((
LifeSpan ((P
+* (J
";" (
Stop
SCM+FSA ))),(
Initialize s)))
+ 3)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set J0 = (
Directed J);
set s0 = (
Initialized s);
set J9 = (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))));
set s00 = (
Initialize s), P00 = (P
+* J0);
set s3 = (
Initialize s), P3 = (P
+* (
if>0 (a,I,J)));
A1: (
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
set s4 = (
Comput (P3,s3,1));
set s5 = (
Comput (P3,s3,2));
set i = (a
>0_goto ((
card J)
+ 3));
A2: J0
c= P00 by
FUNCT_4: 25;
(
if>0 (a,I,J))
= ((((
Macro i)
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25;
then (
if>0 (a,I,J))
= (((
Macro i)
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25;
then
A3: (
if>0 (a,I,J))
= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 25;
(
card (
Macro i))
= 2 by
COMPOS_1: 56;
then
A4: (
Reloc (J9,2))
c= (
if>0 (a,I,J)) by
A3,
SCMFSA6A: 38;
A5:
0
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 65;
A6: (P3
.
0 )
= ((
if>0 (a,I,J))
.
0 ) by
A5,
FUNCT_4: 13
.= i by
Th18;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (2
+ 2)) by
SCMFSA8B: 12
.= (((
card J)
+ 2)
+ ((
card I)
+ 2));
then (((
card J)
+ 2)
+
0 )
< (
card (
if>0 (a,I,J))) by
XREAL_1: 8;
then
A7: ((
card J)
+ 2)
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 66;
A8: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A9: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A8,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
set ss = (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,J0))
+ 2))), PP = P3;
(
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
then
A10: (
Reloc (J9,2))
c= P3 by
A4,
XBOOLE_1: 1;
(
Reloc (J0,2))
c= (
Reloc (J9,2)) by
COMPOS_1: 44,
SCMFSA6A: 16;
then
A11: (
Reloc (J0,2))
c= P3 by
A10,
XBOOLE_1: 1;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 12
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if>0 (a,I,J))) by
NAT_1: 13;
then
A12: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 66;
assume (s
. a)
<=
0 ;
then
A13: (s0
. a)
<=
0 by
SCMFSA_M: 37;
A14: 1
in (
dom (
if>0 (a,I,J))) by
Th17;
assume
A15: J0
is_pseudo-closed_on (s,P);
then
A16: (
pseudo-LifeSpan (s,P,J0))
= (
LifeSpan ((P
+* (J
";" (
Stop
SCM+FSA ))),(
Initialize s))) by
Th21;
A17: (P3
. 1)
= ((
if>0 (a,I,J))
. 1) by
A14,
FUNCT_4: 13
.= (
goto 2) by
Th18;
A18: J0
is_pseudo-closed_on (s00,P00) by
A15;
A19: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A9,
A6,
PBOOLE: 143;
A20: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A20,
TARSKI:def 1;
then not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
then (s3
. a)
= (s
. a) by
FUNCT_4: 11
.= (s0
. a) by
SCMFSA_M: 37;
then
A21: (
IC s4)
= ((
IC s3)
+ 1) by
A13,
A19,
SCMFSA_2: 71
.= (
0
+ 1) by
A9;
A22: (
Comput (P3,s3,(1
+ 1)))
= (
Following (P3,s4)) by
EXTPRO_1: 3
.= (
Exec ((
goto 2),s4)) by
A21,
A17,
PBOOLE: 143;
then
A23: (
IC s5)
= 2 by
SCMFSA_2: 69;
A24:
now
let f be
FinSeq-Location;
thus (s00
. f)
= (s4
. f) by
A19,
SCMFSA_2: 71
.= (s5
. f) by
A22,
SCMFSA_2: 69;
end;
now
let a be
Int-Location;
thus (s00
. a)
= (s4
. a) by
A19,
SCMFSA_2: 71
.= (s5
. a) by
A22,
SCMFSA_2: 69;
end;
then
A25: (
DataPart s00)
= (
DataPart s5) by
A24,
SCMFSA_M: 2;
(
IC ss)
= (
IC (
Comput (P3,s5,(
pseudo-LifeSpan (s00,P00,J0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,J0)))))
+ 2) by
A18,
A11,
A23,
A25,
Th14,
A2
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0)))))
+ 2) by
A15,
Th13
.= ((
card J0)
+ 2) by
A15,
SCMFSA8A:def 4
.= ((
card J)
+ 2) by
SCMFSA6A: 36;
then
A26: (
CurInstr (P3,ss))
= (P3
. ((
card J)
+ 2)) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. ((
card J)
+ 2)) by
A7,
A1,
GRFUNC_1: 2
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
Th27;
(
IC (
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1))))
= (
IC (
Following (P3,ss))) by
EXTPRO_1: 3
.= (((
card I)
+ (
card J))
+ 3) by
A26,
SCMFSA_2: 69;
then
A27: (
CurInstr (P3,(
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A12,
A1,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th25;
then
A28: P3
halts_on s3 by
EXTPRO_1: 29;
hence (
if>0 (a,I,J))
is_halting_on (s,P);
A29: (
CurInstr (P3,s3))
= i by
A9,
A6,
PBOOLE: 143;
now
A30: (
0
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
XREAL_1: 8;
then
A31: 2
in (
dom (
if>0 (a,I,J))) by
Th20;
A32: (
CurInstr (P3,(
Comput (P3,s3,2))))
= (P3
. 2) by
A23,
PBOOLE: 143
.= ((
if>0 (a,I,J))
. 2) by
A31,
A1,
GRFUNC_1: 2;
let k be
Nat;
assume
A33: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
A34: k
<>
0 by
A33,
A29;
A35: k
<> 1 by
A21,
A33,
A17,
PBOOLE: 143;
2
<> k by
A33,
A30,
Th20,
A32;
then k
<>
0 & ... & k
<> 2 by
A34,
A35;
then 2
< k;
then
consider k2 be
Nat such that
A36: (2
+ k2)
= k by
NAT_1: 10;
reconsider k2 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k2))) as
Element of
NAT ;
assume not ((
pseudo-LifeSpan (s00,P00,J0))
+ (1
+ 2))
<= k;
then k
< (((
pseudo-LifeSpan (s00,P00,J0))
+ 1)
+ 2);
then k2
< ((
pseudo-LifeSpan (s00,P00,J0))
+ 1) by
A36,
XREAL_1: 6;
then
A37: k2
<= (
pseudo-LifeSpan (s00,P00,J0)) by
NAT_1: 13;
then
A38: k2
<= (
pseudo-LifeSpan (s,P,J0)) by
A15,
Th13;
A39:
now
per cases by
A38,
XXREAL_0: 1;
suppose
A40: k2
= (
pseudo-LifeSpan (s,P,J0));
(((
card I)
+ (
card J))
+ (2
+ 1))
= ((((
card J)
+ 2)
+ 1)
+ (
card I));
then
A41: (((
card J)
+ 2)
+ 1)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
(
IC (
Comput (P00,s00,k2)))
= (
card J0) by
A15,
A40,
SCMFSA8A:def 4;
then n
= (
card J) by
SCMFSA6A: 36;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A41,
NAT_1: 13;
end;
suppose k2
< (
pseudo-LifeSpan (s,P,J0));
then n
in (
dom J0) by
A15,
SCMFSA8A: 17;
then n
< (
card J0) by
AFINSQ_1: 66;
then (n
+ 2)
< ((
card J0)
+ 2) by
XREAL_1: 6;
then
A42: (n
+ 2)
< ((
card J)
+ 2) by
SCMFSA6A: 36;
(((
card I)
+ (
card J))
+ (1
+ 2))
= (((
card J)
+ 2)
+ ((
card I)
+ 1));
then ((
card J)
+ 2)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A42,
XXREAL_0: 2;
end;
end;
then
A43: (n
+ 2)
in (
dom (
if>0 (a,I,J))) by
Th20;
A44: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s5,k2))) by
A36,
EXTPRO_1: 4
.= (n
+ 2) by
A18,
A11,
A23,
A25,
A37,
Th14,
A2;
(
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A44,
A43,
A1,
GRFUNC_1: 2;
hence contradiction by
A33,
A44,
A39,
Th20;
end;
then (
LifeSpan (P3,s3))
= ((
pseudo-LifeSpan (s00,P00,J0))
+ 3) by
A27,
A28,
EXTPRO_1:def 15;
hence thesis by
A15,
A16,
Th13;
end;
theorem ::
SCMFSA8C:44
for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (s
. (
intloc
0 ))
= 1 & (s
. a)
<=
0 & (
Directed J)
is_pseudo-closed_on (s,P) holds (
DataPart (
IExec ((
if>0 (a,I,J)),P,s)))
= (
DataPart (
IExec ((J
";" (
Stop
SCM+FSA )),P,s)))
proof
let ss be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
set J0 = (
Directed J);
set s = (
Initialized ss);
set s0 = (
Initialized s);
set J9 = (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))));
set s00 = (
Initialize s), P00 = (P
+* J0);
set s3 = (
Initialize s), P3 = (P
+* (
if>0 (a,I,J)));
set s4 = (
Comput (P3,s3,1));
set s5 = (
Comput (P3,s3,2));
set i = (a
>0_goto ((
card J)
+ 3));
A1: (
if>0 (a,I,J))
c= P3 by
FUNCT_4: 25;
A2: J0
c= P00 by
FUNCT_4: 25;
assume
A3: (ss
. (
intloc
0 ))
= 1;
set s1 = (
Initialize s), P1 = (P
+* (J
";" (
Stop
SCM+FSA )));
assume (ss
. a)
<=
0 ;
then
A4: (s0
. a)
<=
0 by
SCMFSA_M: 37;
A5:
0
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 65;
A6: (P3
.
0 )
= ((
if>0 (a,I,J))
.
0 ) by
A5,
FUNCT_4: 13
.= i by
Th18;
(s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
then
A7: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s3;
A8: (J0
";" (
Stop
SCM+FSA ))
= (J
";" (
Stop
SCM+FSA ));
A9: (
IC
SCM+FSA )
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
MEMSTR_0: 15;
A10: (
IC s3)
= (
IC (
Initialize s))
.= (
IC (
Start-At (
0 ,
SCM+FSA ))) by
A9,
FUNCT_4: 13
.=
0 by
FUNCOP_1: 72;
(
if>0 (a,I,J))
= ((((
Macro i)
";" J)
";" (
Goto ((
card I)
+ 1)))
";" (I
";" (
Stop
SCM+FSA ))) by
SCMFSA6A: 25;
then (
if>0 (a,I,J))
= (((
Macro i)
";" J)
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA )))) by
SCMFSA6A: 25;
then
A11: (
if>0 (a,I,J))
= ((
Macro i)
";" (J
";" ((
Goto ((
card I)
+ 1))
";" (I
";" (
Stop
SCM+FSA ))))) by
SCMFSA6A: 25;
(
card (
Macro i))
= 2 by
COMPOS_1: 56;
then
A12: (
Reloc (J9,2))
c= (
if>0 (a,I,J)) by
A11,
SCMFSA6A: 38;
A13: (
Reloc (J0,2))
c= (
Reloc (J9,2)) by
COMPOS_1: 44,
SCMFSA6A: 16;
(
Reloc (J0,2))
c= (
if>0 (a,I,J)) by
A12,
A13,
XBOOLE_1: 1;
then
A14: (
Reloc (J0,2))
c= P3 by
A1,
XBOOLE_1: 1;
A15: (
Comput (P3,s3,(
0
+ 1)))
= (
Following (P3,(
Comput (P3,s3,
0 )))) by
EXTPRO_1: 3
.= (
Following (P3,s3))
.= (
Exec (i,s3)) by
A10,
A6,
PBOOLE: 143;
assume J0
is_pseudo-closed_on (ss,P);
then
A16: J0
is_pseudo-closed_on (s,P) by
A3,
Th16;
then (J
";" (
Stop
SCM+FSA ))
is_halting_on (s,P) by
Th21;
then
A17: P1
halts_on s1;
A18: J0
is_pseudo-closed_on (s00,P00) by
A16;
(s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= (
Initialize (
Initialized s)) by
MEMSTR_0: 44;
then
A19: (s
+* (
Initialize ((
intloc
0 )
.--> 1)))
= s1;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (2
+ 2)) by
SCMFSA8B: 12
.= (((
card J)
+ 2)
+ ((
card I)
+ 2));
then (((
card J)
+ 2)
+
0 )
< (
card (
if>0 (a,I,J))) by
XREAL_1: 8;
then
A20: ((
card J)
+ 2)
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 66;
(
card (
if>0 (a,I,J)))
= (((
card I)
+ (
card J))
+ (3
+ 1)) by
SCMFSA8B: 12
.= ((((
card I)
+ (
card J))
+ 3)
+ 1);
then (((
card I)
+ (
card J))
+ 3)
< (
card (
if>0 (a,I,J))) by
NAT_1: 13;
then
A21: (((
card I)
+ (
card J))
+ 3)
in (
dom (
if>0 (a,I,J))) by
AFINSQ_1: 66;
set s9 = (
Comput (P3,s3,((
pseudo-LifeSpan (s00,P00,J0))
+ 2)));
(
LifeSpan (P1,s1))
= (
pseudo-LifeSpan (s,P,J0)) by
A16,
Th21;
then
A22: (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0)))))
= (
DataPart (
Comput (P1,s1,(
LifeSpan (P1,s1))))) by
A16,
A8,
Th21;
A23: 1
in (
dom (
if>0 (a,I,J))) by
Th17;
A24: a
<> (
IC
SCM+FSA ) by
SCMFSA_2: 56;
not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
A24,
TARSKI:def 1;
then not a
in (
dom (
Start-At (
0 ,
SCM+FSA )));
then (s3
. a)
= (s0
. a) by
FUNCT_4: 11;
then
A25: (
IC s4)
= ((
IC s3)
+ 1) by
A4,
A15,
SCMFSA_2: 71
.= (
0
+ 1) by
A10;
A26: (P3
. 1)
= ((
if>0 (a,I,J))
. 1) by
A23,
FUNCT_4: 13
.= (
goto 2) by
Th18;
A27: (
Comput (P3,s3,(1
+ 1)))
= (
Following (P3,s4)) by
EXTPRO_1: 3
.= (
Exec ((
goto 2),s4)) by
A25,
A26,
PBOOLE: 143;
then
A28: (
IC s5)
= 2 by
SCMFSA_2: 69;
A29:
now
let f be
FinSeq-Location;
thus (s00
. f)
= (s4
. f) by
A15,
SCMFSA_2: 71
.= (s5
. f) by
A27,
SCMFSA_2: 69;
end;
now
let a be
Int-Location;
thus (s00
. a)
= (s4
. a) by
A15,
SCMFSA_2: 71
.= (s5
. a) by
A27,
SCMFSA_2: 69;
end;
then
A30: (
DataPart s00)
= (
DataPart s5) by
A29,
SCMFSA_M: 2;
A31: (
IC s9)
= (
IC (
Comput (P3,s5,(
pseudo-LifeSpan (s00,P00,J0))))) by
EXTPRO_1: 4
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,J0)))))
+ 2) by
A18,
A28,
A30,
Th14,
A2,
A14
.= ((
IC (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0)))))
+ 2) by
A16,
Th13
.= ((
card J0)
+ 2) by
A16,
SCMFSA8A:def 4
.= ((
card J)
+ 2) by
SCMFSA6A: 36;
then
A32: (
CurInstr (P3,s9))
= (P3
. ((
card J)
+ 2)) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. ((
card J)
+ 2)) by
A20,
A1,
GRFUNC_1: 2
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
Th27;
(
IC (
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1))))
= (
IC (
Following (P3,s9))) by
EXTPRO_1: 3
.= (((
card I)
+ (
card J))
+ 3) by
A32,
SCMFSA_2: 69;
then
A33: (
CurInstr (P3,(
Comput (P3,s3,(((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1)))))
= (P3
. (((
card I)
+ (
card J))
+ 3)) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (((
card I)
+ (
card J))
+ 3)) by
A21,
A1,
GRFUNC_1: 2
.= (
halt
SCM+FSA ) by
Th25;
then
A34: P3
halts_on s3 by
EXTPRO_1: 29;
A35: (
CurInstr (P3,s3))
= i by
A10,
A6,
PBOOLE: 143;
now
A36: (
0
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
XREAL_1: 8;
then
A37: 2
in (
dom (
if>0 (a,I,J))) by
Th20;
A38: (
CurInstr (P3,(
Comput (P3,s3,2))))
= (P3
. 2) by
A28,
PBOOLE: 143
.= ((
if>0 (a,I,J))
. 2) by
A37,
A1,
GRFUNC_1: 2;
let k be
Nat;
assume
A39: (
CurInstr (P3,(
Comput (P3,s3,k))))
= (
halt
SCM+FSA );
A40: k
<>
0 by
A39,
A35;
A41: k
<> 1 by
A25,
A26,
A39,
PBOOLE: 143;
2
<> k by
A39,
A36,
Th20,
A38;
then k
<>
0 & ... & k
<> 2 by
A40,
A41;
then 2
< k;
then
consider k2 be
Nat such that
A42: (2
+ k2)
= k by
NAT_1: 10;
reconsider k2 as
Element of
NAT by
ORDINAL1:def 12;
reconsider n = (
IC (
Comput (P00,s00,k2))) as
Element of
NAT ;
assume not ((
pseudo-LifeSpan (s00,P00,J0))
+ (1
+ 2))
<= k;
then k
< (((
pseudo-LifeSpan (s00,P00,J0))
+ 1)
+ 2);
then k2
< ((
pseudo-LifeSpan (s00,P00,J0))
+ 1) by
A42,
XREAL_1: 6;
then
A43: k2
<= (
pseudo-LifeSpan (s00,P00,J0)) by
NAT_1: 13;
then
A44: k2
<= (
pseudo-LifeSpan (s,P,J0)) by
A16,
Th13;
A45:
now
per cases by
A44,
XXREAL_0: 1;
suppose
A46: k2
= (
pseudo-LifeSpan (s,P,J0));
(((
card I)
+ (
card J))
+ (2
+ 1))
= ((((
card J)
+ 2)
+ 1)
+ (
card I));
then
A47: (((
card J)
+ 2)
+ 1)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
(
IC (
Comput (P00,s00,k2)))
= (
card J0) by
A16,
A46,
SCMFSA8A:def 4;
then n
= (
card J) by
SCMFSA6A: 36;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A47,
NAT_1: 13;
end;
suppose k2
< (
pseudo-LifeSpan (s,P,J0));
then n
in (
dom J0) by
A16,
SCMFSA8A: 17;
then n
< (
card J0) by
AFINSQ_1: 66;
then (n
+ 2)
< ((
card J0)
+ 2) by
XREAL_1: 6;
then
A48: (n
+ 2)
< ((
card J)
+ 2) by
SCMFSA6A: 36;
(((
card I)
+ (
card J))
+ (1
+ 2))
= (((
card J)
+ 2)
+ ((
card I)
+ 1));
then ((
card J)
+ 2)
<= (((
card I)
+ (
card J))
+ 3) by
NAT_1: 11;
hence (n
+ 2)
< (((
card I)
+ (
card J))
+ 3) by
A48,
XXREAL_0: 2;
end;
end;
then
A49: (n
+ 2)
in (
dom (
if>0 (a,I,J))) by
Th20;
A50: (
IC (
Comput (P3,s3,k)))
= (
IC (
Comput (P3,s5,k2))) by
A42,
EXTPRO_1: 4
.= (n
+ 2) by
A18,
A28,
A30,
A43,
Th14,
A2,
A14;
(
CurInstr (P3,(
Comput (P3,s3,k))))
= (P3
. (
IC (
Comput (P3,s3,k)))) by
PBOOLE: 143
.= ((
if>0 (a,I,J))
. (
IC (
Comput (P3,s3,k)))) by
A50,
A49,
A1,
GRFUNC_1: 2;
hence contradiction by
A39,
A50,
A45,
Th20;
end;
then
A51: (
LifeSpan (P3,s3))
= (((
pseudo-LifeSpan (s00,P00,J0))
+ 2)
+ 1) by
A33,
A34,
EXTPRO_1:def 15;
(
CurInstr (P3,s9))
= (P3
. ((
card J)
+ 2)) by
A31,
PBOOLE: 143
.= ((
if>0 (a,I,J))
. ((
card J)
+ 2)) by
A20,
A1,
GRFUNC_1: 2
.= (
goto (((
card I)
+ (
card J))
+ 3)) by
Th27;
then (
InsCode (
CurInstr (P3,s9)))
= 6 by
SCMFSA_2: 23;
then (
InsCode (
CurInstr (P3,s9)))
in
{
0 , 6, 7, 8} by
ENUMSET1:def 2;
then
A52: (
DataPart s9)
= (
DataPart (
Following (P3,s9))) by
Th6;
A53: (
DataPart s9)
= (
DataPart (
Comput (P3,s5,(
pseudo-LifeSpan (s00,P00,J0))))) by
EXTPRO_1: 4
.= (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s00,P00,J0))))) by
A18,
A28,
A30,
Th14,
A2,
A14;
thus (
DataPart (
IExec ((
if>0 (a,I,J)),P,ss)))
= (
DataPart (
IExec ((
if>0 (a,I,J)),P,s)))
.= (
DataPart (
Result (P3,s3))) by
A7
.= (
DataPart (
Comput (P3,s3,(
LifeSpan (P3,s3))))) by
A34,
EXTPRO_1: 23
.= (
DataPart (
Following (P3,s9))) by
A51,
EXTPRO_1: 3
.= (
DataPart (
Comput (P00,s00,(
pseudo-LifeSpan (s,P,J0))))) by
A16,
A53,
A52,
Th13
.= (
DataPart (
Result (P1,s1))) by
A17,
A22,
EXTPRO_1: 23
.= (
DataPart (
IExec ((J
";" (
Stop
SCM+FSA )),P,s))) by
A19
.= (
DataPart (
IExec ((J
";" (
Stop
SCM+FSA )),P,ss)));
end;
theorem ::
SCMFSA8C:45
for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (
Directed I)
is_pseudo-closed_on (s,P) & (
Directed J)
is_pseudo-closed_on (s,P) holds (
if=0 (a,I,J))
is_halting_on (s,P)
proof
let s be
State of
SCM+FSA ;
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
assume
A1: (
Directed I)
is_pseudo-closed_on (s,P);
assume
A2: (
Directed J)
is_pseudo-closed_on (s,P);
hereby
per cases ;
suppose
A3: (s
. a)
=
0 ;
thus (
if=0 (a,I,J))
is_halting_on (s,P) by
A1,
A3,
Th28;
end;
suppose
A4: (s
. a)
<>
0 ;
thus (
if=0 (a,I,J))
is_halting_on (s,P) by
A2,
A4,
Th32;
end;
end;
end;
theorem ::
SCMFSA8C:46
for s be
State of
SCM+FSA , I,J be
MacroInstruction of
SCM+FSA , a be
read-write
Int-Location st (
Directed I)
is_pseudo-closed_on (s,P) & (
Directed J)
is_pseudo-closed_on (s,P) holds (
if>0 (a,I,J))
is_halting_on (s,P)
proof
let s be
State of
SCM+FSA ;
let I,J be
MacroInstruction of
SCM+FSA ;
let a be
read-write
Int-Location;
assume
A1: (
Directed I)
is_pseudo-closed_on (s,P);
assume
A2: (
Directed J)
is_pseudo-closed_on (s,P);
hereby
per cases ;
suppose
A3: (s
. a)
>
0 ;
thus (
if>0 (a,I,J))
is_halting_on (s,P) by
A1,
A3,
Th30;
end;
suppose
A4: (s
. a)
<=
0 ;
thus (
if>0 (a,I,J))
is_halting_on (s,P) by
A2,
A4,
Th34;
end;
end;
end;
theorem ::
SCMFSA8C:47
for I be
Program of
SCM+FSA , a be
Int-Location holds not I
destroys a implies not (
Directed I)
destroys a by
SCMFSA8A: 13;
theorem ::
SCMFSA8C:48
Th39: for i be
Instruction of
SCM+FSA , a be
Int-Location holds not i
destroys a implies not (
Macro i)
destroys a
proof
let i be
Instruction of
SCM+FSA ;
let a be
Int-Location;
A1: (
rng (
Macro i))
=
{i, (
halt
SCM+FSA )} by
COMPOS_1: 67;
assume not i
destroys a;
then for ii be
Instruction of
SCM+FSA st ii
in (
rng (
Macro i)) holds not ii
destroys a by
A1,
TARSKI:def 2;
hence thesis;
end;
theorem ::
SCMFSA8C:49
for a be
Int-Location holds not (
halt
SCM+FSA )
refers a;
theorem ::
SCMFSA8C:50
for a,b,c be
Int-Location holds a
<> b implies not (
AddTo (c,b))
refers a
proof
let a,b,c be
Int-Location;
assume
A1: a
<> b;
now
let e be
Int-Location;
let l be
Nat;
let f be
FinSeq-Location;
A2: (
InsCode (
AddTo (c,b)))
= 2 by
SCMFSA_2: 19;
hence (e
:= a)
<> (
AddTo (c,b)) by
SCMFSA_2: 18;
thus (
AddTo (e,a))
<> (
AddTo (c,b)) by
A1,
SF_MASTR: 2;
thus (
SubFrom (e,a))
<> (
AddTo (c,b)) by
A2,
SCMFSA_2: 20;
thus (
MultBy (e,a))
<> (
AddTo (c,b)) by
A2,
SCMFSA_2: 21;
thus (
Divide (a,e))
<> (
AddTo (c,b)) & (
Divide (e,a))
<> (
AddTo (c,b)) by
A2,
SCMFSA_2: 22;
thus (a
=0_goto l)
<> (
AddTo (c,b));
thus (a
>0_goto l)
<> (
AddTo (c,b));
thus (e
:= (f,a))
<> (
AddTo (c,b)) by
A2,
SCMFSA_2: 26;
thus ((f,e)
:= a)
<> (
AddTo (c,b)) & ((f,a)
:= e)
<> (
AddTo (c,b)) by
A2,
SCMFSA_2: 27;
thus (f
:=<0,...,0> a)
<> (
AddTo (c,b)) by
A2,
SCMFSA_2: 29;
end;
hence thesis;
end;
theorem ::
SCMFSA8C:51
for i be
Instruction of
SCM+FSA , a be
Int-Location holds not i
refers a implies not (
Macro i)
refers a
proof
let i be
Instruction of
SCM+FSA ;
let a be
Int-Location;
A1: (
rng (
Macro i))
=
{i, (
halt
SCM+FSA )} by
COMPOS_1: 67;
assume not i
refers a;
then for ii be
Instruction of
SCM+FSA st ii
in (
rng (
Macro i)) holds not ii
refers a by
A1,
TARSKI:def 2;
hence thesis;
end;
theorem ::
SCMFSA8C:52
Th43: for I,J be
Program of
SCM+FSA , a be
Int-Location holds not I
destroys a & not J
destroys a implies not (I
";" J)
destroys a
proof
let I,J be
Program of
SCM+FSA ;
let a be
Int-Location;
assume that
A1: not I
destroys a and
A2: not J
destroys a;
A3: not (
Reloc (J,(
card I)))
destroys a by
A2,
SCMFSA8A: 9;
A4: (I
";" J)
= ((
CutLastLoc (
stop (
Directed I)))
+* (
Reloc (J,((
card (
stop I))
-' 1)))) by
SCMFSA6A: 37
.= ((
Directed I)
+* (
Reloc (J,(
card I)))) by
COMPOS_1: 71;
not (
Directed I)
destroys a by
A1,
SCMFSA8A: 13;
hence thesis by
A3,
A4,
SCMFSA8A: 11;
end;
theorem ::
SCMFSA8C:53
Th44: for J be
Program of
SCM+FSA , i be
Instruction of
SCM+FSA , a be
Int-Location st not i
destroys a & not J
destroys a holds not (i
";" J)
destroys a
proof
let J be
Program of
SCM+FSA ;
let i be
Instruction of
SCM+FSA ;
let a be
Int-Location;
assume that
A1: not i
destroys a and
A2: not J
destroys a;
not (
Macro i)
destroys a by
A1,
Th39;
hence thesis by
A2,
Th43;
end;
theorem ::
SCMFSA8C:54
Th45: for I be
Program of
SCM+FSA , j be
Instruction of
SCM+FSA , a be
Int-Location st not I
destroys a & not j
destroys a holds not (I
";" j)
destroys a
proof
let I be
Program of
SCM+FSA ;
let j be
Instruction of
SCM+FSA ;
let a be
Int-Location;
assume that
A1: not I
destroys a and
A2: not j
destroys a;
not (
Macro j)
destroys a by
A2,
Th39;
hence thesis by
A1,
Th43;
end;
theorem ::
SCMFSA8C:55
for i,j be
Instruction of
SCM+FSA , a be
Int-Location st not i
destroys a & not j
destroys a holds not (i
";" j)
destroys a
proof
let i,j be
Instruction of
SCM+FSA ;
let a be
Int-Location;
assume that
A1: not i
destroys a and
A2: not j
destroys a;
A3: not (
Macro j)
destroys a by
A2,
Th39;
not (
Macro i)
destroys a by
A1,
Th39;
hence thesis by
A3,
Th43;
end;
theorem ::
SCMFSA8C:56
Th47: for a be
Int-Location holds not (
Stop
SCM+FSA )
destroys a
proof
let a be
Int-Location;
now
let i be
Instruction of
SCM+FSA ;
A1: (
rng (
Stop
SCM+FSA ))
=
{(
halt
SCM+FSA )} by
AFINSQ_1: 33;
assume i
in (
rng (
Stop
SCM+FSA ));
then i
= (
halt
SCM+FSA ) by
A1,
TARSKI:def 1;
hence not i
destroys a;
end;
hence thesis;
end;
theorem ::
SCMFSA8C:57
Th48: for a be
Int-Location, l be
Nat holds not (
Goto l)
destroys a
proof
let a be
Int-Location;
let l be
Nat;
now
let i be
Instruction of
SCM+FSA ;
A1: (
rng (
Goto l))
=
{(
goto l)} by
AFINSQ_1: 33;
assume i
in (
rng (
Goto l));
then i
= (
goto l) by
A1,
TARSKI:def 1;
hence not i
destroys a;
end;
hence thesis;
end;
theorem ::
SCMFSA8C:58
Th49: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA st I
is_halting_on ((
Initialized s),P) holds (for a be
read-write
Int-Location holds ((
IExec (I,P,s))
. a)
= ((
Comput ((P
+* I),(
Initialize (
Initialized s)),(
LifeSpan ((P
+* I),(
Initialize (
Initialized s))))))
. a)) & for f be
FinSeq-Location holds ((
IExec (I,P,s))
. f)
= ((
Comput ((P
+* I),(
Initialize (
Initialized s)),(
LifeSpan ((P
+* I),(
Initialize (
Initialized s))))))
. f)
proof
let s be
State of
SCM+FSA ;
let I be
Program of
SCM+FSA ;
set s0 = (
Initialized s);
set s1 = (
Initialize s0), P1 = (P
+* I);
assume I
is_halting_on (s0,P);
then
A1: P1
halts_on s1;
hereby
let a be
read-write
Int-Location;
thus ((
IExec (I,P,s))
. a)
= ((
Result (P1,s1))
. a) by
MEMSTR_0: 44
.= ((
Result (P1,s1))
. a)
.= ((
Comput (P1,s1,(
LifeSpan (P1,s1))))
. a) by
A1,
EXTPRO_1: 23;
end;
let f be
FinSeq-Location;
thus ((
IExec (I,P,s))
. f)
= ((
Result (P1,s1))
. f) by
MEMSTR_0: 44
.= ((
Result (P1,s1))
. f)
.= ((
Comput (P1,s1,(
LifeSpan (P1,s1))))
. f) by
A1,
EXTPRO_1: 23;
end;
theorem ::
SCMFSA8C:59
Th50: for s be
State of
SCM+FSA , I be
parahalting
Program of
SCM+FSA , a be
read-write
Int-Location holds ((
IExec (I,P,s))
. a)
= ((
Comput ((P
+* I),(
Initialize (
Initialized s)),(
LifeSpan ((P
+* I),(
Initialize (
Initialized s))))))
. a)
proof
let s be
State of
SCM+FSA ;
let I be
parahalting
Program of
SCM+FSA ;
let a be
read-write
Int-Location;
I
is_halting_on ((
Initialized s),P) by
SCMFSA7B: 19;
hence thesis by
Th49;
end;
theorem ::
SCMFSA8C:60
Th51: for s be
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA , a be
Int-Location, k be
Element of
NAT st I
is_halting_on ((
Initialized s),P) & not I
destroys a holds ((
IExec (I,P,s))
. a)
= ((
Comput ((P
+* I),(
Initialize (
Initialized s)),k))
. a)
proof
let s be
State of
SCM+FSA ;
let I be
really-closed
Program of
SCM+FSA ;
let a be
Int-Location;
let k be
Element of
NAT ;
set s0 = (
Initialized s);
set s1 = (
Initialize s0), P1 = (P
+* I);
assume I
is_halting_on ((
Initialized s),P);
then
A1: P1
halts_on s1;
assume
A2: not I
destroys a;
thus ((
IExec (I,P,s))
. a)
= ((
Result (P1,s1))
. a) by
MEMSTR_0: 44
.= ((
Result (P1,s1))
. a)
.= ((
Comput (P1,s1,(
LifeSpan (P1,s1))))
. a) by
A1,
EXTPRO_1: 23
.= (s0
. a) by
A2,
SCMFSA7B: 21
.= ((
Comput ((P
+* I),(
Initialize s0),k))
. a) by
A2,
SCMFSA7B: 21;
end;
theorem ::
SCMFSA8C:61
Th52: for s be
State of
SCM+FSA , I be
parahalting
really-closed
Program of
SCM+FSA , a be
Int-Location, k be
Element of
NAT st not I
destroys a holds ((
IExec (I,P,s))
. a)
= ((
Comput ((P
+* I),(
Initialize (
Initialized s)),k))
. a)
proof
let s be
State of
SCM+FSA ;
let I be
parahalting
really-closed
Program of
SCM+FSA ;
let a be
Int-Location;
let k be
Element of
NAT ;
set s0 = (
Initialized s);
set s1 = (
Initialize s0), P1 = (P
+* I);
A1: I
c= P1 by
FUNCT_4: 25;
P1
halts_on s1 by
A1,
SCMFSA6B: 1;
then I
is_halting_on (s0,P);
hence thesis by
Th51;
end;
theorem ::
SCMFSA8C:62
Th53: for s be
State of
SCM+FSA , I be
parahalting
really-closed
Program of
SCM+FSA , a be
Int-Location st not I
destroys a holds ((
IExec (I,P,s))
. a)
= ((
Initialized s)
. a)
proof
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
parahalting
really-closed
Program of
SCM+FSA ;
let a be
Int-Location;
A1: (
DataPart (
Initialized s))
= (
DataPart (
Initialize (
Initialized s))) by
MEMSTR_0: 79;
assume not I
destroys a;
hence ((
IExec (I,P,s))
. a)
= ((
Comput ((P
+* I),(
Initialize (
Initialized s)),
0 ))
. a) by
Th52
.= ((
Initialize (
Initialized s))
. a)
.= ((
Initialized s)
. a) by
A1,
SCMFSA_M: 2;
end;
theorem ::
SCMFSA8C:63
Th54: for s be
State of
SCM+FSA , I be
keeping_0
Program of
SCM+FSA st I
is_halting_on ((
Initialized s),P) holds ((
IExec (I,P,s))
. (
intloc
0 ))
= 1 & for k be
Nat holds ((
Comput ((P
+* I),(
Initialize (
Initialized s)),k))
. (
intloc
0 ))
= 1
proof
set a = (
intloc
0 );
let s be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
keeping_0
Program of
SCM+FSA ;
set s0 = (
Initialized s);
set s1 = (
Initialize s0), P1 = (P
+* I);
A1: I
c= P1 by
FUNCT_4: 25;
A2: (
DataPart s0)
= (
DataPart s1) by
MEMSTR_0: 79;
A3:
now
let k be
Nat;
thus ((
Comput (P1,s1,k))
. a)
= (s1
. a) by
A1,
SCMFSA6B:def 4
.= (s0
. a) by
A2,
SCMFSA_M: 2
.= 1 by
SCMFSA_M: 9;
end;
assume I
is_halting_on (s0,P);
then
A4: P1
halts_on s1;
thus ((
IExec (I,P,s))
. a)
= ((
Result (P1,s1))
. a) by
MEMSTR_0: 44
.= ((
Result (P1,s1))
. a)
.= ((
Comput (P1,s1,(
LifeSpan (P1,s1))))
. a) by
A4,
EXTPRO_1: 23
.= 1 by
A3;
let k be
Nat;
thus thesis by
A3;
end;
theorem ::
SCMFSA8C:64
Th55: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA , a be
Int-Location st not I
destroys a holds for k be
Element of
NAT st (
IC (
Comput ((P
+* I),(
Initialize s),k)))
in (
dom I) holds ((
Comput ((P
+* I),(
Initialize s),(k
+ 1)))
. a)
= ((
Comput ((P
+* I),(
Initialize s),k))
. a)
proof
let s be
State of
SCM+FSA ;
let I be
Program of
SCM+FSA ;
let a be
Int-Location;
assume
A1: not I
destroys a;
set s1 = (
Initialize s), P1 = (P
+* I);
A2: I
c= P1 by
FUNCT_4: 25;
let k be
Element of
NAT ;
assume
A3: (
IC (
Comput ((P
+* I),(
Initialize s),k)))
in (
dom I);
set l = (
IC (
Comput (P1,s1,k)));
(P1
. l)
= (I
. l) by
A3,
A2,
GRFUNC_1: 2;
then (P1
. l)
in (
rng I) by
A3,
FUNCT_1:def 3;
then
A4: not (P1
. l)
destroys a by
A1;
thus ((
Comput (P1,s1,(k
+ 1)))
. a)
= ((
Following (P1,(
Comput (P1,s1,k))))
. a) by
EXTPRO_1: 3
.= ((
Exec ((P1
. l),(
Comput (P1,s1,k))))
. a) by
PBOOLE: 143
.= ((
Comput (P1,s1,k))
. a) by
A4,
SCMFSA7B: 20;
end;
theorem ::
SCMFSA8C:65
Th56: for s be
State of
SCM+FSA , I be
Program of
SCM+FSA , a be
Int-Location st not I
destroys a holds for m be
Nat st (for n be
Nat st n
< m holds (
IC (
Comput ((P
+* I),(
Initialize s),n)))
in (
dom I)) holds for n be
Nat st n
<= m holds ((
Comput ((P
+* I),(
Initialize s),n))
. a)
= (s
. a)
proof
let s be
State of
SCM+FSA ;
let I be
Program of
SCM+FSA ;
let a be
Int-Location;
assume
A1: not I
destroys a;
set s1 = (
Initialize s), P1 = (P
+* I);
let m be
Nat;
defpred
P[
Nat] means $1
<= m implies ((
Comput (P1,s1,$1))
. a)
= (s
. a);
assume
A2: for n be
Nat st n
< m holds (
IC (
Comput ((P
+* I),(
Initialize s),n)))
in (
dom I);
A3: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A4:
P[k];
A5: (k
+
0 )
< (k
+ 1) by
XREAL_1: 6;
assume
A6: (k
+ 1)
<= m;
then k
< m by
A5,
XXREAL_0: 2;
then (
IC (
Comput (P1,s1,k)))
in (
dom I) by
A2;
hence thesis by
A1,
A4,
A6,
A5,
Th55,
XXREAL_0: 2;
end;
let n be
Nat;
assume
A7: n
<= m;
((
Comput (P1,s1,
0 ))
. a)
= (s1
. a)
.= (s
. a) by
SCMFSA_M: 21;
then
A8:
P[
0 ];
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A8,
A3);
hence thesis by
A7;
end;
theorem ::
SCMFSA8C:66
Th57: for s be
State of
SCM+FSA , I be
good
Program of
SCM+FSA holds for m be
Nat st (for n be
Nat st n
< m holds (
IC (
Comput ((P
+* I),(
Initialize s),n)))
in (
dom I)) holds for n be
Nat st n
<= m holds ((
Comput ((P
+* I),(
Initialize s),n))
. (
intloc
0 ))
= (s
. (
intloc
0 )) by
Th56,
SCMFSA7B:def 5;
registration
cluster
good
keeping_0
really-closed
parahalting for
MacroInstruction of
SCM+FSA ;
existence
proof
take (
Stop
SCM+FSA );
thus thesis;
end;
end
theorem ::
SCMFSA8C:67
for s be
State of
SCM+FSA , I be
good
really-closed
Program of
SCM+FSA st I
is_halting_on ((
Initialized s),P) holds ((
IExec (I,P,s))
. (
intloc
0 ))
= 1 & for k be
Nat holds ((
Comput ((P
+* I),(
Initialize (
Initialized s)),k))
. (
intloc
0 ))
= 1
proof
set a = (
intloc
0 );
let s be
State of
SCM+FSA ;
let I be
good
really-closed
Program of
SCM+FSA ;
set s0 = (
Initialized s);
set s1 = (
Initialize s0), P1 = (P
+* I);
defpred
P[
Nat] means for n be
Nat st n
<= $1 holds ((
Comput (P1,s1,n))
. (
intloc
0 ))
= (s0
. (
intloc
0 ));
assume I
is_halting_on (s0,P);
then
A1: P1
halts_on s1;
A2:
P[
0 ]
proof
let n be
Nat;
A3: for i be
Nat st i
<
0 holds (
IC (
Comput (P1,s1,i)))
in (
dom I);
assume n
<=
0 ;
hence thesis by
A3,
Th57;
end;
A4: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
P[k];
let n be
Nat;
assume
A5: n
<= (k
+ 1);
A6: I
c= P1 by
FUNCT_4: 25;
(
IC s1)
=
0 by
MEMSTR_0:def 11;
then (
IC s1)
in (
dom I) by
AFINSQ_1: 65;
then for i be
Nat st i
< (k
+ 1) holds (
IC (
Comput (P1,s1,i)))
in (
dom I) by
AMISTD_1: 21,
A6;
hence thesis by
A5,
Th57;
end;
A7: for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A4);
A8:
now
let k be
Nat;
thus ((
Comput (P1,s1,k))
. (
intloc
0 ))
= (s0
. (
intloc
0 )) by
A7
.= 1 by
SCMFSA_M: 9;
end;
thus ((
IExec (I,P,s))
. a)
= ((
Result (P1,s1))
. a) by
MEMSTR_0: 44
.= ((
Result (P1,s1))
. a)
.= ((
Comput (P1,s1,(
LifeSpan (P1,s1))))
. a) by
A1,
EXTPRO_1: 23
.= 1 by
A8;
thus thesis by
A8;
end;
theorem ::
SCMFSA8C:68
for s be
State of
SCM+FSA , I be
good
really-closed
Program of
SCM+FSA holds for k be
Nat holds ((
Comput ((P
+* I),(
Initialize s),k))
. (
intloc
0 ))
= (s
. (
intloc
0 )) by
SCMFSA7B: 21,
SCMFSA7B:def 5;
theorem ::
SCMFSA8C:69
for P holds for s be
State of
SCM+FSA , I be
keeping_0
parahalting
really-closed
Program of
SCM+FSA , a be
read-write
Int-Location st not I
destroys a holds ((
Comput ((P
+* (I
";" (
SubFrom (a,(
intloc
0 ))))),(
Initialize (
Initialized s)),(
LifeSpan ((P
+* (I
";" (
SubFrom (a,(
intloc
0 ))))),(
Initialize (
Initialized s))))))
. a)
= ((s
. a)
- 1)
proof
let P;
let s be
State of
SCM+FSA ;
let I be
keeping_0
parahalting
really-closed
Program of
SCM+FSA ;
let a be
read-write
Int-Location;
assume
A1: not I
destroys a;
set s0 = (
Initialized s);
set s1 = (
Initialize s0), P1 = (P
+* (I
";" (
SubFrom (a,(
intloc
0 )))));
A2: not a
in (
dom (
Start-At (
0 ,
SCM+FSA ))) by
SCMFSA_2: 102;
((
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),P,s))
. a)
= ((
Exec ((
SubFrom (a,(
intloc
0 ))),(
IExec (I,P,s))))
. a) by
SCMFSA6C: 6
.= (((
IExec (I,P,s))
. a)
- ((
IExec (I,P,s))
. (
intloc
0 ))) by
SCMFSA_2: 65
.= (((
IExec (I,P,s))
. a)
- 1) by
SCMFSA6B: 11
.= (((
Comput ((P
+* I),(
Initialize s0),
0 ))
. a)
- 1) by
A1,
Th52
.= (((
Initialize s0)
. a)
- 1)
.= ((s0
. a)
- 1) by
A2,
FUNCT_4: 11;
hence ((
Comput (P1,s1,(
LifeSpan (P1,s1))))
. a)
= ((s0
. a)
- 1) by
Th50
.= ((s
. a)
- 1) by
SCMFSA_M: 37;
end;
theorem ::
SCMFSA8C:70
for i be
Instruction of
SCM+FSA st not i
destroys (
intloc
0 ) holds (
Macro i) is
good by
Th39;
theorem ::
SCMFSA8C:71
Th62: for s1,s2 be
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st I
is_halting_on (s1,P1) & (
DataPart s1)
= (
DataPart s2) holds for k be
Nat holds (
Comput ((P1
+* I),(
Initialize s1),k))
= (
Comput ((P2
+* I),(
Initialize s2),k)) & (
CurInstr ((P1
+* I),(
Comput ((P1
+* I),(
Initialize s1),k))))
= (
CurInstr ((P2
+* I),(
Comput ((P2
+* I),(
Initialize s2),k))))
proof
let s1,s2 be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
really-closed
Program of
SCM+FSA ;
set ss2 = (
Initialize s2), PP2 = (P2
+* I);
set ss1 = (
Initialize s1), PP1 = (P1
+* I);
A1: I
c= (P1
+* I) by
FUNCT_4: 25;
A2: I
c= (P2
+* I) by
FUNCT_4: 25;
assume I
is_halting_on (s1,P1);
assume
A3: (
DataPart s1)
= (
DataPart s2);
let k be
Nat;
(
IC ss1)
=
0 by
MEMSTR_0:def 11;
then (
IC ss1)
in (
dom I) by
AFINSQ_1: 65;
then
A4: (
IC (
Comput (PP1,ss1,k)))
in (
dom I) by
A1,
AMISTD_1: 21;
(
IC ss2)
=
0 by
MEMSTR_0:def 11;
then
A5: (
IC ss2)
in (
dom I) by
AFINSQ_1: 65;
then
A6: for m be
Nat st m
< k holds (
IC (
Comput (PP2,ss2,m)))
in (
dom I) by
AMISTD_1: 21,
A2;
ss1
= ss2 by
A3,
MEMSTR_0: 80;
hence (
Comput (PP1,ss1,k))
= (
Comput (PP2,ss2,k)) by
A6,
A1,
A2,
AMISTD_2: 10;
then
A7: (
IC (
Comput (PP1,ss1,k)))
= (
IC (
Comput (PP2,ss2,k)));
A8: (
IC (
Comput (PP2,ss2,k)))
in (
dom I) by
AMISTD_1: 21,
A5,
A2;
thus (
CurInstr (PP2,(
Comput (PP2,ss2,k))))
= (PP2
. (
IC (
Comput (PP2,ss2,k)))) by
PBOOLE: 143
.= (I
. (
IC (
Comput (PP2,ss2,k)))) by
A8,
A2,
GRFUNC_1: 2
.= (PP1
. (
IC (
Comput (PP1,ss1,k)))) by
A7,
A4,
A1,
GRFUNC_1: 2
.= (
CurInstr (PP1,(
Comput (PP1,ss1,k)))) by
PBOOLE: 143;
end;
theorem ::
SCMFSA8C:72
Th63: for s1,s2 be
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st I
is_halting_on (s1,P1) & (
DataPart s1)
= (
DataPart s2) holds (
LifeSpan ((P1
+* I),(
Initialize s1)))
= (
LifeSpan ((P2
+* I),(
Initialize s2))) & (
Result ((P1
+* I),(
Initialize s1)))
= (
Result ((P2
+* I),(
Initialize s2)))
proof
let s1,s2 be
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
really-closed
Program of
SCM+FSA ;
set ss2 = (
Initialize s2), PP2 = (P2
+* I);
set ss1 = (
Initialize s1), PP1 = (P1
+* I);
assume
A1: I
is_halting_on (s1,P1);
then
A2: PP1
halts_on ss1;
then
A3: (
Result (PP1,ss1))
= (
Comput (PP1,ss1,(
LifeSpan (PP1,ss1)))) by
EXTPRO_1: 23;
assume
A4: (
DataPart s1)
= (
DataPart s2);
then I
is_halting_on (s2,P2) by
A1,
SCMFSA8B: 5;
then
A5: PP2
halts_on ss2;
A6:
now
let l be
Nat;
assume
A7: (
CurInstr (PP2,(
Comput (PP2,ss2,l))))
= (
halt
SCM+FSA );
(
CurInstr (PP1,(
Comput (PP1,ss1,l))))
= (
CurInstr (PP2,(
Comput (PP2,ss2,l)))) by
A1,
A4,
Th62;
hence (
LifeSpan (PP1,ss1))
<= l by
A2,
A7,
EXTPRO_1:def 15;
end;
(
CurInstr (PP2,(
Comput (PP2,ss2,(
LifeSpan (PP1,ss1))))))
= (
CurInstr (PP1,(
Comput (PP1,ss1,(
LifeSpan (PP1,ss1)))))) by
A1,
A4,
Th62
.= (
halt
SCM+FSA ) by
A2,
EXTPRO_1:def 15;
hence (
LifeSpan (PP1,ss1))
= (
LifeSpan (PP2,ss2)) by
A6,
A5,
EXTPRO_1:def 15;
then (
Result (PP2,ss2))
= (
Comput (PP2,ss2,(
LifeSpan (PP1,ss1)))) by
A5,
EXTPRO_1: 23;
hence thesis by
A1,
A4,
A3,
Th62;
end;
theorem ::
SCMFSA8C:73
for s1,s2 be
0
-started
State of
SCM+FSA , I be
really-closed
Program of
SCM+FSA st I
is_halting_on (s1,P1) & I
c= P1 & I
c= P2 & ex k be
Nat st (
Comput (P1,s1,k))
= s2 holds (
Result (P1,s1))
= (
Result (P2,s2))
proof
let s1,s2 be
0
-started
State of
SCM+FSA ;
set D = (
Data-Locations
SCM+FSA );
let I be
really-closed
Program of
SCM+FSA ;
assume
A1: I
is_halting_on (s1,P1);
A2: (
Start-At (
0 ,
SCM+FSA ))
c= s1 by
MEMSTR_0: 29;
A3: s2
= (
Initialize s2) by
MEMSTR_0: 44;
assume I
c= P1;
then
A4: P1
= (P1
+* I) by
FUNCT_4: 98;
assume I
c= P2;
then
A5: P2
= (P2
+* I) by
FUNCT_4: 98;
s1
= (
Initialize s1) by
A2,
FUNCT_4: 98;
then
A6: P1
halts_on s1 by
A1,
A4;
then
consider n be
Nat such that
A7: (
CurInstr (P1,(
Comput (P1,s1,n))))
= (
halt
SCM+FSA );
given k be
Nat such that
A8: (
Comput (P1,s1,k))
= s2;
set s3 = (
Comput (P1,s1,k)), P3 = P1;
A9: (
IC
SCM+FSA )
in (
dom s3) by
MEMSTR_0: 2;
(
IC s3)
= (
IC s2) by
A8
.= (
IC (
Initialize s2)) by
A3
.=
0 by
FUNCT_4: 113;
then ((
IC
SCM+FSA )
.-->
0 )
c= s3 by
A9,
FUNCOP_1: 73;
then (
Start-At (
0 ,
SCM+FSA ))
c= s3;
then
A10: s3
= (
Initialize s3) by
FUNCT_4: 98;
A11: (
Comput (P1,s1,(n
+ k)))
= (
Comput (P1,(
Comput (P1,s1,k)),n)) by
EXTPRO_1: 4;
A12: (
Comput (P1,s1,(n
+ k)))
= (
Comput (P1,s1,n)) by
A7,
EXTPRO_1: 5,
NAT_1: 11;
P3
halts_on s3 by
A7,
A12,
A11,
EXTPRO_1: 29;
then
A13: I
is_halting_on (s3,P3) by
A10,
A4;
A14: (
DataPart s3)
= (
DataPart s2) by
A8;
consider k be
Nat such that
A15: (
CurInstr (P1,(
Comput (P1,s1,k))))
= (
halt
SCM+FSA ) by
A6;
A16: (P1
. (
IC (
Comput (P1,s1,k))))
= (
halt
SCM+FSA ) by
A15,
PBOOLE: 143;
(
Result (P3,s3))
= (
Result (P2,s2)) by
A3,
A14,
A10,
A13,
Th63,
A4,
A5;
hence thesis by
A16,
EXTPRO_1: 8;
end;
begin
::$Canceled
::$Canceled
begin
definition
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
::
SCMFSA8C:def1
func
Times (a,I) ->
Program of
SCM+FSA equals (
while>0 (a,(I
";" (
SubFrom (a,(
intloc
0 ))))));
correctness ;
end
registration
let a be
Int-Location;
let I be
MacroInstruction of
SCM+FSA ;
cluster (
Times (a,I)) ->
halt-ending
unique-halt;
coherence ;
end
::$Canceled
theorem ::
SCMFSA8C:88
for I,J be
MacroInstruction of
SCM+FSA , a,c be
Int-Location st not I
destroys c & not J
destroys c holds not (
if=0 (a,I,J))
destroys c & not (
if>0 (a,I,J))
destroys c
proof
let I,J be
MacroInstruction of
SCM+FSA ;
let a,c be
Int-Location;
assume
A1: not I
destroys c;
A2: not (
Goto ((
card I)
+ 1))
destroys c by
Th48;
assume
A3: not J
destroys c;
then not ((a
=0_goto ((
card J)
+ 3))
";" J)
destroys c by
Th44,
SCMFSA7B: 12;
then not (((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
destroys c by
A2,
Th43;
then
A4: not ((((a
=0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I)
destroys c by
A1,
Th43;
A5: not (
Goto ((
card I)
+ 1))
destroys c by
Th48;
not ((a
>0_goto ((
card J)
+ 3))
";" J)
destroys c by
A3,
Th44,
SCMFSA7B: 13;
then not (((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
destroys c by
A5,
Th43;
then
A6: not ((((a
>0_goto ((
card J)
+ 3))
";" J)
";" (
Goto ((
card I)
+ 1)))
";" I)
destroys c by
A1,
Th43;
not (
Stop
SCM+FSA )
destroys c by
Th47;
hence not (
if=0 (a,I,J))
destroys c by
A4,
Th43;
not (
Stop
SCM+FSA )
destroys c by
Th47;
hence thesis by
A6,
Th43;
end;
::$Canceled
theorem ::
SCMFSA8C:91
for s be
State of
SCM+FSA , I be
good
parahalting
really-closed
Program of
SCM+FSA , a be
read-write
Int-Location st not I
destroys a holds ((
IExec ((I
";" (
SubFrom (a,(
intloc
0 )))),P,s))
. a)
= ((s
. a)
- 1)
proof
let s be
State of
SCM+FSA ;
let I be
good
parahalting
really-closed
Program of
SCM+FSA ;
let a be
read-write
Int-Location;
set I1 = (I
";" (
SubFrom (a,(
intloc
0 ))));
set ss = (
IExec (I1,P,s));
set s0 = (
Initialized s);
A1: I
is_halting_on (s0,P) by
SCMFSA7B: 19;
assume
A2: not I
destroys a;
thus (ss
. a)
= ((
Exec ((
SubFrom (a,(
intloc
0 ))),(
IExec (I,P,s))))
. a) by
SCMFSA6C: 6
.= (((
IExec (I,P,s))
. a)
- ((
IExec (I,P,s))
. (
intloc
0 ))) by
SCMFSA_2: 65
.= (((
IExec (I,P,s))
. a)
- 1) by
A1,
Th54
.= ((s0
. a)
- 1) by
A2,
Th53
.= ((s
. a)
- 1) by
SCMFSA_M: 37;
end;
begin
reserve aa,bb for
Int-Location;
Lm1: for I,J be
MacroInstruction of
SCM+FSA st not I
destroys aa & not J
destroys aa holds not (I
';' J)
destroys aa
proof
let I,J be
MacroInstruction of
SCM+FSA such that
A1: not I
destroys aa and
A2: not J
destroys aa;
I
<= I;
then (
CutLastLoc I)
c= I;
then
A3: not (
CutLastLoc I)
destroys aa by
A1,
SCMFSA8A: 45;
not (
Reloc (J,((
card I)
-' 1)))
destroys aa by
A2,
SCMFSA8A: 9;
hence thesis by
A3,
SCMFSA8A: 11;
end;
Lm2: for I be
MacroInstruction of
SCM+FSA st not I
destroys aa holds not (I
';' (
goto
0 ))
destroys aa
proof
let I be
MacroInstruction of
SCM+FSA such that
A1: not I
destroys aa;
not (
goto
0 )
destroys aa;
then not (
Macro (
goto
0 ))
destroys aa by
Th39;
then not (I
';' (
Macro (
goto
0 )))
destroys aa by
Lm1,
A1;
hence not (I
';' (
goto
0 ))
destroys aa by
COMPOS_2:def 2;
end;
Lm3: for I be
MacroInstruction of
SCM+FSA holds not I
destroys aa implies not (
if>0 (bb,(I
';' (
goto
0 ))))
destroys aa
proof
let I be
MacroInstruction of
SCM+FSA ;
set i = (bb
>0_goto 3), Mi = (
Macro i);
set IG = (I
';' (
goto
0 ));
A1: not (
Stop
SCM+FSA )
destroys aa by
Th47;
assume not I
destroys aa;
then
A2: not (I
';' (
goto
0 ))
destroys aa by
Lm2;
A3: not (
Goto ((
card IG)
+ 1))
destroys aa by
Th48;
not i
destroys aa;
then not (i
";" (
Goto ((
card IG)
+ 1)))
destroys aa by
A3,
Th44;
then not ((i
";" (
Goto ((
card IG)
+ 1)))
";" IG)
destroys aa by
A2,
Th43;
hence thesis by
A1,
Th43;
end;
theorem ::
SCMFSA8C:92
Th67: for I be
MacroInstruction of
SCM+FSA holds not I
destroys aa implies not (
while>0 (bb,I))
destroys aa
proof
let I be
MacroInstruction of
SCM+FSA ;
set F = (
if>0 (bb,(I
';' (
goto
0 ))));
assume not I
destroys aa;
then
A1: not F
destroys aa by
Lm3;
not (
goto
0 )
destroys aa;
hence thesis by
A1,
SCMFSA8A: 42;
end;
theorem ::
SCMFSA8C:93
for I be
MacroInstruction of
SCM+FSA holds for a,b be
Int-Location st not I
destroys b & a
<> b holds not (
Times (a,I))
destroys b
proof
let I be
MacroInstruction of
SCM+FSA ;
let a,b be
Int-Location;
assume that
A1: not I
destroys b;
assume a
<> b;
then not (
SubFrom (a,(
intloc
0 )))
destroys b by
SCMFSA7B: 8;
then not (I
";" (
SubFrom (a,(
intloc
0 ))))
destroys b by
A1,
Th45;
then not (
while>0 (a,(I
";" (
SubFrom (a,(
intloc
0 ))))))
destroys b by
Th67;
hence thesis;
end;
theorem ::
SCMFSA8C:94
for a be
Int-Location, I be
MacroInstruction of
SCM+FSA holds (
card (
Times (a,I)))
= ((
card I)
+ 7)
proof
let a be
Int-Location, I be
MacroInstruction of
SCM+FSA ;
(
card (I
";" (
SubFrom (a,(
intloc
0 )))))
= ((
card I)
+ 2) by
SCMFSA6A: 34;
hence (
card (
Times (a,I)))
= (((
card I)
+ 2)
+ 5) by
SCMFSA_X: 4
.= ((
card I)
+ 7);
end;
reserve s for
State of
SCM+FSA ,
a for
Int-Location,
I for
Program of
SCM+FSA ,
p for
Instruction-Sequence of
SCM+FSA ;
theorem ::
SCMFSA8C:95
for I be
really-closed
Program of
SCM+FSA st I
is_halting_on ((
Initialized s),p) & not I
destroys a holds ((
IExec (I,p,s))
. a)
= ((
Initialized s)
. a)
proof
let I be
really-closed
Program of
SCM+FSA ;
A1: (
DataPart (
Initialized s))
= (
DataPart (
Initialize (
Initialized s))) by
MEMSTR_0: 79;
assume I
is_halting_on ((
Initialized s),p) & not I
destroys a;
hence ((
IExec (I,p,s))
. a)
= ((
Comput ((p
+* I),(
Initialize (
Initialized s)),
0 ))
. a) by
Th51
.= ((
Initialize (
Initialized s))
. a)
.= ((
Initialized s)
. a) by
A1,
SCMFSA_M: 2;
end;
theorem ::
SCMFSA8C:96
for I,J be
MacroInstruction of
SCM+FSA st not I
destroys aa & not J
destroys aa holds not (I
';' J)
destroys aa by
Lm1;
theorem ::
SCMFSA8C:97
for I be
MacroInstruction of
SCM+FSA st not I
destroys aa holds not (I
';' (
goto
0 ))
destroys aa by
Lm2;
theorem ::
SCMFSA8C:98
for I be
MacroInstruction of
SCM+FSA holds not I
destroys aa implies not (
if>0 (bb,(I
';' (
goto
0 ))))
destroys aa by
Lm3;
theorem ::
SCMFSA8C:99
for I be
MacroInstruction of
SCM+FSA holds not I
destroys aa implies not (
if=0 (bb,(I
';' (
goto
0 ))))
destroys aa
proof
let I be
MacroInstruction of
SCM+FSA ;
set i = (bb
=0_goto 3), Mi = (
Macro i);
set IG = (I
';' (
goto
0 ));
A1: not (
Stop
SCM+FSA )
destroys aa by
Th47;
assume not I
destroys aa;
then
A2: not (I
';' (
goto
0 ))
destroys aa by
Lm2;
A3: not (
Goto ((
card IG)
+ 1))
destroys aa by
Th48;
not i
destroys aa;
then not (i
";" (
Goto ((
card IG)
+ 1)))
destroys aa by
A3,
Th44;
then not ((i
";" (
Goto ((
card IG)
+ 1)))
";" IG)
destroys aa by
A2,
Th43;
hence thesis by
A1,
Th43;
end;