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

set A = the Instruction-Locations of SCM+FSA ;

set D = Int-Locations \/ FinSeq-Locations ;

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

theorem Th2: :: SCMFSA8A:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Function
for D being set st dom g misses D holds
(f +* g) | D = f | D
proof end;

theorem Th3: :: SCMFSA8A:3  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 dom (s | the Instruction-Locations of SCM+FSA ) = the Instruction-Locations of SCM+FSA
proof end;

theorem Th4: :: SCMFSA8A:4  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 is halting holds
for k being Nat st LifeSpan s <= k holds
CurInstr ((Computation s) . k) = halt SCM+FSA
proof end;

theorem Th5: :: SCMFSA8A:5  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 is halting holds
for k being Nat st LifeSpan s <= k holds
IC ((Computation s) . k) = IC ((Computation s) . (LifeSpan s))
proof end;

theorem Th6: :: SCMFSA8A:6  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 holds
( s1,s2 equal_outside the Instruction-Locations of SCM+FSA iff ( IC s1 = IC s2 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) ) )
proof end;

theorem Th7: :: SCMFSA8A:7  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 IC (IExec I,s) = IC (Result (s +* (Initialized I)))
proof end;

theorem :: SCMFSA8A:8  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 (Initialize s) +* (Initialized I) = s +* (Initialized I)
proof end;

theorem Th9: :: SCMFSA8A:9  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 l being Instruction-Location of SCM+FSA holds I c= I +* (Start-At l)
proof end;

theorem Th10: :: SCMFSA8A:10  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 l being Instruction-Location of SCM+FSA holds s | (Int-Locations \/ FinSeq-Locations ) = (s +* (Start-At l)) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem :: SCMFSA8A:11  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 holds s | (Int-Locations \/ FinSeq-Locations ) = (s +* (I +* (Start-At l))) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th12: :: SCMFSA8A:12  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 l being Instruction-Location of SCM+FSA holds dom (s | the Instruction-Locations of SCM+FSA ) misses dom (Start-At l)
proof end;

theorem Th13: :: SCMFSA8A:13  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) = (Initialize s) +* (I +* (Start-At (insloc 0)))
proof end;

theorem Th14: :: SCMFSA8A: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
for I1, I2 being Macro-Instruction
for l being Instruction-Location of SCM+FSA holds s +* (I1 +* (Start-At l)),s +* (I2 +* (Start-At l)) equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem Th15: :: SCMFSA8A:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
dom SCM+FSA-Stop = {(insloc 0)} by CQC_LANG:5, SCMFSA_4:def 5;

theorem Th16: :: SCMFSA8A:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( insloc 0 in dom SCM+FSA-Stop & SCM+FSA-Stop . (insloc 0) = halt SCM+FSA ) by Th15, CQC_LANG:6, SCMFSA_4:def 5, TARSKI:def 1;

theorem Th17: :: SCMFSA8A:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
card SCM+FSA-Stop = 1
proof end;

definition
let P be programmed FinPartState of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
func Directed P,l -> programmed FinPartState of SCM+FSA equals :: SCMFSA8A:def 1
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto l))) * P;
coherence
((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto l))) * P is programmed FinPartState of SCM+FSA
proof end;
end;

:: deftheorem defines Directed SCMFSA8A:def 1 :
for P being programmed FinPartState of SCM+FSA
for l being Instruction-Location of SCM+FSA holds Directed P,l = ((id the Instructions of SCM+FSA ) +* ((halt SCM+FSA ) .--> (goto l))) * P;

theorem Th18: :: SCMFSA8A:18  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 holds Directed I = Directed I,(insloc (card I)) by SCMFSA6A:def 1;

registration
let P be programmed FinPartState of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
cluster Directed P,l -> programmed halt-free ;
correctness
coherence
Directed P,l is halt-free;
proof end;
end;

registration
let P be programmed FinPartState of SCM+FSA ;
cluster Directed P -> halt-free ;
correctness
coherence
Directed P is halt-free;
proof end;
end;

theorem Th19: :: SCMFSA8A:19  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
for l being Instruction-Location of SCM+FSA holds dom (Directed P,l) = dom P
proof end;

theorem Th20: :: SCMFSA8A:20  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
for l being Instruction-Location of SCM+FSA holds Directed P,l = P +* (((halt SCM+FSA ) .--> (goto l)) * P)
proof end;

theorem Th21: :: SCMFSA8A:21  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
for l being Instruction-Location of SCM+FSA
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed P,l) . x = goto l ) & ( P . x <> halt SCM+FSA implies (Directed P,l) . x = P . x ) )
proof end;

theorem Th22: :: SCMFSA8A:22  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
for n being Nat st i does_not_destroy a holds
IncAddr i,n does_not_destroy a
proof end;

