:: On the compositions of macro instructions, Part II
:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996 Association of Mizar Users

begin

theorem :: SCMFSA6B:1

canceled;

theorem :: SCMFSA6B:2

canceled;

theorem :: SCMFSA6B:3

canceled;

theorem :: SCMFSA6B:4

for I being Program of SCM+FSA holds Start-At 0 ,SCM+FSA c= Initialized I by FUNCT_4:26;

theorem Th5: :: SCMFSA6B:5

for n being Element of NAT
for I being Program of SCM+FSA
for s being State of SCM+FSA st I +* (Start-At n,SCM+FSA ) c= s holds
I c= s

proof end;

Lm1: not IC SCM+FSA in NAT
by AMI_1:48;

theorem Th6: :: SCMFSA6B:6

for n being Element of NAT
for I being Program of SCM+FSA holds (I +* (Start-At n,SCM+FSA )) | NAT = I

proof end;

theorem Th7: :: SCMFSA6B:7

for n being Element of NAT
for x being set
for I being Program of SCM+FSA st x in dom I holds
I . x = (I +* (Start-At n,SCM+FSA )) . x

proof end;

theorem Th8: :: SCMFSA6B:8

for I being Program of SCM+FSA
for s being State of SCM+FSA st Initialized I c= s holds
I +* (Start-At 0 ,SCM+FSA ) c= s

proof end;

theorem Th9: :: SCMFSA6B:9

for a being Int-Location
for l being Element of NAT holds not a in dom (Start-At l,SCM+FSA )

proof end;

theorem Th10: :: SCMFSA6B:10

for f being FinSeq-Location
for l being Element of NAT holds not f in dom (Start-At l,SCM+FSA )

proof end;

theorem :: SCMFSA6B:11

canceled;

theorem Th12: :: SCMFSA6B:12

for I being Program of SCM+FSA
for a being Int-Location
for l being Element of NAT holds not a in dom (I +* (Start-At l,SCM+FSA ))

proof end;

theorem Th13: :: SCMFSA6B:13

for I being Program of SCM+FSA
for f being FinSeq-Location
for l being Element of NAT holds not f in dom (I +* (Start-At l,SCM+FSA ))

proof end;

theorem Th14: :: SCMFSA6B:14

for I being Program of SCM+FSA
for s being State of SCM+FSA holds (s +* I) +* (Start-At 0 ,SCM+FSA ) = (s +* (Start-At 0 ,SCM+FSA )) +* I

proof end;

begin

definition

let s be State of SCM+FSA ;
let li be Int-Location ;
let k be Integer;
:: original: +*
redefine func s +* li,k -> State of SCM+FSA ;
coherence
s +* li,k is State of SCM+FSA

proof end;

end;

begin

definition

let I be Program of SCM+FSA ;
let s be State of SCM+FSA ;
func IExec I,s -> State of SCM+FSA equals :: SCMFSA6B:def 1
(Result (s +* (Initialized I))) +* (s | NAT );
coherence
(Result (s +* (Initialized I))) +* (s | NAT ) is State of SCM+FSA ;

end;

:: deftheorem defines IExec SCMFSA6B:def 1 :

for I being Program of SCM+FSA
for s being State of SCM+FSA holds IExec I,s = (Result (s +* (Initialized I))) +* (s | NAT );

definition

let I be Program of SCM+FSA ;
attr I is paraclosed means :Def2: :: SCMFSA6B:def 2
for s being State of SCM+FSA
for n being Element of NAT st I +* (Start-At 0 ,SCM+FSA ) c= s holds
IC (Comput (ProgramPart s),s,n) in dom I;
attr I is parahalting means :Def3: :: SCMFSA6B:def 3
I +* (Start-At 0 ,SCM+FSA ) is halting ;
attr I is keeping_0 means :Def4: :: SCMFSA6B:def 4
for s being State of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s holds
for k being Element of NAT holds (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 );

end;

:: deftheorem Def2 defines paraclosed SCMFSA6B:def 2 :

for I being Program of SCM+FSA holds
( I is paraclosed iff for s being State of SCM+FSA
for n being Element of NAT st I +* (Start-At 0 ,SCM+FSA ) c= s holds
IC (Comput (ProgramPart s),s,n) in dom I );

:: deftheorem Def3 defines parahalting SCMFSA6B:def 3 :

