:: Conditional branch macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996 Association of Mizar Users
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
Lm1:
for I, J being Program of SCM+FSA holds ProgramPart (Relocated J,(card I)) c= I ';' J
theorem :: SCMFSA8B:1
theorem Th2: :: SCMFSA8B:2
theorem Th3: :: SCMFSA8B:3
theorem :: SCMFSA8B:4
canceled;
theorem Th5: :: SCMFSA8B:5
theorem Th6: :: SCMFSA8B:6
theorem Th7: :: SCMFSA8B:7
theorem Th8: :: SCMFSA8B:8
theorem Th9: :: SCMFSA8B:9
theorem Th10: :: SCMFSA8B:10
theorem Th11: :: SCMFSA8B:11
theorem Th12: :: SCMFSA8B:12
theorem Th13: :: SCMFSA8B:13
:: deftheorem defines if=0 SCMFSA8B:def 1 :
:: deftheorem defines if>0 SCMFSA8B:def 2 :
definition
let a be
Int-Location ;
let I,
J be
Program of
SCM+FSA ;
func if<0 a,
I,
J -> Program of
SCM+FSA equals :: SCMFSA8B:def 3
if=0 a,
J,
(if>0 a,J,I);
coherence
if=0 a,J,(if>0 a,J,I) is Program of SCM+FSA
;
end;
:: deftheorem defines if<0 SCMFSA8B:def 3 :
Lm2:
for a being Int-Location
for I, J being Program of SCM+FSA holds
( insloc 0 in dom (if=0 a,I,J) & insloc 1 in dom (if=0 a,I,J) & insloc 0 in dom (if>0 a,I,J) & insloc 1 in dom (if>0 a,I,J) )
Lm3:
for a being Int-Location
for I, J being Program of SCM+FSA holds
( (if=0 a,I,J) . (insloc 0 ) = a =0_goto (insloc ((card J) + 3)) & (if=0 a,I,J) . (insloc 1) = goto (insloc 2) & (if>0 a,I,J) . (insloc 0 ) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )
theorem Th14: :: SCMFSA8B:14
theorem Th15: :: SCMFSA8B:15
theorem Th16: :: SCMFSA8B:16
theorem Th17: :: SCMFSA8B:17
theorem Th18: :: SCMFSA8B:18
theorem Th19: :: SCMFSA8B:19
theorem Th20: :: SCMFSA8B:20
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if=0 a,
I,
J is
parahalting & (
s . a = 0 implies
IExec (if=0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & (
s . a <> 0 implies
IExec (if=0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem Th21: :: SCMFSA8B:21
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if=0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & (
s . a = 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <> 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem Th22: :: SCMFSA8B:22
theorem Th23: :: SCMFSA8B:23
theorem Th24: :: SCMFSA8B:24
theorem Th25: :: SCMFSA8B:25
theorem Th26: :: SCMFSA8B:26
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if>0 a,
I,
J is
parahalting & (
s . a > 0 implies
IExec (if>0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & (
s . a <= 0 implies
IExec (if>0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem Th27: :: SCMFSA8B:27
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if>0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & (
s . a > 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <= 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem :: SCMFSA8B:28
theorem Th29: :: SCMFSA8B:29
theorem :: SCMFSA8B:30
theorem Th31: :: SCMFSA8B:31
theorem :: SCMFSA8B:32
theorem Th33: :: SCMFSA8B:33
theorem :: SCMFSA8B:34
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if<0 a,
I,
J is
parahalting & (
s . a < 0 implies
IExec (if<0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) & (
s . a >= 0 implies
IExec (if<0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) )
definition
let a,
b be
Int-Location ;
let I,
J be
Program of
SCM+FSA ;
func if=0 a,
b,
I,
J -> Program of
SCM+FSA equals :: SCMFSA8B:def 4
(SubFrom a,b) ';' (if=0 a,I,J);
coherence
(SubFrom a,b) ';' (if=0 a,I,J) is Program of SCM+FSA
;
func if>0 a,
b,
I,
J -> Program of
SCM+FSA equals :: SCMFSA8B:def 5
(SubFrom a,b) ';' (if>0 a,I,J);
coherence
(SubFrom a,b) ';' (if>0 a,I,J) is Program of SCM+FSA
;
end;
:: deftheorem defines if=0 SCMFSA8B:def 4 :
:: deftheorem defines if>0 SCMFSA8B:def 5 :
registration
let I,
J be
parahalting Program of
SCM+FSA ;
let a,
b be
read-write Int-Location ;
cluster if=0 a,
b,
I,
J -> parahalting ;
correctness
coherence
if=0 a,b,I,J is parahalting;
;
cluster if>0 a,
b,
I,
J -> parahalting ;
correctness
coherence
if>0 a,b,I,J is parahalting;
;
end;
theorem Th35: :: SCMFSA8B:35
theorem Th36: :: SCMFSA8B:36
theorem Th37: :: SCMFSA8B:37
theorem Th38: :: SCMFSA8B:38
theorem Th39: :: SCMFSA8B:39
theorem Th40: :: SCMFSA8B:40
theorem Th41: :: SCMFSA8B:41
theorem :: SCMFSA8B:42
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a,
b being
read-write Int-Location st
I does_not_refer a &
J does_not_refer a holds
(
IC (IExec (if=0 a,b,I,J),s) = insloc (((card I) + (card J)) + 5) & (
s . a = s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if=0 a,b,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <> s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if=0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem :: SCMFSA8B:43
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a,
b being
read-write Int-Location st
I does_not_refer a &
J does_not_refer a holds
(
IC (IExec (if>0 a,b,I,J),s) = insloc (((card I) + (card J)) + 5) & (
s . a > s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <= s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )