:: Conditional branch macro instructions of SCM+FSA, Part I (preliminary)
:: by Noriko Asamoto
::
:: Copyright (c) 1996-2021 Association of Mizar Users

set A = NAT ;

set D = Data-Locations ;

set SA0 = Start-At (0,SCM+FSA);

set T = () .--> 1;

theorem :: SCMFSA8A:1
canceled;

theorem :: SCMFSA8A:2
canceled;

theorem :: SCMFSA8A:3
canceled;

theorem :: SCMFSA8A:4
canceled;

theorem :: SCMFSA8A:5
canceled;

theorem :: SCMFSA8A:6
canceled;

theorem :: SCMFSA8A:7
canceled;

::$CT 7 theorem Th1: :: SCMFSA8A:8 for i being Instruction of SCM+FSA for a being Int-Location for n being Element of NAT st not i destroys a holds not IncAddr (i,n) destroys a proof end; theorem Th2: :: SCMFSA8A:9 for P being preProgram of SCM+FSA for n being Element of NAT for a being Int-Location st not P destroys a holds not Reloc (P,n) destroys a proof end; theorem Th3: :: SCMFSA8A:10 for P being good preProgram of SCM+FSA for n being Element of NAT holds Reloc (P,n) is good proof end; theorem Th4: :: SCMFSA8A:11 for I, J being preProgram of SCM+FSA for a being Int-Location st not I destroys a & not J destroys a holds not I +* J destroys a proof end; theorem Th5: :: SCMFSA8A:12 for I, J being good preProgram of SCM+FSA holds I +* J is good proof end; theorem Th6: :: SCMFSA8A:13 for I being preProgram of SCM+FSA for a being Int-Location st not I destroys a holds not Directed I destroys a proof end; registration let I be good Program of SCM+FSA; correctness coherence Directed I is good ; proof end; end; registration let I be Program of SCM+FSA; correctness coherence ; ; end; registration let I, J be good Program of SCM+FSA; cluster I ";" J -> good ; coherence I ";" J is good proof end; end; Lm1: for l being Nat holds ( dom (Load (goto l)) = & 0 in dom (Load (goto l)) & (Load (goto l)) . 0 = goto l & card (Load (goto l)) = 1 & not halt SCM+FSA in rng (Load (goto l)) ) proof end; definition let l be Nat; func Goto l -> Program of SCM+FSA equals :: SCMFSA8A:def 1 Load (goto l); coherence Load (goto l) is Program of SCM+FSA ; end; :: deftheorem defines Goto SCMFSA8A:def 1 : for l being Nat holds Goto l = Load (goto l); registration let l be Element of NAT ; coherence ( Goto l is halt-free & Goto l is good ) proof end; end; registration existence ex b1 being Program of SCM+FSA st ( b1 is halt-free & b1 is good ) proof end; end; definition let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; let I be Program of SCM+FSA; pred I is_pseudo-closed_on s,P means :: SCMFSA8A:def 2 ex k being Nat st ( IC (Comput ((P +* I),(),k)) = card I & ( for n being Nat st n < k holds IC (Comput ((P +* I),(),n)) in dom I ) ); end; :: deftheorem defines is_pseudo-closed_on SCMFSA8A:def 2 : for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA holds ( I is_pseudo-closed_on s,P iff ex k being Nat st ( IC (Comput ((P +* I),(),k)) = card I & ( for n being Nat st n < k holds IC (Comput ((P +* I),(),n)) in dom I ) ) ); definition let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; let I be Program of SCM+FSA; assume A1: I is_pseudo-closed_on s,P ; func pseudo-LifeSpan (s,P,I) -> Nat means :Def3: :: SCMFSA8A:def 4 ( IC (Comput ((P +* I),(),it)) = card I & ( for n being Nat st not IC (Comput ((P +* I),(),n)) in dom I holds it <= n ) ); existence ex b1 being Nat st ( IC (Comput ((P +* I),(),b1)) = card I & ( for n being Nat st not IC (Comput ((P +* I),(),n)) in dom I holds b1 <= n ) ) proof end; uniqueness for b1, b2 being Nat st IC (Comput ((P +* I),(),b1)) = card I & ( for n being Nat st not IC (Comput ((P +* I),(),n)) in dom I holds b1 <= n ) & IC (Comput ((P +* I),(),b2)) = card I & ( for n being Nat st not IC (Comput ((P +* I),(),n)) in dom I holds b2 <= n ) holds b1 = b2 proof end; end; :: deftheorem SCMFSA8A:def 3 : canceled; :: deftheorem Def3 defines pseudo-LifeSpan SCMFSA8A:def 4 : for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds for b4 being Nat holds ( b4 = pseudo-LifeSpan (s,P,I) iff ( IC (Comput ((P +* I),(),b4)) = card I & ( for n being Nat st not IC (Comput ((P +* I),(),n)) in dom I holds b4 <= n ) ) ); theorem Th7: :: SCMFSA8A:14 for I, J being Program of SCM+FSA for x being set st x in dom I holds (I ";" J) . x = () . x proof end; theorem :: SCMFSA8A:15 for l being Nat holds card (Goto l) = 1 by Lm1; theorem :: SCMFSA8A:16 for P being preProgram of SCM+FSA for x being set st x in dom P holds ( ( P . x = halt SCM+FSA implies () . x = goto (card P) ) & ( P . x <> halt SCM+FSA implies () . x = P . x ) ) by ; theorem Th10: :: SCMFSA8A:17 for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds for n being Nat st n < pseudo-LifeSpan (s,P,I) holds ( IC (Comput ((P +* I),(),n)) in dom I & CurInstr ((P +* I),(Comput ((P +* I),(),n))) <> halt SCM+FSA ) proof end; theorem Th11: :: SCMFSA8A:18 for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for I, J being Program of SCM+FSA st I is_pseudo-closed_on s,P holds for k being Nat st k <= pseudo-LifeSpan (s,P,I) holds Comput ((P +* I),(),k) = Comput ((P +* (I ";" J)),(),k) proof end; theorem :: SCMFSA8A:19 canceled; theorem :: SCMFSA8A:20 canceled; ::$CT 2
theorem Th12: :: SCMFSA8A:21
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
for k being Nat st k <= LifeSpan ((P +* I),()) holds
( Comput ((P +* I),(),k) = Comput ((P +* ()),(),k) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) <> halt SCM+FSA )
proof end;