for I being Program of SCM+FSA holds
( I is parahalting iff I +* (Start-At 0 ,SCM+FSA ) is halting );

:: deftheorem Def4 defines keeping_0 SCMFSA6B:def 4 :

for I being Program of SCM+FSA holds
( I is keeping_0 iff for s being State of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s holds
for k being Element of NAT holds (Comput (ProgramPart s),s,k) . (intloc 0 ) = s . (intloc 0 ) );

Lm2: Macro (halt SCM+FSA ) is parahalting

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V61() V101() parahalting set ;
existence
ex b₁ being Program of SCM+FSA st b₁ is parahalting by Lm2;

end;

theorem :: SCMFSA6B:15

canceled;

theorem :: SCMFSA6B:16

canceled;

theorem :: SCMFSA6B:17

canceled;

theorem Th18: :: SCMFSA6B:18

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s holds
ProgramPart s halts_on s

proof end;

theorem Th19: :: SCMFSA6B:19

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA st Initialized I c= s holds
ProgramPart s halts_on s

proof end;

registration

let I be parahalting Program of SCM+FSA ;
cluster Initialized I -> halting ;
coherence
Initialized I is halting

proof end;

end;

theorem Th20: :: SCMFSA6B:20

for s2 being State of SCM+FSA holds not ProgramPart (s2 +* (IC s2),(goto (IC s2))) halts_on s2 +* (IC s2),(goto (IC s2))

proof end;

theorem Th21: :: SCMFSA6B:21

for n being Element of NAT
for I being Program of SCM+FSA
for s1, s2 being State of SCM+FSA st s1,s2 equal_outside NAT & I c= s1 & I c= s2 & ( for m being Element of NAT st m < n holds
IC (Comput (ProgramPart s2),s2,m) in dom I ) holds
for m being Element of NAT st m <= n holds
Comput (ProgramPart s1),s1,m, Comput (ProgramPart s2),s2,m equal_outside NAT

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V101() parahalting -> paraclosed set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is parahalting holds
b₁ is paraclosed

proof end;

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V101() keeping_0 -> paraclosed set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is keeping_0 holds
b₁ is paraclosed

proof end;

end;

theorem :: SCMFSA6B:22

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA
for a being read-write Int-Location st not a in UsedIntLoc I holds
(IExec I,s) . a = s . a

proof end;

theorem :: SCMFSA6B:23

for f being FinSeq-Location
for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA st not f in UsedInt*Loc I holds
(IExec I,s) . f = s . f

proof end;

theorem Th24: :: SCMFSA6B:24

for l being Element of NAT
for s being State of SCM+FSA st IC s = l & s . l = goto l holds
not ProgramPart s halts_on s

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V101() parahalting -> non empty set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is parahalting holds
not b₁ is empty

proof end;

end;

theorem :: SCMFSA6B:25

for I being parahalting Program of SCM+FSA holds dom I <> {} ;

theorem Th26: :: SCMFSA6B:26

for I being parahalting Program of SCM+FSA holds 0 in dom I

proof end;

theorem Th27: :: SCMFSA6B:27

for s1, s2 being State of SCM+FSA
for J being parahalting Program of SCM+FSA st J +* (Start-At 0 ,SCM+FSA ) c= s1 holds
for n being Element of NAT st ProgramPart (Relocated J,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )

proof end;

theorem Th28: :: SCMFSA6B:28

for s1, s2 being State of SCM+FSA
for I being parahalting Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Comput (ProgramPart s1),s1,k, Comput (ProgramPart s2),s2,k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),(Comput (ProgramPart s2),s2,k) )

proof end;

theorem Th29: :: SCMFSA6B:29

for s1, s2 being State of SCM+FSA
for I being parahalting Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside NAT )

proof end;

theorem Th30: :: SCMFSA6B:30

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA holds IC (IExec I,s) = IC (Result (s +* (Initialized I)))

proof end;

theorem Th31: :: SCMFSA6B:31

for I being non empty Program of SCM+FSA holds
( 0 in dom I & 0 in dom (Initialized I) & 0 in dom (I +* (Start-At 0 ,SCM+FSA )) )

proof end;

theorem Th32: :: SCMFSA6B:32

for x being set
for i being Instruction of SCM+FSA holds
( x in dom (Macro i) iff ( x = 0 or x = 1 ) )

