:: by Noriko Asamoto

::

:: Received October 29, 1997

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

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

set Q = (intloc 0) .--> 1;

theorem :: SCMFSA8C:1

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds

for k being Nat st ( for n being Nat st n <= k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds

k < pseudo-LifeSpan (s,P,I)

for s being State of SCM+FSA

for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds

for k being Nat st ( for n being Nat st n <= k holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds

k < pseudo-LifeSpan (s,P,I)

proof end;

theorem Th2: :: SCMFSA8C:2

for I, J being Program of SCM+FSA

for k being Nat st card I <= k & k < (card I) + (card J) holds

for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds

(I ";" J) . k = IncAddr (i,(card I))

for k being Nat st card I <= k & k < (card I) + (card J) holds

for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds

(I ";" J) . k = IncAddr (i,(card I))

proof end;

theorem :: SCMFSA8C:3

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA holds IExec (I,P,s) = IExec (I,P,(Initialized s)) ;

for s being State of SCM+FSA

for I being Program of SCM+FSA holds IExec (I,P,s) = IExec (I,P,(Initialized s)) ;

::$CT

theorem Th4: :: SCMFSA8C:5

for I being Program of SCM+FSA st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds

Initialize ((intloc 0) .--> 1) is I -halted

for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds

Initialize ((intloc 0) .--> 1) is I -halted

proof end;

theorem :: SCMFSA8C:6

for I being Program of SCM+FSA st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds

Initialize ((intloc 0) .--> 1) is I -halted by Th4;

for P being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,P ) holds

Initialize ((intloc 0) .--> 1) is I -halted by Th4;

::$CT 5

theorem Th6: :: SCMFSA8C:12

for s being State of SCM+FSA

for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds

DataPart (Exec (i,s)) = DataPart s

for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds

DataPart (Exec (i,s)) = DataPart s

proof end;

::$CT

theorem :: SCMFSA8C:14

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialized s

for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialized s

proof end;

::$CT

theorem Th8: :: SCMFSA8C:16

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 Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 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 Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 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 Th9: :: SCMFSA8C:17

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

for s1, s2 being 0 -started State of SCM+FSA

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

for i being Nat holds

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

for s1, s2 being 0 -started State of SCM+FSA

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

for i being Nat holds

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

proof end;

theorem Th10: :: SCMFSA8C:18

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

for s1, s2 being 0 -started State of SCM+FSA

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

LifeSpan (P1,s1) = LifeSpan (P2,s2)

for s1, s2 being 0 -started State of SCM+FSA

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

LifeSpan (P1,s1) = LifeSpan (P2,s2)

proof end;

theorem :: SCMFSA8C:19

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 s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds

DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds

DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

proof end;

theorem :: SCMFSA8C:20

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 s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

for s1, s2 being State of SCM+FSA

for I being really-closed Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

proof end;

theorem Th13: :: SCMFSA8C:21

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds

( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) )

for s being State of SCM+FSA

for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds

( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) )

proof end;

theorem Th14: :: SCMFSA8C:22

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 Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds

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

( ( for i being Nat st i < pseudo-LifeSpan (s1,P1,I) holds

IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Nat st i <= pseudo-LifeSpan (s1,P1,I) holds

( (IC (Comput (P1,s1,i))) + n = IC (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 Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds

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

( ( for i being Nat st i < pseudo-LifeSpan (s1,P1,I) holds

IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Nat st i <= pseudo-LifeSpan (s1,P1,I) holds

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

proof end;

theorem Th15: :: SCMFSA8C:23

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

for s1, s2 being State of SCM+FSA

for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds

I is_pseudo-closed_on s2,P2

for s1, s2 being State of SCM+FSA

for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds

I is_pseudo-closed_on s2,P2

proof end;

theorem Th16: :: SCMFSA8C:24

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )

for s being State of SCM+FSA

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

( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )

proof end;

theorem Th17: :: SCMFSA8C:25

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

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;

theorem Th18: :: SCMFSA8C:26

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 )

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 Th19: :: SCMFSA8C:27

for a being Int-Location

for I, J being MacroInstruction of SCM+FSA

for n being Element of NAT st n < ((card I) + (card J)) + 3 holds

( n in dom (if=0 (a,I,J)) & (if=0 (a,I,J)) . n <> halt SCM+FSA )

for I, J being MacroInstruction of SCM+FSA

for n being Element of NAT st n < ((card I) + (card J)) + 3 holds

( n in dom (if=0 (a,I,J)) & (if=0 (a,I,J)) . n <> halt SCM+FSA )

proof end;

theorem Th20: :: SCMFSA8C:28

for a being Int-Location

for I, J being MacroInstruction of SCM+FSA

for n being Element of NAT st n < ((card I) + (card J)) + 3 holds

( n in dom (if>0 (a,I,J)) & (if>0 (a,I,J)) . n <> halt SCM+FSA )

for I, J being MacroInstruction of SCM+FSA

for n being Element of NAT st n < ((card I) + (card J)) + 3 holds

( n in dom (if>0 (a,I,J)) & (if>0 (a,I,J)) . n <> halt SCM+FSA )

proof end;

theorem Th21: :: SCMFSA8C:29

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds

( I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being Nat st n < pseudo-LifeSpan (s,P,(Directed I)) holds

IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds

DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )

for s being State of SCM+FSA

for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds

( I ";" (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being Nat st n < pseudo-LifeSpan (s,P,(Directed I)) holds

IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) & ( for n being Nat st n <= pseudo-LifeSpan (s,P,(Directed I)) holds

DataPart (Comput ((P +* I),(Initialize s),n)) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),n)) ) )

proof end;

theorem Th22: :: SCMFSA8C:30

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds

DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))

