begin
:: deftheorem defines Directed SCMFSA6A:def 1 :
for P being preProgram of SCM+FSA
for l being Element of NAT holds Directed P,l = P +~ (halt SCM+FSA ),(goto l);
:: deftheorem defines Directed SCMFSA6A:def 2 :
for P being preProgram of SCM+FSA holds Directed P = Directed P,(card P);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem defines Macro SCMFSA6A:def 3 :
for i being Instruction of SCM+FSA holds Macro i = 0 ,1 --> i,(halt SCM+FSA );
theorem
canceled;
theorem Th16:
theorem Th17:
theorem
theorem
theorem
canceled;
theorem Th21:
theorem Th22:
:: deftheorem defines Initialized SCMFSA6A:def 4 :
for I being PartState of SCM+FSA holds Initialized I = (I +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA );
theorem Th23:
theorem Th24:
theorem
Lm1:
not intloc 0 in NAT
by SCMFSA_2:84;
Lm2:
not IC SCM+FSA in NAT
by COMPOS_1:3;
theorem Th26:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th38:
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem
theorem
begin
:: deftheorem defines ';' SCMFSA6A:def 5 :
for I, J being Program of SCM+FSA holds I ';' J = (Directed I) +* (ProgramPart (Relocated J,(card I)));
theorem
theorem
theorem Th56:
theorem
theorem
begin
:: deftheorem defines ';' SCMFSA6A:def 6 :
for i being Instruction of SCM+FSA
for J being Program of SCM+FSA holds i ';' J = (Macro i) ';' J;
:: deftheorem defines ';' SCMFSA6A:def 7 :
for I being Program of SCM+FSA
for j being Instruction of SCM+FSA holds I ';' j = I ';' (Macro j);
:: deftheorem defines ';' SCMFSA6A:def 8 :
for i, j being Instruction of SCM+FSA holds i ';' j = (Macro i) ';' (Macro j);
theorem
theorem
theorem Th61:
theorem
canceled;
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem
theorem
theorem
theorem
theorem
theorem
theorem