theorem Th23: :: SCMFSA8A:23  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
for n being Nat
for a being Int-Location st P does_not_destroy a holds
ProgramPart (Relocated P,n) does_not_destroy a
proof end;

theorem Th24: :: SCMFSA8A:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being programmed good FinPartState of SCM+FSA
for n being Nat holds ProgramPart (Relocated P,n) is good
proof end;

theorem Th25: :: SCMFSA8A:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being programmed FinPartState 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 Th26: :: SCMFSA8A:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being programmed good FinPartState of SCM+FSA holds I +* J is good
proof end;

theorem Th27: :: SCMFSA8A:27  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
for a being Int-Location st I does_not_destroy a holds
Directed I,l does_not_destroy a
proof end;

registration
let I be programmed good FinPartState of SCM+FSA ;
let l be Instruction-Location of SCM+FSA ;
cluster Directed I,l -> programmed good halt-free ;
correctness
coherence
Directed I,l is good;
proof end;
end;

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

registration
let I be Macro-Instruction;
let l be Instruction-Location of SCM+FSA ;
cluster Directed I,l -> programmed initial halt-free ;
correctness
coherence
Directed I,l is initial;
proof end;
end;

registration
let I, J be good Macro-Instruction;
cluster I ';' J -> good ;
coherence
I ';' J is good
proof end;
end;

Lm1: for l being Instruction-Location of SCM+FSA holds
( dom ((insloc 0) .--> (goto l)) = {(insloc 0)} & insloc 0 in dom ((insloc 0) .--> (goto l)) & ((insloc 0) .--> (goto l)) . (insloc 0) = goto l & card ((insloc 0) .--> (goto l)) = 1 & not halt SCM+FSA in rng ((insloc 0) .--> (goto l)) )
proof end;

definition
let l be Instruction-Location of SCM+FSA ;
func Goto l -> good halt-free Macro-Instruction equals :: SCMFSA8A:def 2
(insloc 0) .--> (goto l);
coherence
(insloc 0) .--> (goto l) is good halt-free Macro-Instruction
proof end;
end;

:: deftheorem defines Goto SCMFSA8A:def 2 :
for l being Instruction-Location of SCM+FSA holds Goto l = (insloc 0) .--> (goto l);

definition
let s be State of SCM+FSA ;
let P be initial FinPartState of SCM+FSA ;
pred P is_pseudo-closed_on s means :Def3: :: SCMFSA8A:def 3
 ex k being Nat st
( IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . k) = insloc (card (ProgramPart P)) & ( for n being Nat st n < k holds
IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P ) );
end;

:: deftheorem Def3 defines is_pseudo-closed_on SCMFSA8A:def 3 :
for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA holds
( P is_pseudo-closed_on s iff ex k being Nat st
( IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . k) = insloc (card (ProgramPart P)) & ( for n being Nat st n < k holds
IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P ) ) );

definition
let P be initial FinPartState of SCM+FSA ;
attr P is pseudo-paraclosed means :Def4: :: SCMFSA8A:def 4
for s being State of SCM+FSA holds P is_pseudo-closed_on s;
end;

:: deftheorem Def4 defines pseudo-paraclosed SCMFSA8A:def 4 :
for P being initial FinPartState of SCM+FSA holds
( P is pseudo-paraclosed iff for s being State of SCM+FSA holds P is_pseudo-closed_on s );

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

definition
let s be State of SCM+FSA ;
let P be initial FinPartState of SCM+FSA ;
assume A1: P is_pseudo-closed_on s ;
func pseudo-LifeSpan s,P -> Nat means :Def5: :: SCMFSA8A:def 5
( IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . it) = insloc (card (ProgramPart P)) & ( for n being Nat st not IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P holds
it <= n ) );
existence
ex b1 being Nat st
( IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . b1) = insloc (card (ProgramPart P)) & ( for n being Nat st not IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P holds
b1 <= n ) )
proof end;
uniqueness
for b1, b2 being Nat st IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . b1) = insloc (card (ProgramPart P)) & ( for n being Nat st not IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P holds
b1 <= n ) & IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . b2) = insloc (card (ProgramPart P)) & ( for n being Nat st not IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P holds
b2 <= n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines pseudo-LifeSpan SCMFSA8A:def 5 :
for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for b3 being Nat holds
( b3 = pseudo-LifeSpan s,P iff ( IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . b3) = insloc (card (ProgramPart P)) & ( for n being Nat st not IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P holds
b3 <= n ) ) );

theorem Th28: :: SCMFSA8A:28  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 x being set st x in dom I holds
(I ';' J) . x = (Directed I) . x
proof end;

theorem Th29: :: SCMFSA8A:29  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 card (Goto l) = 1 by Lm1;

