:: SCMFSA8C semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster pseudo-paraclosed FinPartState of SCM+FSA ;
existence
ex b1 being Macro-Instruction st b1 is pseudo-paraclosed
proof end;
end;

theorem :: SCMFSA8C:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: SCMFSA8C:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for k being Nat st ( for n being Nat st n <= k holds
IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P ) holds
k < pseudo-LifeSpan s,P
proof end;

theorem :: SCMFSA8C:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SCMFSA8C:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: SCMFSA8C:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: SCMFSA8C:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for x being set st x in dom f holds
f +* (x .--> (f . x)) = f
proof end;

theorem Th7: :: SCMFSA8C:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being Instruction-Location of SCM+FSA holds l + 0 = l
proof end;

theorem Th8: :: SCMFSA8C:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds IncAddr i,0 = i
proof end;

theorem Th9: :: SCMFSA8C:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being programmed FinPartState of SCM+FSA holds ProgramPart (Relocated P,0) = P
proof end;

theorem Th10: :: SCMFSA8C:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being FinPartState of SCM+FSA st P c= Q holds
ProgramPart P c= ProgramPart Q
proof end;

theorem Th11: :: SCMFSA8C:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being programmed FinPartState of SCM+FSA
for k being Nat st P c= Q holds
Shift P,k c= Shift Q,k
proof end;

theorem Th12: :: SCMFSA8C:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, Q being FinPartState of SCM+FSA
for k being Nat st P c= Q holds
ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k)
proof end;