proof end;

theorem Th33: :: SCMFSA6B:33

for i being Instruction of SCM+FSA holds
( (Macro i) . 0 = i & (Macro i) . 1 = halt SCM+FSA & (Initialized (Macro i)) . 0 = i & (Initialized (Macro i)) . 1 = halt SCM+FSA & ((Macro i) +* (Start-At 0 ,SCM+FSA )) . 0 = i )

proof end;

theorem :: SCMFSA6B:34

for I being Program of SCM+FSA
for s being State of SCM+FSA st Initialized I c= s holds
IC s = 0

proof end;

Lm3: ( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )

proof end;

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V61() V101() parahalting keeping_0 set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is keeping_0 & b₁ is parahalting ) by Lm3;

end;

theorem :: SCMFSA6B:35

for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA holds (IExec I,s) . (intloc 0 ) = 1

proof end;

begin

registration

cluster Relation-like NAT -defined the carrier of SCM+FSA -defined Function-like the Object-Kind of SCM+FSA -compatible V31() V61() V101() paraclosed set ;
existence
ex b₁ being Program of SCM+FSA st b₁ is paraclosed

proof end;

end;

theorem Th36: :: SCMFSA6B:36

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA
for J being Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s & ProgramPart s halts_on s holds
for m being Element of NAT st m <= LifeSpan s holds
Comput (ProgramPart s),s,m, Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),m equal_outside NAT

proof end;

theorem Th37: :: SCMFSA6B:37

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I & Directed I c= s & Start-At 0 ,SCM+FSA c= s holds
IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I

proof end;

theorem Th38: :: SCMFSA6B:38

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I & Directed I c= s & Start-At 0 ,SCM+FSA c= s holds
DataPart (Comput (ProgramPart s),s,(LifeSpan (s +* I))) = DataPart (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1))

proof end;

theorem Th39: :: SCMFSA6B:39

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan s holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Directed I))),(s +* (Directed I)),k)),(Comput (ProgramPart (s +* (Directed I))),(s +* (Directed I)),k) <> halt SCM+FSA

proof end;

theorem Th40: :: SCMFSA6B:40

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA )) holds
for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k, Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k equal_outside NAT

proof end;

Lm4: for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA
for s being State of SCM+FSA st Initialized (I ';' J) c= s holds
( IC (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = card I & DataPart (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) = DataPart ((Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1) & (Comput (ProgramPart s),s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & ProgramPart s halts_on s & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )

proof end;

registration

let I, J be parahalting Program of SCM+FSA ;
cluster I ';' J -> parahalting ;
coherence
I ';' J is parahalting

proof end;

end;

theorem Th41: :: SCMFSA6B:41

for s being State of SCM+FSA
for I being keeping_0 Program of SCM+FSA st not ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on s +* (I +* (Start-At 0 ,SCM+FSA )) holds
for J being Program of SCM+FSA
for k being Element of NAT holds Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k, Comput (ProgramPart (s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),k equal_outside NAT

proof end;

theorem Th42: :: SCMFSA6B:42

for s being State of SCM+FSA
for I being keeping_0 Program of SCM+FSA st ProgramPart (s +* I) halts_on s +* I holds
for J being paraclosed Program of SCM+FSA st (I ';' J) +* (Start-At 0 ,SCM+FSA ) c= s holds
for k being Element of NAT holds (Comput (ProgramPart ((Result (s +* I)) +* (J +* (Start-At 0 ,SCM+FSA )))),((Result (s +* I)) +* (J +* (Start-At 0 ,SCM+FSA ))),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (s +* I)) +* (J +* (Start-At 0 ,SCM+FSA )))),((Result (s +* I)) +* (J +* (Start-At 0 ,SCM+FSA ))),k)) + (card I)),SCM+FSA ), Comput (ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan (s +* I)) + 1) + k) equal_outside NAT

proof end;

registration

let I, J be keeping_0 Program of SCM+FSA ;
cluster I ';' J -> keeping_0 ;
coherence
I ';' J is keeping_0

proof end;

end;

theorem Th43: :: SCMFSA6B:43

for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds LifeSpan (s +* (Initialized (I ';' J))) = ((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Result (s +* (Initialized I))) +* (Initialized J)))

proof end;

theorem :: SCMFSA6B:44

for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)),SCM+FSA )

proof end;