theorem Th30: :: SCMFSA8A:30  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
for x being set st x in dom P holds
( ( P . x = halt SCM+FSA implies (Directed P) . x = goto (insloc (card P)) ) & ( P . x <> halt SCM+FSA implies (Directed P) . x = P . x ) )
proof end;

theorem Th31: :: SCMFSA8A: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 initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for n being Nat st n < pseudo-LifeSpan s,P holds
( IC ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) in dom P & CurInstr ((Computation (s +* (P +* (Start-At (insloc 0))))) . n) <> halt SCM+FSA )
proof end;

theorem Th32: :: SCMFSA8A: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, J being Macro-Instruction st I is_pseudo-closed_on s holds
for k being Nat st k <= pseudo-LifeSpan s,I holds
(Computation (s +* (I +* (Start-At (insloc 0))))) . k,(Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . k equal_outside the Instruction-Locations of SCM+FSA
proof end;

theorem Th33: :: SCMFSA8A:33  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 card (Directed I,l) = card I
proof end;

theorem Th34: :: SCMFSA8A:34  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 card (Directed I) = card I
proof end;

theorem Th35: :: SCMFSA8A:35  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 k being Nat st k <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
( (Computation (s +* (I +* (Start-At (insloc 0))))) . k,(Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . k equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . k) <> halt SCM+FSA )
proof end;

theorem Th36: :: SCMFSA8A: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
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
( IC ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) = insloc (card I) & ((Computation (s +* (I +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

Lm2: for s being State of SCM+FSA
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1 )
proof end;

theorem :: SCMFSA8A:37  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
Directed I is_pseudo-closed_on s by Lm2;

theorem :: SCMFSA8A: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
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s holds
pseudo-LifeSpan s,(Directed I) = (LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1 by Lm2;

theorem Th39: :: SCMFSA8A:39  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 st I is halt-free holds
Directed I,l = I
proof end;

theorem Th40: :: SCMFSA8A:40  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 I is halt-free holds
Directed I = I
proof end;

theorem Th41: :: SCMFSA8A:41  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 holds (Directed I) ';' J = I ';' J
proof end;

theorem Th42: :: SCMFSA8A:42  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 st I is_closed_on s & I is_halting_on s holds
( ( for k being Nat st k <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
( IC ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . k) = IC ((Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . k) & CurInstr ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . k) = CurInstr ((Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . k) ) ) & ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & IC ((Computation (s +* ((Directed I) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) = IC ((Computation (s +* ((I ';' J) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) )
proof end;

theorem Th43: :: SCMFSA8A:43  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 st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( ( for k being Nat st k <= LifeSpan (s +* (Initialized I)) holds
( IC ((Computation (s +* (Initialized (Directed I)))) . k) = IC ((Computation (s +* (Initialized (I ';' J)))) . k) & CurInstr ((Computation (s +* (Initialized (Directed I)))) . k) = CurInstr ((Computation (s +* (Initialized (I ';' J)))) . k) ) ) & ((Computation (s +* (Initialized (Directed I)))) . ((LifeSpan (s +* (Initialized I))) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (Initialized (I ';' J)))) . ((LifeSpan (s +* (Initialized I))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & IC ((Computation (s +* (Initialized (Directed I)))) . ((LifeSpan (s +* (Initialized I))) + 1)) = IC ((Computation (s +* (Initialized (I ';' J)))) . ((LifeSpan (s +* (Initialized I))) + 1)) )
proof end;

theorem Th44: :: SCMFSA8A:44  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 Initialize s & I is_halting_on Initialize s holds
for k being Nat st k <= LifeSpan (s +* (Initialized I)) holds
( (Computation (s +* (Initialized I))) . k,(Computation (s +* (Initialized (Directed I)))) . k equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation (s +* (Initialized (Directed I)))) . k) <> halt SCM+FSA )
proof end;

theorem Th45: :: SCMFSA8A:45  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 Initialize s & I is_halting_on Initialize s holds
( IC ((Computation (s +* (Initialized (Directed I)))) . ((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & ((Computation (s +* (Initialized I))) . (LifeSpan (s +* (Initialized I)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (Initialized (Directed I)))) . ((LifeSpan (s +* (Initialized I))) + 1)) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

Lm3: for I being Macro-Instruction
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC ((Computation (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) = insloc (card I) & ((Computation (s +* (I +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))) is halting & LifeSpan (s +* ((I ';' SCM+FSA-Stop ) +* (Start-At (insloc 0)))) = (LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1 & I ';' SCM+FSA-Stop is_closed_on s & I ';' SCM+FSA-Stop is_halting_on s )
proof end;

theorem :: SCMFSA8A:46  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 s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( I ';' SCM+FSA-Stop is_closed_on s & I ';' SCM+FSA-Stop is_halting_on s ) by Lm3;

theorem Th47: :: SCMFSA8A:47  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
( insloc 0 in dom (Goto l) & (Goto l) . (insloc 0) = goto l ) by Lm1;

theorem Th48: :: SCMFSA8A:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being with_non-empty_elements set
for S being non empty non void definite AMI-Struct of N
for I being programmed FinPartState of S
for x being set st x in dom I holds
I . x is Instruction of S
proof end;

theorem Th49: :: SCMFSA8A:49  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 x being set
for k being Nat st x in dom (ProgramPart (Relocated I,k)) holds
(ProgramPart (Relocated I,k)) . x = (Relocated I,k) . x
proof end;

theorem Th50: :: SCMFSA8A:50  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 k being Nat holds ProgramPart (Relocated (Directed I),k) = Directed (ProgramPart (Relocated I,k)),(insloc ((card I) + k))
proof end;

theorem Th51: :: SCMFSA8A:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I, J being programmed FinPartState of SCM+FSA
for l being Instruction-Location of SCM+FSA holds Directed (I +* J),l = (Directed I,l) +* (Directed J,l)
proof end;

theorem Th52: :: SCMFSA8A:52  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 holds Directed (I ';' J) = I ';' (Directed J)
proof end;

Lm4: for I being Macro-Instruction
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC ((Computation (s +* (Initialized (I ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & ((Computation (s +* (Initialized I))) . (LifeSpan (s +* (Initialized I)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (Initialized (I ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 1)) | (Int-Locations \/ FinSeq-Locations ) & s +* (Initialized (I ';' SCM+FSA-Stop )) is halting & LifeSpan (s +* (Initialized (I ';' SCM+FSA-Stop ))) = (LifeSpan (s +* (Initialized I))) + 1 )
proof end;

theorem :: SCMFSA8A:53  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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IC ((Computation (s +* (Initialized (I ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) by Lm4;

theorem :: SCMFSA8A:54  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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
((Computation (s +* (Initialized I))) . (LifeSpan (s +* (Initialized I)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (Initialized (I ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 1)) | (Int-Locations \/ FinSeq-Locations ) by Lm4;

theorem :: SCMFSA8A:55  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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
s +* (Initialized (I ';' SCM+FSA-Stop )) is halting by Lm4;

theorem :: SCMFSA8A:56  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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
LifeSpan (s +* (Initialized (I ';' SCM+FSA-Stop ))) = (LifeSpan (s +* (Initialized I))) + 1 by Lm4;

theorem :: SCMFSA8A:57  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 Initialize s & I is_halting_on Initialize s holds
IExec (I ';' SCM+FSA-Stop ),s = (IExec I,s) +* (Start-At (insloc (card I)))
proof end;

Lm5: for I, J being Macro-Instruction
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( IC ((Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 2)) = insloc (((card I) + (card J)) + 1) & ((Computation (s +* (I +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 2)) | (Int-Locations \/ FinSeq-Locations ) & ( for k being Nat st k < (LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 2 holds
CurInstr ((Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . k) <> halt SCM+FSA ) & ( for k being Nat st k <= LifeSpan (s +* (I +* (Start-At (insloc 0)))) holds
IC ((Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . k) = IC ((Computation (s +* (I +* (Start-At (insloc 0))))) . k) ) & IC ((Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 1)) = insloc (card I) & s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))) is halting & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0)))) = (LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 2 )
proof end;

theorem :: SCMFSA8A:58  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 s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( ((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop is_closed_on s & ((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop is_halting_on s )
proof end;

theorem :: SCMFSA8A:59  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 s being State of SCM+FSA st I is_closed_on s & I is_halting_on s holds
s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ) +* (Start-At (insloc 0))) is halting by Lm5;

Lm6: for I, J being Macro-Instruction
for s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC ((Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 2)) = insloc (((card I) + (card J)) + 1) & ((Computation (s +* (Initialized I))) . (LifeSpan (s +* (Initialized I)))) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 2)) | (Int-Locations \/ FinSeq-Locations ) & ( for k being Nat st k < (LifeSpan (s +* (Initialized I))) + 2 holds
CurInstr ((Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )))) . k) <> halt SCM+FSA ) & ( for k being Nat st k <= LifeSpan (s +* (Initialized I)) holds
IC ((Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )))) . k) = IC ((Computation (s +* (Initialized I))) . k) ) & IC ((Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )))) . ((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )) is halting & LifeSpan (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ))) = (LifeSpan (s +* (Initialized I))) + 2 )
proof end;

theorem :: SCMFSA8A:60  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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop )) is halting by Lm6;

theorem :: SCMFSA8A: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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IC (IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ),s) = insloc (((card I) + (card J)) + 1)
proof end;

theorem :: SCMFSA8A: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 s being State of SCM+FSA st I is_closed_on Initialize s & I is_halting_on Initialize s holds
IExec (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' SCM+FSA-Stop ),s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 1)))
proof end;