theorem Th13: :: SCMFSA8C:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for k being Nat st card I <= k & k < (card I) + (card J) holds
for i being Instruction of SCM+FSA st i = J . (insloc (k -' (card I))) holds
(I ';' J) . (insloc k) = IncAddr i,(card I)
proof end;

theorem Th14: :: SCMFSA8C:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA st s . (intloc 0) = 1 & IC s = insloc 0 holds
Initialize s = s
proof end;

theorem Th15: :: SCMFSA8C:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA holds Initialize (Initialize s) = Initialize s
proof end;

theorem Th16: :: SCMFSA8C:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction holds s +* ((Initialized I) +* (Start-At (insloc 0))) = (Initialize s) +* (I +* (Start-At (insloc 0)))
proof end;

theorem Th17: :: SCMFSA8C:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction holds IExec I,s = IExec I,(Initialize s)
proof end;

theorem Th18: :: SCMFSA8C:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st s . (intloc 0) = 1 holds
s +* (I +* (Start-At (insloc 0))) = s +* (Initialized I)
proof end;

theorem Th19: :: SCMFSA8C:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds I +* (Start-At (insloc 0)) c= Initialized I
proof end;

theorem Th20: :: SCMFSA8C:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for l being Instruction-Location of SCM+FSA
for I being Macro-Instruction holds
( l in dom I iff l in dom (Initialized I) )
proof end;

theorem :: SCMFSA8C:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction holds
( Initialized I is_closed_on s iff I is_closed_on Initialize s )
proof end;

theorem Th22: :: SCMFSA8C:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction holds
( Initialized I is_halting_on s iff I is_halting_on Initialize s )
proof end;

theorem :: SCMFSA8C:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction st ( for s being State of SCM+FSA holds I is_halting_on Initialize s ) holds
Initialized I is halting
proof end;

theorem Th24: :: SCMFSA8C:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction st ( for s being State of SCM+FSA holds Initialized I is_halting_on s ) holds
Initialized I is halting
proof end;

theorem Th25: :: SCMFSA8C:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds ProgramPart (Initialized I) = I
proof end;

theorem Th26: :: SCMFSA8C:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction
for l being Instruction-Location of SCM+FSA
for x being set st x in dom I holds
I . x = (s +* (I +* (Start-At l))) . x
proof end;

theorem Th27: :: SCMFSA8C:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA st s . (intloc 0) = 1 holds
(Initialize s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th28: :: SCMFSA8C:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location
for l being Instruction-Location of SCM+FSA holds (s +* (I +* (Start-At l))) . a = s . a
proof end;

theorem :: SCMFSA8C:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being programmed FinPartState of SCM+FSA
for l being Instruction-Location of SCM+FSA holds IC SCM+FSA in dom (I +* (Start-At l))
proof end;

theorem :: SCMFSA8C:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being programmed FinPartState of SCM+FSA
for l being Instruction-Location of SCM+FSA holds (I +* (Start-At l)) . (IC SCM+FSA ) = l
proof end;

theorem Th31: :: SCMFSA8C:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for P being FinPartState of SCM+FSA
for l being Instruction-Location of SCM+FSA holds IC (s +* (P +* (Start-At l))) = l
proof end;

theorem Th32: :: SCMFSA8C:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds
(Exec i,s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th33: :: SCMFSA8C:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA st s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem :: SCMFSA8C:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for P being programmed FinPartState of SCM+FSA holds (s +* P) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th35: :: SCMFSA8C:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, ss being State of SCM+FSA holds (s +* (ss | the Instruction-Locations of SCM+FSA )) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th36: :: SCMFSA8C:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA holds (Initialize s) | the Instruction-Locations of SCM+FSA = s | the Instruction-Locations of SCM+FSA
proof end;

theorem Th37: :: SCMFSA8C:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, ss being State of SCM+FSA
for I being Macro-Instruction holds (ss +* (s | the Instruction-Locations of SCM+FSA )) | (Int-Locations \/ FinSeq-Locations ) = ss | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th38: :: SCMFSA8C:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA holds IExec SCM+FSA-Stop ,s = (Initialize s) +* (Start-At (insloc 0))
proof end;

theorem Th39: :: SCMFSA8C:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s holds
insloc 0 in dom I
proof end;

theorem :: SCMFSA8C:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being paraclosed Macro-Instruction holds insloc 0 in dom I
proof end;

theorem Th41: :: SCMFSA8C:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA holds rng (Macro i) = {i,(halt SCM+FSA )}
proof end;

theorem Th42: :: SCMFSA8C:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s1 & I +* (Start-At (insloc 0)) c= s1 holds
for n being Nat st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for i being Nat holds
( (IC ((Computation s1) . i)) + n = IC ((Computation s2) . i) & IncAddr (CurInstr ((Computation s1) . i)),n = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s2) . i) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th43: :: SCMFSA8C:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s1 & I +* (Start-At (insloc 0)) c= s1 & I +* (Start-At (insloc 0)) c= s2 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for i being Nat holds
( IC ((Computation s1) . i) = IC ((Computation s2) . i) & CurInstr ((Computation s1) . i) = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s2) . i) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th44: :: SCMFSA8C:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (insloc 0)) c= s1 & I +* (Start-At (insloc 0)) c= s2 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
LifeSpan s1 = LifeSpan s2
proof end;

theorem Th45: :: SCMFSA8C:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st s1 . (intloc 0) = 1 & I is_closed_on s1 & I is_halting_on s1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
(IExec I,s1) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s2) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th46: :: SCMFSA8C:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st s1 . (intloc 0) = 1 & I is_closed_on s1 & I is_halting_on s1 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
(IExec I,s1) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,s2) | (Int-Locations \/ FinSeq-Locations )
proof end;

registration
let I be Macro-Instruction;
cluster Initialized I -> initial ;
correctness
coherence
Initialized I is initial;
proof end;
end;

