begin
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
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)) )
:: deftheorem SCMFSA8A:def 1 :
canceled;
:: deftheorem defines Goto SCMFSA8A:def 2 :
:: deftheorem Def3 defines is_pseudo-closed_on SCMFSA8A:def 3 :
:: deftheorem Def4 defines pseudo-paraclosed SCMFSA8A:def 4 :
definition
let s be
State of ;
let P be
initial FinPartState of ;
assume A1:
P is_pseudo-closed_on s
;
func pseudo-LifeSpan s,
P -> Element of
NAT means :
Def5:
(
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),it) = insloc (card (ProgramPart P)) & ( for
n being
Element of
NAT st not
IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
it <= n ) );
existence
ex b1 being Element of NAT st
( IC (Computation (s +* (P +* (Start-At (insloc 0 )))),b1) = insloc (card (ProgramPart P)) & ( for n being Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
b1 <= n ) )
uniqueness
for b1, b2 being Element of NAT st IC (Computation (s +* (P +* (Start-At (insloc 0 )))),b1) = insloc (card (ProgramPart P)) & ( for n being Element of 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 Element of NAT st not IC (Computation (s +* (P +* (Start-At (insloc 0 )))),n) in dom P holds
b2 <= n ) holds
b1 = b2
end;
:: deftheorem Def5 defines pseudo-LifeSpan SCMFSA8A:def 5 :
theorem Th28:
theorem
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
Lm2:
for s being State of
for I being Program of 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 )
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
Lm3:
for I being Program of
for s being State of st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) & ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 & I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s )
theorem
theorem
Lm4:
for I being Program of
for s being State of st I is_closed_on Initialize s & I is_halting_on Initialize s holds
( IC (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) & ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) & LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 1 )
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
Lm5:
for I, J being Program of
for s being State of st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )
theorem
theorem
Lm6:
for I, J being Program of
for s being State of 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) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) = DataPart (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (Initialized I))) + 2 holds
CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) = IC (Computation (s +* (Initialized I)),k) ) & IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & ProgramPart (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))) & LifeSpan (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 2 )
theorem
theorem
theorem