for s being State of SCM+FSA

for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds

DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))

proof end;

theorem :: SCMFSA8C:31

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P holds

DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))

for s being State of SCM+FSA

for I being Program of SCM+FSA st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P holds

DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))

proof end;

theorem Th24: :: SCMFSA8C:32

for I, J being MacroInstruction of SCM+FSA

for a being Int-Location holds (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA

for a being Int-Location holds (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA

proof end;

theorem Th25: :: SCMFSA8C:33

for I, J being MacroInstruction of SCM+FSA

for a being Int-Location holds (if>0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA

for a being Int-Location holds (if>0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA

proof end;

theorem Th26: :: SCMFSA8C:34

for I, J being MacroInstruction of SCM+FSA

for a being Int-Location holds (if=0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)

for a being Int-Location holds (if=0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)

proof end;

theorem Th27: :: SCMFSA8C:35

for I, J being MacroInstruction of SCM+FSA

for a being Int-Location holds (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)

for a being Int-Location holds (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)

proof end;

::$CT

theorem Th28: :: SCMFSA8C:37

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if=0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if=0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )

proof end;

theorem :: SCMFSA8C:38

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a = 0 & Directed I is_pseudo-closed_on s,P holds

DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s))

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a = 0 & Directed I is_pseudo-closed_on s,P holds

DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s))

proof end;

theorem Th30: :: SCMFSA8C:39

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if>0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if>0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )

proof end;

theorem :: SCMFSA8C:40

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a > 0 & Directed I is_pseudo-closed_on s,P holds

DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s))

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a > 0 & Directed I is_pseudo-closed_on s,P holds

DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s))

proof end;

theorem Th32: :: SCMFSA8C:41

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if=0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if=0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )

proof end;

theorem :: SCMFSA8C:42

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <> 0 & Directed J is_pseudo-closed_on s,P holds

DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s))

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <> 0 & Directed J is_pseudo-closed_on s,P holds

DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s))

proof end;

theorem Th34: :: SCMFSA8C:43

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if>0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Start-At (0,SCM+FSA)))) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

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

( if>0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Start-At (0,SCM+FSA)))) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )

proof end;

theorem :: SCMFSA8C:44

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds

DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s))

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds

DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ";" (Stop SCM+FSA)),P,s))

proof end;

theorem :: SCMFSA8C:45

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_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 MacroInstruction of SCM+FSA

for a being read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_on s,P holds

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

proof end;

theorem :: SCMFSA8C:46

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_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 MacroInstruction of SCM+FSA

for a being read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_on s,P holds

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

proof end;

theorem :: SCMFSA8C:47

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a holds

not Directed I destroys a by SCMFSA8A:13;

for a being Int-Location st not I destroys a holds

not Directed I destroys a by SCMFSA8A:13;

theorem Th39: :: SCMFSA8C:48

for i being Instruction of SCM+FSA

for a being Int-Location st not i destroys a holds

not Macro i destroys a

for a being Int-Location st not i destroys a holds

not Macro i destroys a

proof end;

theorem :: SCMFSA8C:51

for i being Instruction of SCM+FSA

for a being Int-Location st not i refers a holds

not Macro i refers a

for a being Int-Location st not i refers a holds

not Macro i refers a

proof end;

theorem Th43: :: SCMFSA8C:52

for I, J being Program of SCM+FSA

for a being Int-Location st not I destroys a & not J destroys a holds

not I ";" J destroys a

for a being Int-Location st not I destroys a & not J destroys a holds

not I ";" J destroys a

proof end;

theorem Th44: :: SCMFSA8C:53

for J being Program of SCM+FSA

for i being Instruction of SCM+FSA

for a being Int-Location st not i destroys a & not J destroys a holds

not i ";" J destroys a

for i being Instruction of SCM+FSA

for a being Int-Location st not i destroys a & not J destroys a holds

not i ";" J destroys a

proof end;

theorem Th45: :: SCMFSA8C:54

