:: by Noriko Asamoto

::

:: Received August 27, 1996

:: Copyright (c) 1996-2017 Association of Mizar Users

set A = NAT ;

set D = Data-Locations ;

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

::$CT 4

theorem Th1: :: SCMFSA8B:5

for P1, P2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_halting_on s1,P1 holds

I is_halting_on s2,P2

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_halting_on s1,P1 holds

I is_halting_on s2,P2

proof end;

:: theorem Th5:

:: for s being State of SCM+FSA, I,J being Program of SCM+FSA holds

:: I is_closed_on Initialized s,P iff

:: I is_closed_on s +* Initialize((intloc 0).-->1),P+*J

:: proof

:: let s be State of SCM+FSA;

:: let I,J be Program of SCM+FSA;

:: DataPart Initialized s = DataPart(s +* Initialize((intloc 0).-->1));

:: hence thesis by Th2;

:: end;

:: theorem Th6:

:: for s being State of SCM+FSA, I,J being Program of SCM+FSA, l

:: being Element of NAT holds I is_closed_on s,P iff I is_closed_on

:: s +* (Start-At(0,SCM+FSA)),P+*I

:: proof

:: let s be State of SCM+FSA;

:: let I,J be Program of SCM+FSA;

:: let l be Element of NAT;

:: DataPart s = DataPart(Initialize s) by MEMSTR_0:79;

:: hence thesis by Th2;

:: end;

::$CT 2

:: for s being State of SCM+FSA, I,J being Program of SCM+FSA holds

:: I is_closed_on Initialized s,P iff

:: I is_closed_on s +* Initialize((intloc 0).-->1),P+*J

:: proof

:: let s be State of SCM+FSA;

:: let I,J be Program of SCM+FSA;

:: DataPart Initialized s = DataPart(s +* Initialize((intloc 0).-->1));

:: hence thesis by Th2;

:: end;

:: theorem Th6:

:: for s being State of SCM+FSA, I,J being Program of SCM+FSA, l

:: being Element of NAT holds I is_closed_on s,P iff I is_closed_on

:: s +* (Start-At(0,SCM+FSA)),P+*I

:: proof

:: let s be State of SCM+FSA;

:: let I,J be Program of SCM+FSA;

:: let l be Element of NAT;

:: DataPart s = DataPart(Initialize s) by MEMSTR_0:79;

:: hence thesis by Th2;

:: end;

::$CT 2

theorem Th2: :: SCMFSA8B:8

for P1, P2 being Instruction-Sequence of SCM+FSA

for s1 being 0 -started State of SCM+FSA

for s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA st I c= P1 holds

for n being Nat st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

for s1 being 0 -started State of SCM+FSA

for s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA st I c= P1 holds

for n being Nat st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds

for i being Nat holds

( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;

theorem Th3: :: SCMFSA8B:9

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being keeping_0 sequential Instruction of SCM+FSA

for J being really-closed parahalting Program of SCM+FSA

for a being Int-Location holds (IExec ((i ";" J),P,s)) . a = (IExec (J,P,(Exec (i,(Initialized s))))) . a

for s being State of SCM+FSA

for i being keeping_0 sequential Instruction of SCM+FSA

for J being really-closed parahalting Program of SCM+FSA

for a being Int-Location holds (IExec ((i ";" J),P,s)) . a = (IExec (J,P,(Exec (i,(Initialized s))))) . a

proof end;

theorem Th4: :: SCMFSA8B:10

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being keeping_0 sequential Instruction of SCM+FSA

for J being really-closed parahalting Program of SCM+FSA

for f being FinSeq-Location holds (IExec ((i ";" J),P,s)) . f = (IExec (J,P,(Exec (i,(Initialized s))))) . f

for s being State of SCM+FSA

for i being keeping_0 sequential Instruction of SCM+FSA

for J being really-closed parahalting Program of SCM+FSA

for f being FinSeq-Location holds (IExec ((i ";" J),P,s)) . f = (IExec (J,P,(Exec (i,(Initialized s))))) . f

proof end;

definition

let a be Int-Location;

let I, J be MacroInstruction of SCM+FSA ;

((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of SCM+FSA ;

((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of SCM+FSA ;

end;
let I, J be MacroInstruction of SCM+FSA ;

func if=0 (a,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 1

((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

coherence ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((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 ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

coherence ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of SCM+FSA ;

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

for a being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

for a being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

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

for a being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

for a being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

canceled;

Lm1: for a being Int-Location

for I, J being MacroInstruction of SCM+FSA holds

( 1 in dom (if=0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) )

proof end;

Lm2: for a being Int-Location

for I, J being MacroInstruction of SCM+FSA holds

( (if=0 (a,I,J)) . 0 = a =0_goto ((card J) + 3) & (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )

proof end;

theorem :: SCMFSA8B:11

for I, J being MacroInstruction of SCM+FSA

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

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

proof end;

theorem :: SCMFSA8B:12

for I, J being MacroInstruction of SCM+FSA

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

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

proof end;

theorem Th7: :: SCMFSA8B:13

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_on s,P holds

if=0 (a,I,J) is_halting_on s,P

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_on s,P holds

if=0 (a,I,J) is_halting_on s,P

proof end;

theorem Th8: :: SCMFSA8B:14

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_on Initialized s,P holds

IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_on Initialized s,P holds

IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

Lm3: for I, J being really-closed MacroInstruction of SCM+FSA holds ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is really-closed

proof end;

registration

let I, J be really-closed MacroInstruction of SCM+FSA ;

let a be Int-Location;

coherence

if=0 (a,I,J) is really-closed

if>0 (a,I,J) is really-closed

end;
let a be Int-Location;

coherence

if=0 (a,I,J) is really-closed

proof end;

coherence if>0 (a,I,J) is really-closed

proof end;

theorem Th9: :: SCMFSA8B:15

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <> 0 & J is_halting_on s,P holds

if=0 (a,I,J) is_halting_on s,P

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <> 0 & J is_halting_on s,P holds

if=0 (a,I,J) is_halting_on s,P

proof end;

theorem Th10: :: SCMFSA8B:16

for P being Instruction-Sequence of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <> 0 & J is_halting_on Initialized s,P holds

IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <> 0 & J is_halting_on Initialized s,P holds

IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th11: :: SCMFSA8B:17

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction 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)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction 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)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

proof end;

theorem Th12: :: SCMFSA8B:18

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if=0 (a,I,J)),P,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if=0 (a,I,J)),P,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

proof end;

theorem Th13: :: SCMFSA8B:19

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & I is_halting_on s,P holds

if>0 (a,I,J) is_halting_on s,P

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & I is_halting_on s,P holds

if>0 (a,I,J) is_halting_on s,P

proof end;

theorem Th14: :: SCMFSA8B:20

for P being Instruction-Sequence of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a > 0 & I is_halting_on Initialized s,P holds

IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a > 0 & I is_halting_on Initialized s,P holds

IExec ((if>0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th15: :: SCMFSA8B:21

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 & J is_halting_on s,P holds

if>0 (a,I,J) is_halting_on s,P

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 & J is_halting_on s,P holds

if>0 (a,I,J) is_halting_on s,P

proof end;

theorem Th16: :: SCMFSA8B:22

for P being Instruction-Sequence of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <= 0 & J is_halting_on Initialized s,P holds

IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <= 0 & J is_halting_on Initialized s,P holds

IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th17: :: SCMFSA8B:23

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction 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)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction 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)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

proof end;

theorem Th18: :: SCMFSA8B:24

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if>0 (a,I,J)),P,s)) = ((card I) + (card J)) + 3 & ( s . a > 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <= 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if>0 (a,I,J)),P,s)) = ((card I) + (card J)) + 3 & ( s . a > 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <= 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

proof end;

::$CT 7

registration

let I, J be really-closed parahalting MacroInstruction of SCM+FSA ;

let a be read-write Int-Location;

correctness

coherence

if=0 (a,I,J) is parahalting ;

by Th11;

correctness

coherence

if>0 (a,I,J) is parahalting ;

by Th17;

end;
let a be read-write Int-Location;

correctness

coherence

if=0 (a,I,J) is parahalting ;

by Th11;

correctness

coherence

if>0 (a,I,J) is parahalting ;

by Th17;

definition

let a, b be Int-Location;

let I, J be MacroInstruction of SCM+FSA ;

(SubFrom (a,b)) ";" (if=0 (a,I,J)) is Program of SCM+FSA ;

(SubFrom (a,b)) ";" (if>0 (a,I,J)) is Program of SCM+FSA ;

end;
let I, J be MacroInstruction of SCM+FSA ;

func if=0 (a,b,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 3

(SubFrom (a,b)) ";" (if=0 (a,I,J));

coherence (SubFrom (a,b)) ";" (if=0 (a,I,J));

(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 4

(SubFrom (a,b)) ";" (if>0 (a,I,J));

coherence (SubFrom (a,b)) ";" (if>0 (a,I,J));

(SubFrom (a,b)) ";" (if>0 (a,I,J)) is Program of SCM+FSA ;

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

for a, b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if=0 (a,b,I,J) = (SubFrom (a,b)) ";" (if=0 (a,I,J));

for a, b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if=0 (a,b,I,J) = (SubFrom (a,b)) ";" (if=0 (a,I,J));

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

for a, b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if>0 (a,b,I,J) = (SubFrom (a,b)) ";" (if>0 (a,I,J));

for a, b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds if>0 (a,b,I,J) = (SubFrom (a,b)) ";" (if>0 (a,I,J));

registration

let a be Int-Location;

let I, J be MacroInstruction of SCM+FSA ;

coherence

( if=0 (a,I,J) is halt-ending & if=0 (a,I,J) is unique-halt ) ;

coherence

( if>0 (a,I,J) is halt-ending & if>0 (a,I,J) is unique-halt ) ;

end;
let I, J be MacroInstruction of SCM+FSA ;

coherence

( if=0 (a,I,J) is halt-ending & if=0 (a,I,J) is unique-halt ) ;

coherence

( if>0 (a,I,J) is halt-ending & if>0 (a,I,J) is unique-halt ) ;

registration

let a, b be Int-Location;

let I, J be really-closed MacroInstruction of SCM+FSA ;

coherence

if=0 (a,b,I,J) is really-closed ;

coherence

if>0 (a,b,I,J) is really-closed ;

end;
let I, J be really-closed MacroInstruction of SCM+FSA ;

coherence

if=0 (a,b,I,J) is really-closed ;

coherence

if>0 (a,b,I,J) is really-closed ;

registration

let a, b be Int-Location;

let I, J be MacroInstruction of SCM+FSA ;

coherence

( if=0 (a,b,I,J) is halt-ending & if=0 (a,b,I,J) is unique-halt ) ;

coherence

( if>0 (a,b,I,J) is halt-ending & if>0 (a,b,I,J) is unique-halt ) ;

end;
let I, J be MacroInstruction of SCM+FSA ;

coherence

( if=0 (a,b,I,J) is halt-ending & if=0 (a,b,I,J) is unique-halt ) ;

coherence

( if>0 (a,b,I,J) is halt-ending & if>0 (a,b,I,J) is unique-halt ) ;

registration

let I, J be really-closed parahalting MacroInstruction of SCM+FSA ;

let a, b be read-write Int-Location;

correctness

coherence

if=0 (a,b,I,J) is parahalting ;

;

correctness

coherence

if>0 (a,b,I,J) is parahalting ;

;

end;
let a, b be read-write Int-Location;

correctness

coherence

if=0 (a,b,I,J) is parahalting ;

;

correctness

coherence

if>0 (a,b,I,J) is parahalting ;

;

registration

let I, J be really-closed MacroInstruction of SCM+FSA ;

let a, b be read-write Int-Location;

correctness

coherence

if=0 (a,b,I,J) is really-closed ;

;

correctness

coherence

if>0 (a,b,I,J) is really-closed ;

;

end;
let a, b be read-write Int-Location;

correctness

coherence

if=0 (a,b,I,J) is really-closed ;

;

correctness

coherence

if>0 (a,b,I,J) is really-closed ;

;

theorem :: SCMFSA8B:32

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA holds DataPart (Result ((P +* I),(Initialized s))) = DataPart (IExec (I,P,s)) by SCMFSA6B:def 1;

for s being State of SCM+FSA

for I being Program of SCM+FSA holds DataPart (Result ((P +* I),(Initialized s))) = DataPart (IExec (I,P,s)) by SCMFSA6B:def 1;

theorem Th20: :: SCMFSA8B:33

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA holds Result ((P +* I),(Initialized s)) = IExec (I,P,s) by SCMFSA6B:def 1;

for s being State of SCM+FSA

for I being Program of SCM+FSA holds Result ((P +* I),(Initialized s)) = IExec (I,P,s) by SCMFSA6B:def 1;

theorem Th21: :: SCMFSA8B:34

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 ) & not i refers 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)) )

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 ) & not i refers 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 Th22: :: SCMFSA8B:35

