:: Conditional branch macro instructions of SCM+FSA, Part I (preliminary)
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996 Association of Mizar Users
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
theorem :: SCMFSA8A:1
canceled;
theorem :: SCMFSA8A:2
canceled;
theorem Th3: :: SCMFSA8A:3
theorem Th4: :: SCMFSA8A:4
theorem Th5: :: SCMFSA8A:5
theorem Th6: :: SCMFSA8A:6
theorem Th7: :: SCMFSA8A:7
theorem :: SCMFSA8A:8
theorem Th9: :: SCMFSA8A:9
theorem Th10: :: SCMFSA8A:10
theorem :: SCMFSA8A:11
theorem Th12: :: SCMFSA8A:12
theorem Th13: :: SCMFSA8A:13
theorem Th14: :: SCMFSA8A:14
theorem Th16: :: SCMFSA8A:15
theorem Th16A: :: SCMFSA8A:16
theorem Th17: :: SCMFSA8A:17
theorem :: SCMFSA8A:18
canceled;
theorem :: SCMFSA8A:19
canceled;
theorem :: SCMFSA8A:20
canceled;
theorem :: SCMFSA8A:21
theorem Th22: :: SCMFSA8A:22
theorem Th23: :: SCMFSA8A:23
theorem Th24: :: SCMFSA8A:24
theorem Th25: :: SCMFSA8A:25
theorem Th26: :: SCMFSA8A:26
theorem Th27: :: SCMFSA8A:27
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
SCM+FSA ;
let P be
initial FinPartState of
SCM+FSA ;
assume A1:
P is_pseudo-closed_on s
;
func pseudo-LifeSpan s,
P -> Element of
NAT means :
Def5:
:: SCMFSA8A:def 5
(
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: :: SCMFSA8A:28
theorem :: SCMFSA8A:29
theorem :: SCMFSA8A:30
theorem Th31: :: SCMFSA8A:31
theorem Th32: :: SCMFSA8A:32
theorem Th33: :: SCMFSA8A:33
theorem :: SCMFSA8A:34
theorem Th35: :: SCMFSA8A:35
theorem Th36: :: SCMFSA8A:36
Lm2:
for s being State of SCM+FSA
for I being Program of SCM+FSA 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 :: SCMFSA8A:37
theorem :: SCMFSA8A:38
theorem :: SCMFSA8A:39
canceled;
theorem :: SCMFSA8A:40
canceled;
theorem Th41: :: SCMFSA8A:41
theorem Th42: :: SCMFSA8A:42
theorem Th43: :: SCMFSA8A:43
theorem Th44: :: SCMFSA8A:44
theorem Th45: :: SCMFSA8A:45
Lm3:
for I being Program of SCM+FSA
for s being State of SCM+FSA 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)) & s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & 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 :: SCMFSA8A:46
theorem :: SCMFSA8A:47
Lm4:
for I being Program of SCM+FSA
for s being State of SCM+FSA 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)) & s +* (Initialized (I ';' (Stop SCM+FSA ))) is halting & LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 1 )
theorem :: SCMFSA8A:48
canceled;
theorem :: SCMFSA8A:49
canceled;
theorem :: SCMFSA8A:50
canceled;
theorem :: SCMFSA8A:51
canceled;
theorem :: SCMFSA8A:52
canceled;
theorem :: SCMFSA8A:53
theorem :: SCMFSA8A:54
theorem :: SCMFSA8A:55
theorem :: SCMFSA8A:56
theorem :: SCMFSA8A:57
Lm5:
for I, J being Program of SCM+FSA
for s being State of SCM+FSA 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) & s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting & 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 :: SCMFSA8A:58
theorem :: SCMFSA8A:59
Lm6:
for I, J being Program of SCM+FSA
for s being State of SCM+FSA 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) & s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))) is halting & LifeSpan (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 2 )
theorem :: SCMFSA8A:60
theorem :: SCMFSA8A:61
theorem :: SCMFSA8A:62