for I being Program of SCM+FSA

for j being Instruction of SCM+FSA

for a being Int-Location st not I destroys a & not j destroys a holds

not I ";" j destroys a

for j being Instruction of SCM+FSA

for a being Int-Location st not I destroys a & not j destroys a holds

not I ";" j destroys a

proof end;

theorem :: SCMFSA8C:55

for i, j being Instruction of SCM+FSA

for a being Int-Location st not i destroys a & not j destroys a holds

not i ";" j destroys a

for a being Int-Location st not i destroys a & not j destroys a holds

not i ";" j destroys a

proof end;

theorem Th49: :: SCMFSA8C:58

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds

( ( for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a ) & ( for f being FinSeq-Location holds (IExec (I,P,s)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f ) )

for s being State of SCM+FSA

for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds

( ( for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a ) & ( for f being FinSeq-Location holds (IExec (I,P,s)) . f = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . f ) )

proof end;

theorem Th50: :: SCMFSA8C:59

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being parahalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a

for s being State of SCM+FSA

for I being parahalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a

proof end;

theorem Th51: :: SCMFSA8C:60

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 a being Int-Location

for k being Element of NAT st I is_halting_on Initialized s,P & not I destroys a holds

(IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),k)) . a

for s being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location

for k being Element of NAT st I is_halting_on Initialized s,P & not I destroys a holds

(IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),k)) . a

proof end;

theorem Th52: :: SCMFSA8C:61

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for a being Int-Location

for k being Element of NAT st not I destroys a holds

(IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),k)) . a

for s being State of SCM+FSA

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

for a being Int-Location

for k being Element of NAT st not I destroys a holds

(IExec (I,P,s)) . a = (Comput ((P +* I),(Initialize (Initialized s)),k)) . a

proof end;

theorem Th53: :: SCMFSA8C:62

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for a being Int-Location st not I destroys a holds

(IExec (I,P,s)) . a = (Initialized s) . a

for s being State of SCM+FSA

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

for a being Int-Location st not I destroys a holds

(IExec (I,P,s)) . a = (Initialized s) . a

proof end;

theorem Th54: :: SCMFSA8C:63

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds

( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )

for s being State of SCM+FSA

for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds

( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )

proof end;

theorem Th55: :: SCMFSA8C:64

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a holds

for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds

(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a

for s being State of SCM+FSA

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a holds

for k being Element of NAT st IC (Comput ((P +* I),(Initialize s),k)) in dom I holds

(Comput ((P +* I),(Initialize s),(k + 1))) . a = (Comput ((P +* I),(Initialize s),k)) . a

proof end;

theorem Th56: :: SCMFSA8C:65

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a holds

for m being Nat st ( for n being Nat st n < m holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds

for n being Nat st n <= m holds

(Comput ((P +* I),(Initialize s),n)) . a = s . a

for s being State of SCM+FSA

for I being Program of SCM+FSA

for a being Int-Location st not I destroys a holds

for m being Nat st ( for n being Nat st n < m holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds

for n being Nat st n <= m holds

(Comput ((P +* I),(Initialize s),n)) . a = s . a

proof end;

theorem Th57: :: SCMFSA8C:66

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being good Program of SCM+FSA

for m being Nat st ( for n being Nat st n < m holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds

for n being Nat st n <= m holds

(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) by Th56, SCMFSA7B:def 5;

for s being State of SCM+FSA

for I being good Program of SCM+FSA

for m being Nat st ( for n being Nat st n < m holds

IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds

for n being Nat st n <= m holds

(Comput ((P +* I),(Initialize s),n)) . (intloc 0) = s . (intloc 0) by Th56, SCMFSA7B:def 5;

registration

ex b_{1} being MacroInstruction of SCM+FSA st

( b_{1} is good & b_{1} is keeping_0 & b_{1} is really-closed & b_{1} is parahalting )
end;

cluster V4() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V24() V38() initial non halt-free halt-ending unique-halt keeping_0 good really-closed parahalting for set ;

existence ex b

( b

proof end;

theorem :: SCMFSA8C:67

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being good really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds

( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )

for s being State of SCM+FSA

for I being good really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds

( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )

proof end;

theorem :: SCMFSA8C:68

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being good really-closed Program of SCM+FSA

for k being Nat holds (Comput ((P +* I),(Initialize s),k)) . (intloc 0) = s . (intloc 0) by SCMFSA7B:21, SCMFSA7B:def 5;

for s being State of SCM+FSA

for I being good really-closed Program of SCM+FSA

for k being Nat holds (Comput ((P +* I),(Initialize s),k)) . (intloc 0) = s . (intloc 0) by SCMFSA7B:21, SCMFSA7B:def 5;

theorem :: SCMFSA8C:69

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being keeping_0 really-closed parahalting Program of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

(Comput ((P +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((P +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

for s being State of SCM+FSA

for I being keeping_0 really-closed parahalting Program of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

(Comput ((P +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((P +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

proof end;

theorem :: SCMFSA8C:70

theorem Th62: :: SCMFSA8C:71

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 I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* I),(Initialize s1),k) = 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 st I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

for k being Nat holds

( Comput ((P1 +* I),(Initialize s1),k) = 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 Th63: :: SCMFSA8C:72

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 I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds

( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )

for s1, s2 being State of SCM+FSA

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

( LifeSpan ((P1 +* I),(Initialize s1)) = LifeSpan ((P2 +* I),(Initialize s2)) & Result ((P1 +* I),(Initialize s1)) = Result ((P2 +* I),(Initialize s2)) )

proof end;

theorem :: SCMFSA8C:73

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

for s1, s2 being 0 -started State of SCM+FSA

for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

for s1, s2 being 0 -started State of SCM+FSA

for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds

Result (P1,s1) = Result (P2,s2)

proof end;

canceled;

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

while>0 (a,(I ";" (SubFrom (a,(intloc 0))))) is Program of SCM+FSA;

;

end;
let I be MacroInstruction of SCM+FSA ;

func Times (a,I) -> Program of SCM+FSA equals :: SCMFSA8C:def 1

while>0 (a,(I ";" (SubFrom (a,(intloc 0)))));

correctness while>0 (a,(I ";" (SubFrom (a,(intloc 0)))));

coherence

while>0 (a,(I ";" (SubFrom (a,(intloc 0))))) is Program of SCM+FSA;

;

:: deftheorem defines Times SCMFSA8C:def 1 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds Times (a,I) = while>0 (a,(I ";" (SubFrom (a,(intloc 0)))));

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds Times (a,I) = while>0 (a,(I ";" (SubFrom (a,(intloc 0)))));

registration

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

( Times (a,I) is halt-ending & Times (a,I) is unique-halt )

end;
let I be MacroInstruction of SCM+FSA ;

coherence

( Times (a,I) is halt-ending & Times (a,I) is unique-halt )

proof end;

::$CT 6

theorem :: SCMFSA8C:88

for I, J being MacroInstruction of SCM+FSA

for a, c being Int-Location st not I destroys c & not J destroys c holds

( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c )

for a, c being Int-Location st not I destroys c & not J destroys c holds

( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c )

proof end;

::$CT 2

theorem :: SCMFSA8C:91

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being good really-closed parahalting Program of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1

for s being State of SCM+FSA

for I being good really-closed parahalting Program of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

(IExec ((I ";" (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1

proof end;

Lm1: for aa being Int-Location

for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds

not I ';' J destroys aa

proof end;

Lm2: for aa being Int-Location

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not I ';' (goto 0) destroys aa

proof end;

Lm3: for aa, bb being Int-Location

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not if>0 (bb,(I ';' (goto 0))) destroys aa

proof end;

theorem Th67: :: SCMFSA8C:92

for aa, bb being Int-Location

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not while>0 (bb,I) destroys aa

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not while>0 (bb,I) destroys aa

proof end;

theorem :: SCMFSA8C:93

for I being MacroInstruction of SCM+FSA

for a, b being Int-Location st not I destroys b & a <> b holds

not Times (a,I) destroys b

for a, b being Int-Location st not I destroys b & a <> b holds

not Times (a,I) destroys b

proof end;

theorem :: SCMFSA8C:94

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds card (Times (a,I)) = (card I) + 7

for I being MacroInstruction of SCM+FSA holds card (Times (a,I)) = (card I) + 7

proof end;

theorem :: SCMFSA8C:95

for s being State of SCM+FSA

for a being Int-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,p & not I destroys a holds

(IExec (I,p,s)) . a = (Initialized s) . a

for a being Int-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,p & not I destroys a holds

(IExec (I,p,s)) . a = (Initialized s) . a

proof end;

theorem :: SCMFSA8C:96

for aa being Int-Location

for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds

not I ';' J destroys aa by Lm1;

for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds

not I ';' J destroys aa by Lm1;

theorem :: SCMFSA8C:97

for aa being Int-Location

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not I ';' (goto 0) destroys aa by Lm2;

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not I ';' (goto 0) destroys aa by Lm2;

theorem :: SCMFSA8C:98

for aa, bb being Int-Location

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not if>0 (bb,(I ';' (goto 0))) destroys aa by Lm3;

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not if>0 (bb,(I ';' (goto 0))) destroys aa by Lm3;

theorem :: SCMFSA8C:99

for aa, bb being Int-Location

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not if=0 (bb,(I ';' (goto 0))) destroys aa

for I being MacroInstruction of SCM+FSA st not I destroys aa holds

not if=0 (bb,(I ';' (goto 0))) destroys aa

proof end;