:: 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-2011 Association of Mizar Users

begin

set SA0 = Start-At (0,SCM+FSA);

theorem :: SCMFSA6B:1

canceled;

theorem :: SCMFSA6B:2

canceled;

theorem :: SCMFSA6B:3

canceled;

theorem :: SCMFSA6B:4

for p being PartState of SCM+FSA holds Start-At (0,SCM+FSA) c= Initialized p

proof end;

theorem :: 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 by SCMFSA_2:129;

theorem :: SCMFSA6B:6

canceled;

theorem :: SCMFSA6B:7

canceled;

theorem :: SCMFSA6B:8

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
Start-At (0,SCM+FSA) c= s

proof end;

theorem :: SCMFSA6B:9

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

theorem :: SCMFSA6B:10

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

theorem :: SCMFSA6B:11

canceled;

theorem :: 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))) by SCMFSA_2:132;

theorem :: 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))) by SCMFSA_2:133;

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;
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
func IExec (I,P,s) -> State of SCM+FSA equals :: SCMFSA6B:def 1
(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT);
coherence
(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (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
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds IExec (I,P,s) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I;
attr I is parahalting means :Def3: :: SCMFSA6B:def 3
for s being State of SCM+FSA st Start-At (0,SCM+FSA) c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s;
attr I is keeping_0 means :Def4: :: SCMFSA6B:def 4
for s being State of SCM+FSA st Start-At (0,SCM+FSA) c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for k being Element of NAT holds (Comput (P,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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for n being Element of NAT st Start-At (0,SCM+FSA) c= s holds
IC (Comput (P,s,n)) in dom I );

:: deftheorem Def3 defines parahalting SCMFSA6B:def 3 :
for I being Program of SCM+FSA holds
( I is parahalting iff for s being State of SCM+FSA st Start-At (0,SCM+FSA) c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s );

:: 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 Start-At (0,SCM+FSA) c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for k being Element of NAT holds (Comput (P,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() V144() 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
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P & Start-At (0,SCM+FSA) c= s holds
P 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 Initialize ((intloc 0) .--> 1) c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P 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 :: SCMFSA6B:20

for s2 being State of SCM+FSA
for P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds not P2 +* ((IC s2),(goto (IC s2))) halts_on s2 +* ((IC s2),(goto (IC s2)))

proof end;

Lm45: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds not P +* ((IC s),(goto (IC 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 -> 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:21

canceled;

theorem :: SCMFSA6B:22

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

proof end;

theorem :: SCMFSA6B:23

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

proof end;

theorem :: SCMFSA6B:24

for l being Element of NAT
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st IC s = l & P . l = goto l holds
not P 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 ;

end;

theorem :: SCMFSA6B:25

canceled;

theorem :: SCMFSA6B:26

canceled;

theorem Th27: :: SCMFSA6B:27

for s1, s2 being State of SCM+FSA
for P, Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for J being parahalting Program of SCM+FSA st Start-At (0,SCM+FSA) c= s1 & J c= P holds
for n being Element of NAT st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )

proof end;

theorem Th28: :: SCMFSA6B:28

for s1, s2 being State of SCM+FSA
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting Program of SCM+FSA st I c= P1 & I c= P2 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & NPP s1 = NPP s2 holds
for k being Element of NAT holds
( NPP (Comput (P1,s1,k)) = NPP (Comput (P2,s2,k)) & CurInstr (P1,(Comput (P1,s1,k))) = CurInstr (P2,(Comput (P2,s2,k))) )

proof end;

theorem Th29: :: SCMFSA6B:29

for s1, s2 being State of SCM+FSA
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting Program of SCM+FSA st I c= P1 & I c= P2 & Start-At (0,SCM+FSA) c= s1 & Start-At (0,SCM+FSA) c= s2 & NPP s1 = NPP s2 holds
( LifeSpan (P1,s1) = LifeSpan (P2,s2) & NPP (Result (P1,s1)) = NPP (Result (P2,s2)) )

proof end;

theorem Th30: :: SCMFSA6B:30

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting Program of SCM+FSA holds IC (IExec (I,P,s)) = IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))

proof end;

theorem :: SCMFSA6B:31

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

proof end;

theorem :: SCMFSA6B:32

canceled;

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 s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
IC s = 0

proof end;

Lm3: Macro (halt SCM+FSA) is keeping_0

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() V144() parahalting keeping_0 set ;
existence
ex b₁ being Program of SCM+FSA st
( b₁ is keeping_0 & b₁ is parahalting ) by Lm3, Lm2;

end;

theorem :: SCMFSA6B:35

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA holds (IExec (I,P,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() V144() 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
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P & Start-At (0,SCM+FSA) c= s & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
NPP (Comput (P,s,m)) = NPP (Comput ((P +* (I ';' J)),s,m))

proof end;

theorem Th37: :: SCMFSA6B:37

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

proof end;

theorem Th38: :: SCMFSA6B:38

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

proof end;

LmA: for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
Start-At (0,SCM+FSA) c= s

proof end;

theorem Th39: :: SCMFSA6B:39

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting Program of SCM+FSA st I c= P & Initialize ((intloc 0) .--> 1) c= s holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),s,k))) <> halt SCM+FSA

proof end;

theorem Th40: :: SCMFSA6B:40

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

proof end;

Lm5: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 I ';' J c= P & Initialize ((intloc 0) .--> 1) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) = DataPart ((Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),s)) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (P,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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being keeping_0 Program of SCM+FSA st not P +* I halts_on s +* (Start-At (0,SCM+FSA)) holds
for J being Program of SCM+FSA
for k being Element of NAT holds NPP (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),k))

proof end;

theorem Th42: :: SCMFSA6B:42

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being keeping_0 Program of SCM+FSA st P +* I halts_on s holds
for J being paraclosed Program of SCM+FSA st I ';' J c= P & Start-At (0,SCM+FSA) c= s holds
for k being Element of NAT holds NPP (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I))) = NPP (Comput ((P +* (I ';' J)),(s +* (Start-At (0,SCM+FSA))),(((LifeSpan ((P +* I),(s +* (Start-At (0,SCM+FSA))))) + 1) + k)))

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 P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds LifeSpan ((P +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))

proof end;

theorem :: SCMFSA6B:44

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

proof end;

theorem :: SCMFSA6B:45

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds not P +* ((IC s),(goto (IC s))) halts_on s by Lm45;

theorem :: SCMFSA6B:46

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
Start-At (0,SCM+FSA) c= s by LmA;