:: 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
theorem Th5: :: SCMFSA6B:5
theorem Th6: :: SCMFSA6B:6
theorem Th7: :: SCMFSA6B:7
theorem Th8: :: SCMFSA6B:8
theorem Th9: :: SCMFSA6B:9
theorem Th10: :: SCMFSA6B:10
theorem :: SCMFSA6B:11
canceled;
theorem Th12: :: SCMFSA6B:12
theorem Th13: :: SCMFSA6B:13
theorem Th14: :: SCMFSA6B:14
:: deftheorem defines IExec SCMFSA6B:def 1 :
:: deftheorem Def2 defines paraclosed SCMFSA6B:def 2 :
:: deftheorem Def3 defines parahalting SCMFSA6B:def 3 :
:: deftheorem Def4 defines keeping_0 SCMFSA6B:def 4 :
Lm2:
Macro (halt SCM+FSA ) is parahalting
theorem :: SCMFSA6B:15
canceled;
theorem :: SCMFSA6B:16
canceled;
theorem :: SCMFSA6B:17
canceled;
theorem Th18: :: SCMFSA6B:18
theorem Th19: :: SCMFSA6B:19
theorem Th20: :: SCMFSA6B:20
theorem Th21: :: SCMFSA6B:21
theorem :: SCMFSA6B:22
theorem :: SCMFSA6B:23
theorem Th24: :: SCMFSA6B:24
theorem :: SCMFSA6B:25
theorem Th26: :: SCMFSA6B:26
theorem Th27: :: SCMFSA6B:27
theorem Th28: :: SCMFSA6B:28
theorem Th29: :: SCMFSA6B:29
theorem Th30: :: SCMFSA6B:30
theorem Th31: :: SCMFSA6B:31
theorem Th32: :: SCMFSA6B:32
theorem Th33: :: SCMFSA6B:33
theorem :: SCMFSA6B:34
Lm3:
( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )
theorem :: SCMFSA6B:35
theorem Th36: :: SCMFSA6B:36
theorem Th37: :: SCMFSA6B:37
theorem Th38: :: SCMFSA6B:38
theorem Th39: :: SCMFSA6B:39
theorem Th40: :: SCMFSA6B:40
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 ) )
theorem Th41: :: SCMFSA6B:41
theorem Th42: :: SCMFSA6B:42
theorem Th43: :: SCMFSA6B:43
theorem :: SCMFSA6B:44