theorem Th13: :: SCMFSA8A:22
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) )
proof end;

Lm2: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 )

proof end;

theorem :: SCMFSA8A:23
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
Directed I is_pseudo-closed_on s,P by Lm2;

theorem :: SCMFSA8A:24
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 by Lm2;

theorem :: SCMFSA8A:25
for I, J being Program of SCM+FSA holds () ";" J = I ";" J ;

theorem Th17: :: SCMFSA8A:26
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA st I is_halting_on s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
( IC (Comput ((P +* ()),(),k)) = IC (Comput ((P +* (I ";" J)),(),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(),k))) ) ) & DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) & IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" J)),(),((LifeSpan ((P +* I),())) + 1))) )
proof end;

theorem Th18: :: SCMFSA8A:27
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA st I is_halting_on Initialized s,P holds
( ( for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize (() .--> 1)))) holds
( IC (Comput ((P +* ()),(s +* (Initialize (() .--> 1))),k)) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize (() .--> 1))),k)) & CurInstr ((P +* ()),(Comput ((P +* ()),(s +* (Initialize (() .--> 1))),k))) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize (() .--> 1))),k))) ) ) & DataPart (Comput ((P +* ()),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) & IC (Comput ((P +* ()),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) = IC (Comput ((P +* (I ";" J)),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) )
proof end;

theorem Th19: :: SCMFSA8A:28
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds
for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize (() .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize (() .--> 1))),k) = Comput ((P +* ()),(s +* (Initialize (() .--> 1))),k) & CurInstr ((P +* ()),(Comput ((P +* ()),(s +* (Initialize (() .--> 1))),k))) <> halt SCM+FSA )
proof end;

theorem Th20: :: SCMFSA8A:29
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds
( IC (Comput ((P +* ()),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize (() .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))))) = DataPart (Comput ((P +* ()),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) )
proof end;