for P1, P2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location st not I refers a & ( for b being Int-Location st a <> b holds

s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds

for k being Nat holds

( ( for b being Int-Location st a <> b holds

(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location st not I refers a & ( for b being Int-Location st a <> b holds

s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds

for k being Nat holds

( ( for b being Int-Location st a <> b holds

(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for f being FinSeq-Location holds (Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) & IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k))) )

proof end;

theorem :: SCMFSA8B:36

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for l being Nat holds

( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )

for s being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for l being Nat holds

( I is_halting_on s,P iff I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I )

proof end;

theorem Th24: :: SCMFSA8B:37

for P1, P2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location st not I refers 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_halting_on s1,P1 holds

I is_halting_on s2,P2

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location st not I refers 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_halting_on s1,P1 holds

I is_halting_on s2,P2

proof end;

theorem Th25: :: SCMFSA8B:38

for P1, P2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for I being really-closed 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 ) & not I refers a & I is_halting_on Initialized s1,P1 holds

( ( for d being Int-Location st a <> d holds

(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )

for s1, s2 being State of SCM+FSA

for I being really-closed 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 ) & not I refers a & I is_halting_on Initialized s1,P1 holds

( ( for d being Int-Location st a <> d holds

(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for f being FinSeq-Location holds (IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) & IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )

proof end;

theorem :: SCMFSA8B:39

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a, b being read-write Int-Location st not I refers a & not J refers a holds

( IC (IExec ((if=0 (a,b,I,J)),P,s)) = ((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)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <> s . b implies ( ( for d being Int-Location st a <> d holds

(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a, b being read-write Int-Location st not I refers a & not J refers a holds

( IC (IExec ((if=0 (a,b,I,J)),P,s)) = ((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)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <> s . b implies ( ( for d being Int-Location st a <> d holds

(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

proof end;

theorem :: SCMFSA8B:40

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a, b being read-write Int-Location st not I refers a & not J refers a holds

( IC (IExec ((if>0 (a,b,I,J)),P,s)) = ((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)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds

(IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

for s being State of SCM+FSA

for I, J being really-closed parahalting MacroInstruction of SCM+FSA

for a, b being read-write Int-Location st not I refers a & not J refers a holds

( IC (IExec ((if>0 (a,b,I,J)),P,s)) = ((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)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds

(IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )

proof end;

:: theorem

:: s.intloc 0 = 1 implies (I is_closed_on s,p iff I is_closed_on

:: Initialized s,p)

:: proof

:: assume s.intloc 0 = 1;

:: then DataPart Initialized s = DataPart s by SCMFSA_M:19;

:: hence thesis by Th2;

:: end;

::$CT

:: s.intloc 0 = 1 implies (I is_closed_on s,p iff I is_closed_on

:: Initialized s,p)

:: proof

:: assume s.intloc 0 = 1;

:: then DataPart Initialized s = DataPart s by SCMFSA_M:19;

:: hence thesis by Th2;

:: end;

::$CT

theorem :: SCMFSA8B:42

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st s . (intloc 0) = 1 holds

( I is_halting_on s,p iff I is_halting_on Initialized s,p )

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st s . (intloc 0) = 1 holds

( I is_halting_on s,p iff I is_halting_on Initialized s,p )

proof end;