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;
theorem
canceled;
theorem Th16:
theorem Th17:
theorem
theorem
theorem
canceled;
theorem Th21:
theorem Th22:
:: deftheorem SCMFSA6A:def 3 :
canceled;
:: 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
theorem
theorem
theorem