Lm1: now
let s be State of SCM+FSA ; :: thesis: for I being Macro-Instruction holds
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )
let I be Macro-Instruction; :: thesis: ( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )
A1: ProgramPart (Initialized I) = I by Th25;
hereby :: thesis: ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) )
assume A2: Initialized I is_pseudo-closed_on s ; :: thesis: ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )
set k = pseudo-LifeSpan s,(Initialized I);
( IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . (pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart (Initialized I))) & ( for n being Nat st n < pseudo-LifeSpan s,(Initialized I) holds
IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom (Initialized I) ) ) by A2, SCMFSA8A:def 5;
then IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart (Initialized I))) by Th16;
then A3: IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart I)) by A1, AMI_5:72;
A4: now
let n be Nat; :: thesis: ( n < pseudo-LifeSpan s,(Initialized I) implies IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom I )
assume n < pseudo-LifeSpan s,(Initialized I) ; :: thesis: IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom I
then IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom (Initialized I) by A2, SCMFSA8A:def 5;
then IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom (Initialized I) by Th16;
hence IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom I by Th20; :: thesis: verum
end;
then A5: for n being Nat st not IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom I holds
pseudo-LifeSpan s,(Initialized I) <= n ;
thus I is_pseudo-closed_on Initialize s by A3, A4, SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I
hence pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by A3, A5, SCMFSA8A:def 5; :: thesis: verum
end;
assume A6: I is_pseudo-closed_on Initialize s ; :: thesis: ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )
set k = pseudo-LifeSpan (Initialize s),I;
( IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart I)) & ( for n being Nat st n < pseudo-LifeSpan (Initialize s),I holds
IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom I ) ) by A6, SCMFSA8A:def 5;
then IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . (pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart I)) by Th16;
then A7: IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . (pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart (Initialized I))) by A1, AMI_5:72;
A8: now
let n be Nat; :: thesis: ( n < pseudo-LifeSpan (Initialize s),I implies IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom (Initialized I) )
assume n < pseudo-LifeSpan (Initialize s),I ; :: thesis: IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom (Initialized I)
then IC ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . n) in dom I by A6, SCMFSA8A:def 5;
then IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom I by Th16;
hence IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom (Initialized I) by Th20; :: thesis: verum
end;
then A9: for n being Nat st not IC ((Computation (s +* ((Initialized I) +* (Start-At (insloc 0))))) . n) in dom (Initialized I) holds
pseudo-LifeSpan (Initialize s),I <= n ;
thus Initialized I is_pseudo-closed_on s by A7, A8, SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I
hence pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by A7, A9, SCMFSA8A:def 5; :: thesis: verum
end;

theorem :: SCMFSA8C:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction holds
( Initialized I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s ) by Lm1;

theorem :: SCMFSA8C:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_pseudo-closed_on Initialize s holds
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by Lm1;

theorem :: SCMFSA8C:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st Initialized I is_pseudo-closed_on s holds
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by Lm1;

theorem Th50: :: SCMFSA8C:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being initial FinPartState of SCM+FSA st I is_pseudo-closed_on s holds
( I is_pseudo-closed_on s +* (I +* (Start-At (insloc 0))) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At (insloc 0)))),I )
proof end;

theorem Th51: :: SCMFSA8C:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I +* (Start-At (insloc 0)) c= s1 & I is_pseudo-closed_on s1 holds
for n being Nat st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
( ( for i being Nat st i < pseudo-LifeSpan s1,I holds
IncAddr (CurInstr ((Computation s1) . i)),n = CurInstr ((Computation s2) . i) ) & ( for i being Nat st i <= pseudo-LifeSpan s1,I holds
( (IC ((Computation s1) . i)) + n = IC ((Computation s2) . i) & ((Computation s1) . i) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s2) . i) | (Int-Locations \/ FinSeq-Locations ) ) ) )
proof end;

theorem Th52: :: SCMFSA8C:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) & I is_pseudo-closed_on s1 holds
I is_pseudo-closed_on s2
proof end;

theorem Th53: :: SCMFSA8C:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st s . (intloc 0) = 1 holds
( I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s )
proof end;

Lm2: for l being Instruction-Location of SCM+FSA holds goto l <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;

Lm3: for a being Int-Location
for l being Instruction-Location of SCM+FSA holds a =0_goto l <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;

Lm4: for a being Int-Location
for l being Instruction-Location of SCM+FSA holds a >0_goto l <> halt SCM+FSA
by SCMFSA_2:49, SCMFSA_2:124;

Lm5: for I, J being Macro-Instruction holds ProgramPart (Relocated J,(card I)) c= I ';' J
proof end;

theorem Th54: :: SCMFSA8C:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for I, J being Macro-Instruction 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;

theorem Th55: :: SCMFSA8C:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for I, J being Macro-Instruction 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 Th56: :: SCMFSA8C:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for I, J being Macro-Instruction
for n being Nat st n < ((card I) + (card J)) + 3 holds
( insloc n in dom (if=0 a,I,J) & (if=0 a,I,J) . (insloc n) <> halt SCM+FSA )
proof end;

