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

proof end;

theorem :: SCMFSA8B:1

for s being State of SCM+FSA holds IC SCM+FSA in dom s

proof end;

theorem Th2: :: SCMFSA8B:2

for s being State of SCM+FSA
for l being Instruction-Location of SCM+FSA holds l in dom s

proof end;

theorem Th3: :: SCMFSA8B:3

for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s holds
insloc 0 in dom I

proof end;

theorem :: SCMFSA8B:4

canceled;

theorem Th5: :: SCMFSA8B:5

for s being State of SCM+FSA
for I being Program of SCM+FSA holds DataPart (Initialize s) = DataPart (s +* (Initialized I))

proof end;

theorem Th6: :: SCMFSA8B:6

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1 holds
I is_closed_on s2

proof end;

theorem Th7: :: SCMFSA8B:7

for s1, s2 being State of SCM+FSA
for I, J being Program of SCM+FSA st DataPart s1 = DataPart s2 holds
s1 +* (I +* (Start-At (insloc 0 ))),s2 +* (J +* (Start-At (insloc 0 ))) equal_outside NAT

proof end;

theorem Th8: :: SCMFSA8B:8

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )

proof end;

theorem Th9: :: SCMFSA8B:9

for s being State of SCM+FSA
for I, J being Program of SCM+FSA holds
( I is_closed_on Initialize s iff I is_closed_on s +* (Initialized J) )

proof end;

theorem Th10: :: SCMFSA8B:10

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA holds
( I is_closed_on s iff I is_closed_on s +* (I +* (Start-At l)) )

proof end;

