:: 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 COMPOS_1:3;

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 by COMPOS_1:144;

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 by COMPOS_1:145;

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;

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 ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT);
coherence
(Result ((ProgramPart (s +* (Initialized I))),(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 ((ProgramPart (s +* (Initialized I))),(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 the Instructions of SCM+FSA -valued non empty Function-like the Object-Kind of SCM+FSA -compatible V30() V66() parahalting set ;
existence
ex b₁ being Program of SCM+FSA st b₁ is parahalting by Lm2;

end;

theorem :: SCMFSA6B:14

canceled;

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 the Instructions of SCM+FSA -valued non empty Function-like the Object-Kind of SCM+FSA -compatible V30() V66() 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 the Instructions of SCM+FSA -valued non empty Function-like the Object-Kind of SCM+FSA -compatible V30() V66() 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 the Instructions of SCM+FSA -valued non empty Function-like the Object-Kind of SCM+FSA -compatible V30() V66() parahalting -> set ;
coherence
for b₁ being Program of SCM+FSA st b₁ is parahalting holds
not b₁ is empty

proof end;

end;

theorem :: SCMFSA6B:25

canceled;

theorem :: SCMFSA6B:26

canceled;

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 ((ProgramPart s1),s1) = LifeSpan ((ProgramPart s2),s2) & Result ((ProgramPart s1),s1), Result ((ProgramPart s2),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 ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))

proof end;

theorem :: SCMFSA6B:31

for I being non empty Program of SCM+FSA holds 0 in dom (Initialized I)

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 ) ) by COMPOS_1:147;

theorem :: SCMFSA6B:33

for i being Instruction of SCM+FSA holds
( (Initialized (Macro i)) . 0 = i & (Initialized (Macro i)) . 1 = halt SCM+FSA )

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 the Instructions of SCM+FSA -valued non empty Function-like the Object-Kind of SCM+FSA -compatible V30() V66() 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 the Instructions of SCM+FSA -valued non empty Function-like the Object-Kind of SCM+FSA -compatible V30() V66() 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 ((ProgramPart s),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 ((ProgramPart (s +* I)),(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 ((ProgramPart (s +* I)),(s +* I))))) = DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(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 ((ProgramPart s),s) holds
CurInstr ((ProgramPart (s +* (Directed I))),(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 ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(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 ((ProgramPart (s +* I)),(s +* I))) + 1))) = card I & DataPart (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) = DataPart ((Comput ((ProgramPart (s +* I)),(s +* I),(LifeSpan ((ProgramPart (s +* I)),(s +* I))))) +* (Initialized J)) & ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1)) & (Comput ((ProgramPart s),s,((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1))) . (intloc 0) = 1 & ProgramPart s halts_on s & LifeSpan ((ProgramPart s),s) = ((LifeSpan ((ProgramPart (s +* I)),(s +* I))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result ((ProgramPart s),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 ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k)) +* (Start-At (((IC (Comput ((ProgramPart ((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA))))),((Result ((ProgramPart (s +* I)),(s +* I))) +* (J +* (Start-At (0,SCM+FSA)))),k))) + (card I)),SCM+FSA)), Comput ((ProgramPart (s +* (I ';' J))),(s +* (I ';' J)),(((LifeSpan ((ProgramPart (s +* I)),(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 ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) = ((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(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;