theorem Th57: :: SCMFSA8C:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for I, J being Macro-Instruction
for n being Nat st n < ((card I) + (card J)) + 3 holds
( insloc n in dom (if>0 a,I,J) & (if>0 a,I,J) . (insloc n) <> halt SCM+FSA )
proof end;

theorem Th58: :: SCMFSA8C:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st Directed I is_pseudo-closed_on s holds
( I ';' SCM+FSA-Stop is_closed_on s & I ';' SCM+FSA-Stop is_halting_on s & LifeSpan (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0)))) = pseudo-LifeSpan s,(Directed I) & ( for n being Nat st n < pseudo-LifeSpan s,(Directed I) holds
IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . n) = IC ((Computation (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . n) ) & ( for n being Nat st n <= pseudo-LifeSpan s,(Directed I) holds
((Computation (s +* (I +* (Start-At (insloc 0))))) . n) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . n) | (Int-Locations \/ FinSeq-Locations ) ) )
proof end;

theorem Th59: :: SCMFSA8C:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st Directed I is_pseudo-closed_on s holds
(Result (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (I +* (Start-At (insloc 0))))) . (pseudo-LifeSpan s,(Directed I))) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem :: SCMFSA8C:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s holds
(IExec (I ';' SCM+FSA-Stop ),s) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (I +* (Start-At (insloc 0))))) . (pseudo-LifeSpan s,(Directed I))) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th61: :: SCMFSA8C:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a being Int-Location holds (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) = halt SCM+FSA
proof end;

theorem Th62: :: SCMFSA8C:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a being Int-Location holds (if>0 a,I,J) . (insloc (((card I) + (card J)) + 3)) = halt SCM+FSA
proof end;

theorem Th63: :: SCMFSA8C:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a being Int-Location holds (if=0 a,I,J) . (insloc ((card J) + 2)) = goto (insloc (((card I) + (card J)) + 3))
proof end;

theorem Th64: :: SCMFSA8C:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a being Int-Location holds (if>0 a,I,J) . (insloc ((card J) + 2)) = goto (insloc (((card I) + (card J)) + 3))
proof end;

theorem Th65: :: SCMFSA8C:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J being Macro-Instruction
for a being Int-Location holds (if=0 a,(Goto (insloc 2)),J) . (insloc ((card J) + 3)) = goto (insloc ((card J) + 5))
proof end;