Lm3: for I being really-closed Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) & P +* (I ";" ()) halts_on Initialize s & LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P )

proof end;

theorem :: SCMFSA8A:30
for I being really-closed Program of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
I ";" () is_halting_on s,P by Lm3;

theorem :: SCMFSA8A:31
for l being Nat holds
( 0 in dom (Goto l) & (Goto l) . 0 = goto l ) by Lm1;

Lm4: for I being really-closed Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (I ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize (() .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))))) = DataPart (Comput ((P +* (I ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) & P +* (I ";" ()) halts_on s +* (Initialize (() .--> 1)) & LifeSpan ((P +* (I ";" ())),(s +* (Initialize (() .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1 )

proof end;

theorem :: SCMFSA8A:32
for I being really-closed Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
IC (Comput ((P +* (I ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) = card I by Lm4;

theorem :: SCMFSA8A:33
for I being really-closed Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
DataPart (Comput ((P +* I),(s +* (Initialize (() .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))))) = DataPart (Comput ((P +* (I ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) by Lm4;

theorem :: SCMFSA8A:34
for I being really-closed Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
P +* (I ";" ()) halts_on s +* (Initialize (() .--> 1)) by Lm4;

theorem :: SCMFSA8A:35
for I being really-closed Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
LifeSpan ((P +* (I ";" ())),(s +* (Initialize (() .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1 by Lm4;

theorem :: SCMFSA8A:36
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds
IExec ((I ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
proof end;

Lm5: for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),((LifeSpan ((P +* I),())) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),((LifeSpan ((P +* I),())) + 2))) & ( for k being Nat st k < (LifeSpan ((P +* I),())) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),k))) <> halt SCM+FSA ) & ( for k being Nat st k <= LifeSpan ((P +* I),()) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),k)) = IC (Comput ((P +* I),(),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on Initialize s & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),()) = (LifeSpan ((P +* I),())) + 2 )

proof end;

theorem :: SCMFSA8A:37
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P
proof end;

theorem :: SCMFSA8A:38
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on s,P holds
P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on Initialize s by Lm5;

Lm6: for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
( IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 2))) = ((card I) + (card J)) + 1 & DataPart (Comput ((P +* I),(s +* (Initialize (() .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 2))) & ( for k being Nat st k < (LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 2 holds
CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(s +* (Initialize (() .--> 1))),k))) <> halt SCM+FSA ) & ( for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize (() .--> 1)))) holds
IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(s +* (Initialize (() .--> 1))),k)) = IC (Comput ((P +* I),(s +* (Initialize (() .--> 1))),k)) ) & IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(s +* (Initialize (() .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 1))) = card I & P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on s +* (Initialize (() .--> 1)) & LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ())),(s +* (Initialize (() .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize (() .--> 1))))) + 2 )

proof end;

theorem :: SCMFSA8A:39
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on s +* (Initialize (() .--> 1)) by Lm6;

theorem :: SCMFSA8A:40
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
IC (IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s)) = ((card I) + (card J)) + 1
proof end;

theorem :: SCMFSA8A:41
for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on Initialized s,P holds
IExec ((((I ";" (Goto ((card J) + 1))) ";" J) ";" ()),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
proof end;

theorem :: SCMFSA8A:42
for I being Program of SCM+FSA
for a being Int-Location
for k being Nat
for i being Instruction of SCM+FSA st not I destroys a & not i destroys a holds
not I +* (k,i) destroys a
proof end;

registration
let I, J be good preProgram of SCM+FSA;
cluster I +* J -> good ;
coherence
I +* J is good
proof end;
end;

theorem :: SCMFSA8A:43
for I being MacroInstruction of SCM+FSA
for k being Nat holds (Goto k) ";" I = (Macro (goto k)) ';' I
proof end;

theorem :: SCMFSA8A:44
for i, j being Nat holds IncAddr ((Goto i),j) = <%(goto (i + j))%>
proof end;

theorem :: SCMFSA8A:45
for I, J being NAT -defined the InstructionsF of SCM+FSA -valued Function st I c= J holds
for a being Int-Location st not J destroys a holds
not I destroys a
proof end;