:: 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

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 (insloc 0 ) 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 (insloc n)) c= s holds
I c= s

proof end;

Lm1: now

assume IC SCM+FSA in NAT ; :: thesis: contradiction
then reconsider l = IC SCM+FSA as Instruction-Location of SCM+FSA by AMI_1:def 4;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

theorem Th6: :: SCMFSA6B:6

for n being Element of NAT
for I being Program of SCM+FSA holds (I +* (Start-At (insloc n))) | 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 (insloc n))) . 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 (insloc 0 )) c= s

proof end;

theorem Th9: :: SCMFSA6B:9

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

proof end;

theorem Th10: :: SCMFSA6B:10

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

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 Instruction-Location of SCM+FSA holds not a in dom (I +* (Start-At l))

proof end;

theorem Th13: :: SCMFSA6B:13

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

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 (insloc 0 )) = (s +* (Start-At (insloc 0 ))) +* I

proof end;

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;

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 by CARD_3:96;

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 (insloc 0 )) c= s holds
IC (Computation s,n) in dom I;
attr I is parahalting means :Def3: :: SCMFSA6B:def 3
I +* (Start-At (insloc 0 )) is halting;
attr I is keeping_0 means :Def4: :: SCMFSA6B:def 4
for s being State of SCM+FSA st I +* (Start-At (insloc 0 )) c= s holds
for k being Element of NAT holds (Computation 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 (insloc 0 )) c= s holds
IC (Computation 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 (insloc 0 )) 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 (insloc 0 )) c= s holds
for k being Element of NAT holds (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) );

Lm2: Macro (halt SCM+FSA ) is parahalting

proof end;

registration

cluster parahalting Element of K243(the Object-Kind of SCM+FSA );
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 (insloc 0 )) c= s holds
s is halting

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
s is halting

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 s2 +* (IC s2),(goto (IC s2)) is halting

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 (Computation s2,m) in dom I ) holds
for m being Element of NAT st m <= n holds
Computation s1,m, Computation s2,m equal_outside NAT

proof end;

registration

cluster parahalting -> paraclosed Element of K243(the Object-Kind of SCM+FSA );
coherence
for b₁ being Program of SCM+FSA st b₁ is parahalting holds
b₁ is paraclosed

proof end;

cluster keeping_0 -> paraclosed Element of K243(the Object-Kind of SCM+FSA );
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 Instruction-Location of SCM+FSA
for s being State of SCM+FSA st IC s = l & s . l = goto l holds
not s is halting

proof end;

registration

cluster parahalting -> non empty Element of K243(the Object-Kind of SCM+FSA );
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 insloc 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 (insloc 0 )) c= s1 holds
for n being Element of NAT st ProgramPart (Relocated J,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation 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 (insloc 0 )) c= s1 & I +* (Start-At (insloc 0 )) c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Computation s1,k, Computation s2,k equal_outside NAT & CurInstr (Computation s1,k) = CurInstr (Computation 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 (insloc 0 )) c= s1 & I +* (Start-At (insloc 0 )) 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
( insloc 0 in dom I & insloc 0 in dom (Initialized I) & insloc 0 in dom (I +* (Start-At (insloc 0 ))) )

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 = insloc 0 or x = insloc 1 ) )

proof end;

theorem Th33: :: SCMFSA6B:33

for i being Instruction of SCM+FSA holds
( (Macro i) . (insloc 0 ) = i & (Macro i) . (insloc 1) = halt SCM+FSA & (Initialized (Macro i)) . (insloc 0 ) = i & (Initialized (Macro i)) . (insloc 1) = halt SCM+FSA & ((Macro i) +* (Start-At (insloc 0 ))) . (insloc 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 = insloc 0

proof end;

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

proof end;

registration

cluster parahalting keeping_0 Element of K243(the Object-Kind of SCM+FSA );
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;

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 (insloc 0 )) c= s & s is halting holds
for m being Element of NAT st m <= LifeSpan s holds
Computation s,m, Computation (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 s +* I is halting & Directed I c= s & Start-At (insloc 0 ) c= s holds
IC (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I)

proof end;

theorem Th38: :: SCMFSA6B:38

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st s +* I is halting & Directed I c= s & Start-At (insloc 0 ) c= s holds
DataPart (Computation s,(LifeSpan (s +* I))) = DataPart (Computation 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 (Computation (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 s +* (I +* (Start-At (insloc 0 ))) is halting holds
for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),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 (Computation s,((LifeSpan (s +* I)) + 1)) = insloc (card I) & DataPart (Computation s,((LifeSpan (s +* I)) + 1)) = DataPart ((Computation (s +* I),(LifeSpan (s +* I))) +* (Initialized J)) & ProgramPart (Relocated J,(card I)) c= Computation s,((LifeSpan (s +* I)) + 1) & (Computation s,((LifeSpan (s +* I)) + 1)) . (intloc 0 ) = 1 & s is halting & LifeSpan s = ((LifeSpan (s +* I)) + 1) + (LifeSpan ((Result (s +* I)) +* (Initialized J))) & ( J is keeping_0 implies (Result s) . (intloc 0 ) = 1 ) )

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 s +* (I +* (Start-At (insloc 0 ))) is halting holds
for J being Program of SCM+FSA
for k being Element of NAT holds Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),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 s +* I is halting holds
for J being paraclosed Program of SCM+FSA st (I ';' J) +* (Start-At (insloc 0 )) c= s holds
for k being Element of NAT holds (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k) +* (Start-At ((IC (Computation ((Result (s +* I)) +* (J +* (Start-At (insloc 0 )))),k)) + (card I))), Computation (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)))

proof end;