theorem Th66: :: SCMFSA8C:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a = 0 & Directed I is_pseudo-closed_on s holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0)))) = (LifeSpan (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 1 )
proof end;

theorem :: SCMFSA8C:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a = 0 & Directed I is_pseudo-closed_on s holds
(IExec (if=0 a,I,J),s) | (Int-Locations \/ FinSeq-Locations ) = (IExec (I ';' SCM+FSA-Stop ),s) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th68: :: SCMFSA8C:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a > 0 & Directed I is_pseudo-closed_on s holds
( if>0 a,I,J is_halting_on s & if>0 a,I,J is_closed_on s & LifeSpan (s +* ((if>0 a,I,J) +* (Start-At (insloc 0)))) = (LifeSpan (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 1 )
proof end;

theorem Th69: :: SCMFSA8C:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a > 0 & Directed I is_pseudo-closed_on s holds
(IExec (if>0 a,I,J),s) | (Int-Locations \/ FinSeq-Locations ) = (IExec (I ';' SCM+FSA-Stop ),s) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th70: :: SCMFSA8C:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a <> 0 & Directed J is_pseudo-closed_on s holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0)))) = (LifeSpan (s +* ((J ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 3 )
proof end;

theorem :: SCMFSA8C:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <> 0 & Directed J is_pseudo-closed_on s holds
(IExec (if=0 a,I,J),s) | (Int-Locations \/ FinSeq-Locations ) = (IExec (J ';' SCM+FSA-Stop ),s) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th72: :: SCMFSA8C:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . a <= 0 & Directed J is_pseudo-closed_on s holds
( if>0 a,I,J is_halting_on s & if>0 a,I,J is_closed_on s & LifeSpan (s +* ((if>0 a,I,J) +* (Start-At (insloc 0)))) = (LifeSpan (s +* ((J ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) + 3 )
proof end;

theorem Th73: :: SCMFSA8C:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s holds
(IExec (if>0 a,I,J),s) | (Int-Locations \/ FinSeq-Locations ) = (IExec (J ';' SCM+FSA-Stop ),s) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem :: SCMFSA8C:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st Directed I is_pseudo-closed_on s & Directed J is_pseudo-closed_on s holds
( if=0 a,I,J is_closed_on s & if=0 a,I,J is_halting_on s )
proof end;

theorem :: SCMFSA8C:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I, J being Macro-Instruction
for a being read-write Int-Location st Directed I is_pseudo-closed_on s & Directed J is_pseudo-closed_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
proof end;

theorem Th76: :: SCMFSA8C:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction
for a being Int-Location st I does_not_destroy a holds
Directed I does_not_destroy a
proof end;

theorem Th77: :: SCMFSA8C:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA
for a being Int-Location st i does_not_destroy a holds
Macro i does_not_destroy a
proof end;

theorem Th78: :: SCMFSA8C:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location holds halt SCM+FSA does_not_refer a
proof end;

theorem :: SCMFSA8C:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c being Int-Location st a <> b holds
AddTo c,b does_not_refer a
proof end;

theorem :: SCMFSA8C:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA
for a being Int-Location st i does_not_refer a holds
Macro i does_not_refer a
proof end;

theorem Th81: :: SCMFSA8C:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a being Int-Location st I does_not_destroy a & J does_not_destroy a holds
I ';' J does_not_destroy a
proof end;

theorem Th82: :: SCMFSA8C:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for J being Macro-Instruction
for i being Instruction of SCM+FSA
for a being Int-Location st i does_not_destroy a & J does_not_destroy a holds
i ';' J does_not_destroy a
proof end;

theorem :: SCMFSA8C:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction
for j being Instruction of SCM+FSA
for a being Int-Location st I does_not_destroy a & j does_not_destroy a holds
I ';' j does_not_destroy a
proof end;

theorem :: SCMFSA8C:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Instruction of SCM+FSA
for a being Int-Location st i does_not_destroy a & j does_not_destroy a holds
i ';' j does_not_destroy a
proof end;

theorem Th85: :: SCMFSA8C:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location holds SCM+FSA-Stop does_not_destroy a
proof end;

theorem Th86: :: SCMFSA8C:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Int-Location
for l being Instruction-Location of SCM+FSA holds Goto l does_not_destroy a
proof end;

theorem Th87: :: SCMFSA8C:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_halting_on Initialize s holds
( ( for a being read-write Int-Location holds (IExec I,s) . a = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0)))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0)))))) . f ) )
proof end;

theorem Th88: :: SCMFSA8C:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting Macro-Instruction
for a being read-write Int-Location holds (IExec I,s) . a = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0)))))) . a
proof end;

theorem Th89: :: SCMFSA8C:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location
for k being Nat st I is_closed_on Initialize s & I is_halting_on Initialize s & I does_not_destroy a holds
(IExec I,s) . a = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . k) . a
proof end;

theorem Th90: :: SCMFSA8C:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting Macro-Instruction
for a being Int-Location
for k being Nat st I does_not_destroy a holds
(IExec I,s) . a = ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . k) . a
proof end;

theorem Th91: :: SCMFSA8C:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting Macro-Instruction
for a being Int-Location st I does_not_destroy a holds
(IExec I,s) . a = (Initialize s) . a
proof end;

theorem Th92: :: SCMFSA8C:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being keeping_0 Macro-Instruction st I is_halting_on Initialize s holds
( (IExec I,s) . (intloc 0) = 1 & ( for k being Nat holds ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . k) . (intloc 0) = 1 ) )
proof end;

theorem Th93: :: SCMFSA8C:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location st I does_not_destroy a holds
for k being Nat st IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) in dom I holds
((Computation (s +* (I +* (Start-At (insloc 0))))) . (k + 1)) . a = ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) . a
proof end;

theorem Th94: :: SCMFSA8C:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction
for a being Int-Location st I does_not_destroy a holds
for m being Nat st ( for n being Nat st n < m holds
IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . n) in dom I ) holds
for n being Nat st n <= m holds
((Computation (s +* (I +* (Start-At (insloc 0))))) . n) . a = s . a
proof end;

