:: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto

::

:: Received June 20, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

canceled;

::$CD

definition

let P be preProgram of SCM+FSA;

P +~ ((halt SCM+FSA),(goto (card P))) is preProgram of SCM+FSA ;

projectivity

for b_{1}, b_{2} being preProgram of SCM+FSA st b_{1} = b_{2} +~ ((halt SCM+FSA),(goto (card b_{2}))) holds

b_{1} = b_{1} +~ ((halt SCM+FSA),(goto (card b_{1})))
by FUNCT_4:127;

end;
func Directed P -> preProgram of SCM+FSA equals :: SCMFSA6A:def 1

P +~ ((halt SCM+FSA),(goto (card P)));

coherence P +~ ((halt SCM+FSA),(goto (card P)));

P +~ ((halt SCM+FSA),(goto (card P))) is preProgram of SCM+FSA ;

projectivity

for b

b

:: deftheorem defines Directed SCMFSA6A:def 1 :

for P being preProgram of SCM+FSA holds Directed P = P +~ ((halt SCM+FSA),(goto (card P)));

for P being preProgram of SCM+FSA holds Directed P = P +~ ((halt SCM+FSA),(goto (card P)));

registration
end;

theorem :: SCMFSA6A:1

theorem :: SCMFSA6A:2

for m being Nat

for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))

for I being Program of holds Reloc ((Directed I),m) = ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (m + (card I))))) * (Reloc (I,m))

proof end;

set q = (intloc 0) .--> 1;

set f = the_Values_of SCM+FSA;

theorem Th3: :: SCMFSA6A:3

for i being Instruction of SCM+FSA

for s being State of SCM+FSA holds

( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

for s being State of SCM+FSA holds

( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = (IC s) + 1 )

proof end;

::$CT 4

theorem :: SCMFSA6A:8

for s1, s2 being State of SCM+FSA

for n being Nat

for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds

( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )

for n being Nat

for i being Instruction of SCM+FSA st (IC s1) + n = IC s2 & DataPart s1 = DataPart s2 holds

( (IC (Exec (i,s1))) + n = IC (Exec ((IncAddr (i,n)),s2)) & DataPart (Exec (i,s1)) = DataPart (Exec ((IncAddr (i,n)),s2)) )

proof end;

:: deftheorem defines ";" SCMFSA6A:def 3 :

for I, J being Program of holds I ";" J = (stop (Directed I)) ';' J;

for I, J being Program of holds I ";" J = (stop (Directed I)) ';' J;

registration
end;

registration
end;

registration

ex b_{1} being Program of st b_{1} is halt-free
end;

cluster Relation-like NAT -defined the InstructionsF of SCM+FSA -valued V10() non empty Function-like V39() initial halt-free for set ;

existence ex b

proof end;

registration
end;

Lm1: for I being preProgram of SCM+FSA holds card (Directed I) = card I

proof end;

Lm2: for I being Program of holds card (stop (Directed I)) = card (stop I)

proof end;

theorem Th5: :: SCMFSA6A:15

for I, J being Program of

for l being Nat st l in dom I & I . l <> halt SCM+FSA holds

(I ";" J) . l = I . l

for l being Nat st l in dom I & I . l <> halt SCM+FSA holds

(I ";" J) . l = I . l

proof end;

definition

let i be Instruction of SCM+FSA;

let J be Program of ;

correctness

coherence

(Macro i) ";" J is Program of ;

;

end;
let J be Program of ;

correctness

coherence

(Macro i) ";" J is Program of ;

;

:: deftheorem defines ";" SCMFSA6A:def 4 :

for i being Instruction of SCM+FSA

for J being Program of holds i ";" J = (Macro i) ";" J;

for i being Instruction of SCM+FSA

for J being Program of holds i ";" J = (Macro i) ";" J;

definition

let I be Program of ;

let j be Instruction of SCM+FSA;

correctness

coherence

I ";" (Macro j) is Program of ;

;

end;
let j be Instruction of SCM+FSA;

correctness

coherence

I ";" (Macro j) is Program of ;

;

:: deftheorem defines ";" SCMFSA6A:def 5 :

for I being Program of

for j being Instruction of SCM+FSA holds I ";" j = I ";" (Macro j);

for I being Program of

for j being Instruction of SCM+FSA holds I ";" j = I ";" (Macro j);

definition
end;

:: deftheorem defines ";" SCMFSA6A:def 6 :

for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" (Macro j);

for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" (Macro j);

registration

coherence

for b_{1} being Instruction of SCM+FSA st b_{1} is sequential holds

b_{1} is No-StopCode

end;
for b

b

proof end;

registration

let i, j be sequential Instruction of SCM+FSA;

coherence

( i ";" j is halt-ending & i ";" j is unique-halt ) ;

end;
coherence

( i ";" j is halt-ending & i ";" j is unique-halt ) ;

registration

let I be MacroInstruction of SCM+FSA ;

let j be sequential Instruction of SCM+FSA;

coherence

( I ";" j is halt-ending & I ";" j is unique-halt ) ;

end;
let j be sequential Instruction of SCM+FSA;

coherence

( I ";" j is halt-ending & I ";" j is unique-halt ) ;

registration

let i be sequential Instruction of SCM+FSA;

let J be MacroInstruction of SCM+FSA ;

coherence

( i ";" J is halt-ending & i ";" J is unique-halt ) ;

end;
let J be MacroInstruction of SCM+FSA ;

coherence

( i ";" J is halt-ending & i ";" J is unique-halt ) ;

theorem :: SCMFSA6A:22

theorem Th13: :: SCMFSA6A:23

for I being preProgram of SCM+FSA

for k being Element of NAT holds Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))

for k being Element of NAT holds Reloc ((Directed I),k) = (Reloc (I,k)) +~ ((halt SCM+FSA),(goto ((card I) + k)))

proof end;

theorem :: SCMFSA6A:26

theorem :: SCMFSA6A:27

theorem :: SCMFSA6A:28

theorem :: SCMFSA6A:29

theorem :: SCMFSA6A:30

theorem :: SCMFSA6A:31

theorem :: SCMFSA6A:32

theorem :: SCMFSA6A:40

for n being Nat

for I, J being Program of st n in dom (Reloc (J,(card I))) holds

(I ";" J) . n = (Reloc (J,(card I))) . n

for I, J being Program of st n in dom (Reloc (J,(card I))) holds

(I ";" J) . n = (Reloc (J,(card I))) . n

proof end;

registration
end;

theorem :: SCMFSA6A:41

for I, J being MacroInstruction of SCM+FSA

for n being Nat st n < LastLoc I holds

(I ";" J) . n = I . n

for n being Nat st n < LastLoc I holds

(I ";" J) . n = I . n

proof end;