theorem Th11: :: SCMFSA8B:11

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I +* (Start-At (insloc 0 )) c= s1 & I is_closed_on s1 holds
for n being Element of NAT st ProgramPart (Relocated I,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 Th12: :: SCMFSA8B:12

for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being parahalting Program of SCM+FSA
for a being Int-Location holds (IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a

proof end;

theorem Th13: :: SCMFSA8B:13

for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being parahalting Program of SCM+FSA
for f being FinSeq-Location holds (IExec (i ';' J),s) . f = (IExec J,(Exec i,(Initialize s))) . f

proof end;

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 1
((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );
coherence
((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is Program of SCM+FSA ;
func if>0 a,I,J -> Program of SCM+FSA equals :: SCMFSA8B:def 2
((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );
coherence
((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is Program of SCM+FSA ;

end;

:: deftheorem defines if=0 SCMFSA8B:def 1 :

for a being Int-Location
for I, J being Program of SCM+FSA holds if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );

:: deftheorem defines if>0 SCMFSA8B:def 2 :

for a being Int-Location
for I, J being Program of SCM+FSA holds if>0 a,I,J = ((((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );

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 :

for a being Int-Location
for I, J being Program of SCM+FSA holds if<0 a,I,J = if=0 a,J,(if>0 a,J,I);

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

proof end;

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

proof end;

theorem Th14: :: SCMFSA8B:14

for I, J being Program of SCM+FSA
for a being Int-Location holds card (if=0 a,I,J) = ((card I) + (card J)) + 4

proof end;

theorem Th15: :: SCMFSA8B:15

for I, J being Program of SCM+FSA
for a being Int-Location holds card (if>0 a,I,J) = ((card I) + (card J)) + 4

proof end;

theorem Th16: :: SCMFSA8B:16

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on s & I is_halting_on s holds
( if=0 a,I,J is_closed_on s & if=0 a,I,J is_halting_on s )

proof end;

theorem Th17: :: SCMFSA8B:17

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (if=0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th18: :: SCMFSA8B:18

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <> 0 & J is_closed_on s & J is_halting_on s holds
( if=0 a,I,J is_closed_on s & if=0 a,I,J is_halting_on s )

proof end;

theorem Th19: :: SCMFSA8B:19

for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <> 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if=0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

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

proof end;

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

proof end;

theorem Th22: :: SCMFSA8B:22

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_closed_on s & I is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )

proof end;

theorem Th23: :: SCMFSA8B:23

for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a > 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (if>0 a,I,J),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

theorem Th24: :: SCMFSA8B:24

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 & J is_closed_on s & J is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )

proof end;

theorem Th25: :: SCMFSA8B:25

for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <= 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))

proof end;

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

proof end;

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

proof end;

theorem :: SCMFSA8B:28

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a < 0 & I is_closed_on s & I is_halting_on s holds
( if<0 a,I,J is_closed_on s & if<0 a,I,J is_halting_on s )

proof end;

theorem Th29: :: SCMFSA8B:29

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a < 0 & I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem :: SCMFSA8B:30

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & J is_closed_on s & J is_halting_on s holds
( if<0 a,I,J is_closed_on s & if<0 a,I,J is_halting_on s ) by Th16;

theorem Th31: :: SCMFSA8B:31

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

theorem :: SCMFSA8B:32

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & J is_closed_on s & J is_halting_on s holds
( if<0 a,I,J is_closed_on s & if<0 a,I,J is_halting_on s )

proof end;

theorem Th33: :: SCMFSA8B:33

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))

proof end;

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

proof end;

registration

let I, J be parahalting Program of SCM+FSA ;
let a be read-write Int-Location ;
cluster if=0 a,I,J -> parahalting ;
correctness
coherence
if=0 a,I,J is parahalting;
by Th20;
cluster if>0 a,I,J -> parahalting ;
correctness
coherence
if>0 a,I,J is parahalting;
by Th26;

end;

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 :

for a, b being Int-Location
for I, J being Program of SCM+FSA holds if=0 a,b,I,J = (SubFrom a,b) ';' (if=0 a,I,J);

:: deftheorem defines if>0 SCMFSA8B:def 5 :

for a, b being Int-Location
for I, J being Program of SCM+FSA holds if>0 a,b,I,J = (SubFrom a,b) ';' (if>0 a,I,J);

notation

let a, b be Int-Location ;
let I, J be Program of SCM+FSA ;
synonym if<0 b,a,I,J for if>0 a,b,I,J;

end;

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

for s being State of SCM+FSA
for I being Program of SCM+FSA holds DataPart (Result (s +* (Initialized I))) = DataPart (IExec I,s)

proof end;

theorem Th36: :: SCMFSA8B:36

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location holds Result (s +* (Initialized I)), IExec I,s equal_outside NAT

proof end;

theorem Th37: :: SCMFSA8B:37

for s1, s2 being State of SCM+FSA
for i being Instruction of SCM+FSA
for a being Int-Location st ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & i does_not_refer a & IC s1 = IC s2 holds
( ( for b being Int-Location st a <> b holds
(Exec i,s1) . b = (Exec i,s2) . b ) & ( for f being FinSeq-Location holds (Exec i,s1) . f = (Exec i,s2) . f ) & IC (Exec i,s1) = IC (Exec i,s2) )

proof end;

theorem Th38: :: SCMFSA8B:38

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )

proof end;

theorem Th39: :: SCMFSA8B:39

for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for l being Instruction-Location of SCM+FSA holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on s +* (I +* (Start-At l)) & I is_halting_on s +* (I +* (Start-At l)) ) )

proof end;

theorem Th40: :: SCMFSA8B:40

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 & I is_halting_on s1 holds
( I is_closed_on s2 & I is_halting_on s2 )

proof end;

theorem Th41: :: SCMFSA8B:41

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st ( for d being read-write Int-Location st a <> d holds
s1 . d = s2 . d ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I does_not_refer a & I is_closed_on Initialize s1 & I is_halting_on Initialize s1 holds
( ( for d being Int-Location st a <> d holds
(IExec I,s1) . d = (IExec I,s2) . d ) & ( for f being FinSeq-Location holds (IExec I,s1) . f = (IExec I,s2) . f ) & IC (IExec I,s1) = IC (IExec I,s2) )

proof end;

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

proof end;

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

proof end;