theorem Th95: :: SCMFSA8C:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being good Macro-Instruction
for m being Nat st ( for n being Nat st n < m holds
IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . n) in dom I ) holds
for n being Nat st n <= m holds
((Computation (s +* (I +* (Start-At (insloc 0))))) . n) . (intloc 0) = s . (intloc 0)
proof end;

theorem Th96: :: SCMFSA8C:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being good Macro-Instruction st I is_halting_on Initialize s & I is_closed_on Initialize s holds
( (IExec I,s) . (intloc 0) = 1 & ( for k being Nat holds ((Computation ((Initialize s) +* (I +* (Start-At (insloc 0))))) . k) . (intloc 0) = 1 ) )
proof end;

theorem :: SCMFSA8C:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being good Macro-Instruction st I is_closed_on s holds
for k being Nat holds ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) . (intloc 0) = s . (intloc 0)
proof end;

theorem Th98: :: SCMFSA8C:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting keeping_0 Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a holds
((Computation ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0))) +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0))) +* (Start-At (insloc 0)))))) . a = (s . a) - 1
proof end;

theorem Th99: :: SCMFSA8C:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Instruction of SCM+FSA st i does_not_destroy intloc 0 holds
Macro i is good
proof end;

theorem Th100: :: SCMFSA8C:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for k being Nat holds
( (Computation (s1 +* (I +* (Start-At (insloc 0))))) . k,(Computation (s2 +* (I +* (Start-At (insloc 0))))) . k equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation (s1 +* (I +* (Start-At (insloc 0))))) . k) = CurInstr ((Computation (s2 +* (I +* (Start-At (insloc 0))))) . k) )
proof end;

theorem Th101: :: SCMFSA8C:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
( LifeSpan (s1 +* (I +* (Start-At (insloc 0)))) = LifeSpan (s2 +* (I +* (Start-At (insloc 0)))) & Result (s1 +* (I +* (Start-At (insloc 0)))), Result (s2 +* (I +* (Start-At (insloc 0)))) equal_outside the Instruction-Locations of SCM+FSA )
proof end;

theorem :: SCMFSA8C:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th103: :: SCMFSA8C:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s1, s2 being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At (insloc 0)) c= s1 & I +* (Start-At (insloc 0)) c= s2 & ex k being Nat st (Computation s1) . k,s2 equal_outside the Instruction-Locations of SCM+FSA holds
Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA
proof end;

registration
let I be Macro-Instruction;
let k be Nat;
cluster IncAddr I,k -> initial ;
correctness
coherence
( IncAddr I,k is initial & IncAddr I,k is programmed );
proof end;
end;

definition
let I be Macro-Instruction;
canceled;
canceled;
canceled;
func loop I -> halt-free Macro-Instruction equals :: SCMFSA8C:def 4
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 0)))) * I;
coherence
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 0)))) * I is halt-free Macro-Instruction
proof end;
end;

:: deftheorem SCMFSA8C:def 1 :
canceled;

:: deftheorem SCMFSA8C:def 2 :
canceled;

:: deftheorem SCMFSA8C:def 3 :
canceled;

:: deftheorem defines loop SCMFSA8C:def 4 :
for I being Macro-Instruction holds loop I = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto (insloc 0)))) * I;

theorem Th104: :: SCMFSA8C:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds loop I = Directed I,(insloc 0) by SCMFSA8A:def 1;

theorem :: SCMFSA8C:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction
for a being Int-Location st I does_not_destroy a holds
loop I does_not_destroy a
proof end;

registration
let I be good Macro-Instruction;
cluster loop I -> good halt-free ;
correctness
coherence
loop I is good;
proof end;
end;

theorem Th106: :: SCMFSA8C:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds dom (loop I) = dom I
proof end;

theorem Th107: :: SCMFSA8C:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction holds not halt SCM+FSA in rng (loop I)
proof end;

theorem Th108: :: SCMFSA8C:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being Macro-Instruction
for x being set st I . x <> halt SCM+FSA holds
(loop I) . x = I . x
proof end;

theorem Th109: :: SCMFSA8C:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
for m being Nat st m <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
(Computation (s +* (I +* (Start-At (insloc 0))))) . m,(Computation (s +* ((loop I) +* (Start-At (insloc 0))))) . m equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem Th110: :: SCMFSA8C:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
for m being Nat st m < LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
CurInstr ((Computation (s +* (I +* (Start-At (insloc 0))))) . m) = CurInstr ((Computation (s +* ((loop I) +* (Start-At (insloc 0))))) . m)
proof end;

Lm6: for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
( CurInstr ((Computation (s +* ((loop I) +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) = goto (insloc 0) & ( for m being Nat st m <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
CurInstr ((Computation (s +* ((loop I) +* (Start-At (insloc 0))))) . m) <> halt SCM+FSA ) )
proof end;

theorem :: SCMFSA8C:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
for m being Nat st m <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
CurInstr ((Computation (s +* ((loop I) +* (Start-At (insloc 0))))) . m) <> halt SCM+FSA by Lm6;

theorem :: SCMFSA8C:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
CurInstr ((Computation (s +* ((loop I) +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) = goto (insloc 0) by Lm6;

theorem Th113: :: SCMFSA8C:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being paraclosed Macro-Instruction st I +* (Start-At (insloc 0)) c= s & s is halting holds
for m being Nat st m <= LifeSpan s holds
(Computation s) . m,(Computation (s +* (loop I))) . m equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem :: SCMFSA8C:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting Macro-Instruction st Initialized I c= s holds
for k being Nat st k <= LifeSpan s holds
CurInstr ((Computation (s +* (loop I))) . k) <> halt SCM+FSA
proof end;

definition
let a be Int-Location ;
let I be Macro-Instruction;
func Times a,I -> Macro-Instruction equals :: SCMFSA8C:def 5
 if>0 a,(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))))),SCM+FSA-Stop ;
correctness
coherence
if>0 a,(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))))),SCM+FSA-Stop is Macro-Instruction;
;
end;

:: deftheorem defines Times SCMFSA8C:def 5 :
for a being Int-Location
for I being Macro-Instruction holds Times a,I = if>0 a,(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))))),SCM+FSA-Stop ;

theorem Th115: :: SCMFSA8C:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being good Macro-Instruction
for a being read-write Int-Location holds if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))) is good
proof end;

theorem Th116: :: SCMFSA8C:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a being Int-Location holds (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0)))) . (insloc ((card (I ';' (SubFrom a,(intloc 0)))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0)))) + 5))
proof end;

theorem Th117: :: SCMFSA8C:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0) = 1 & s . a > 0 holds
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0)))) is_pseudo-closed_on s
proof end;

theorem :: SCMFSA8C:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))))) is_pseudo-closed_on s
proof end;

theorem :: SCMFSA8C:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0) = 1 holds
( Times a,I is_closed_on s & Times a,I is_halting_on s )
proof end;

theorem :: SCMFSA8C:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a holds
Initialized (Times a,I) is halting
proof end;

theorem :: SCMFSA8C:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being Macro-Instruction
for a, c being Int-Location st I does_not_destroy c & J does_not_destroy c holds
( if=0 a,I,J does_not_destroy c & if>0 a,I,J does_not_destroy c )
proof end;

theorem Th122: :: SCMFSA8C:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Nat st
( s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))))) +* (Start-At (insloc 0))) & k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0)))) +* (Start-At (insloc 0))))) + 1 & ((Computation s2) . k) . a = (s . a) - 1 & ((Computation s2) . k) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
((Computation s2) . k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds ((Computation s2) . k) . f = (IExec I,s) . f ) & IC ((Computation s2) . k) = insloc 0 & ( for n being Nat st n <= k holds
IC ((Computation s2) . n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0))))) ) )
proof end;

theorem Th123: :: SCMFSA8C:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 holds
(IExec (Times a,I),s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th124: :: SCMFSA8C:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for I being parahalting good Macro-Instruction
for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
( (IExec (I ';' (SubFrom a,(intloc 0))),s) . a = (s . a) - 1 & (IExec (Times a,I),s) | (Int-Locations \/ FinSeq-Locations ) = (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0))),s)) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem :: SCMFSA8C:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s being State of SCM+FSA
for a, b, c being read-write Int-Location st a <> b & a <> c & b <> c & s . a >= 0 holds
(IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a))
proof end;