:: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA}
:: by Noriko Asamoto
::
:: Received October 29, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem :: SCMFSA8C:1
canceled;
theorem Th2: :: SCMFSA8C:2
theorem :: SCMFSA8C:3
canceled;
theorem :: SCMFSA8C:4
canceled;
theorem :: SCMFSA8C:5
canceled;
theorem :: SCMFSA8C:6
canceled;
theorem :: SCMFSA8C:7
canceled;
theorem Th8: :: SCMFSA8C:8
theorem Th9: :: SCMFSA8C:9
theorem :: SCMFSA8C:10
canceled;
theorem :: SCMFSA8C:11
canceled;
theorem Th12: :: SCMFSA8C:12
theorem Th13: :: SCMFSA8C:13
theorem Th14: :: SCMFSA8C:14
theorem Th15: :: SCMFSA8C:15
theorem Th16: :: SCMFSA8C:16
theorem Th17: :: SCMFSA8C:17
theorem Th18: :: SCMFSA8C:18
theorem Th19: :: SCMFSA8C:19
theorem Th20: :: SCMFSA8C:20
theorem :: SCMFSA8C:21
theorem Th22: :: SCMFSA8C:22
theorem :: SCMFSA8C:23
theorem Th24: :: SCMFSA8C:24
theorem :: SCMFSA8C:25
theorem Th26: :: SCMFSA8C:26
theorem Th27: :: SCMFSA8C:27
theorem Th28: :: SCMFSA8C:28
theorem :: SCMFSA8C:29
theorem :: SCMFSA8C:30
theorem Th31: :: SCMFSA8C:31
theorem Th32: :: SCMFSA8C:32
theorem Th33: :: SCMFSA8C:33
theorem :: SCMFSA8C:34
theorem Th35: :: SCMFSA8C:35
theorem Th36: :: SCMFSA8C:36
theorem Th37: :: SCMFSA8C:37
theorem Th38: :: SCMFSA8C:38
theorem Th39: :: SCMFSA8C:39
theorem :: SCMFSA8C:40
theorem :: SCMFSA8C:41
theorem Th42: :: SCMFSA8C:42
theorem Th43: :: SCMFSA8C:43
theorem Th44: :: SCMFSA8C:44
theorem Th45: :: SCMFSA8C:45
theorem Th46: :: SCMFSA8C:46
Lm1:
now
let s be
State of
SCM+FSA ;
:: thesis: for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )let I be
Program of
SCM+FSA ;
:: thesis: ( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )A1:
ProgramPart (Initialized I) = I
by SCMFSA6A:33;
hereby :: thesis: ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) )
assume A2:
Initialized I is_pseudo-closed_on s
;
:: thesis: ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )set k =
pseudo-LifeSpan s,
(Initialized I);
(
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart (Initialized I))) & ( for
n being
Element of
NAT st
n < pseudo-LifeSpan s,
(Initialized I) holds
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),n) in dom (Initialized I) ) )
by A2, SCMFSA8A:def 5;
then
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart (Initialized I)))
by Th16;
then A3:
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Initialized I))) = insloc (card (ProgramPart I))
by A1, AMI_1:105;
then A5:
for
n being
Element of
NAT st not
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),n) in dom I holds
pseudo-LifeSpan s,
(Initialized I) <= n
;
thus
I is_pseudo-closed_on Initialize s
by A3, A4, SCMFSA8A:def 3;
:: thesis: pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),Ihence
pseudo-LifeSpan s,
(Initialized I) = pseudo-LifeSpan (Initialize s),
I
by A3, A5, SCMFSA8A:def 5;
:: thesis: verum
end;
assume A6:
I is_pseudo-closed_on Initialize s
;
:: thesis: ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )set k =
pseudo-LifeSpan (Initialize s),
I;
(
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart I)) & ( for
n being
Element of
NAT st
n < pseudo-LifeSpan (Initialize s),
I holds
IC (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),n) in dom I ) )
by A6, SCMFSA8A:def 5;
then
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart I))
by Th16;
then A7:
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (Initialize s),I)) = insloc (card (ProgramPart (Initialized I)))
by A1, AMI_1:105;
then A9:
for
n being
Element of
NAT st not
IC (Computation (s +* ((Initialized I) +* (Start-At (insloc 0 )))),n) in dom (Initialized I) holds
pseudo-LifeSpan (Initialize s),
I <= n
;
thus
Initialized I is_pseudo-closed_on s
by A7, A8, SCMFSA8A:def 3;
:: thesis: pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),Ihence
pseudo-LifeSpan s,
(Initialized I) = pseudo-LifeSpan (Initialize s),
I
by A7, A9, SCMFSA8A:def 5;
:: thesis: verum
end;
theorem :: SCMFSA8C:47
theorem :: SCMFSA8C:48
theorem :: SCMFSA8C:49
theorem Th50: :: SCMFSA8C:50
theorem Th51: :: SCMFSA8C:51
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I +* (Start-At (insloc 0 )) c= s1 &
I is_pseudo-closed_on s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated I,n) c= s2 &
IC s2 = insloc n &
DataPart s1 = DataPart s2 holds
( ( for
i being
Element of
NAT st
i < pseudo-LifeSpan s1,
I holds
IncAddr (CurInstr (Computation s1,i)),
n = CurInstr (Computation s2,i) ) & ( for
i being
Element of
NAT st
i <= pseudo-LifeSpan s1,
I holds
(
(IC (Computation s1,i)) + n = IC (Computation s2,i) &
DataPart (Computation s1,i) = DataPart (Computation s2,i) ) ) )
theorem Th52: :: SCMFSA8C:52
theorem Th53: :: SCMFSA8C:53
theorem Th54: :: SCMFSA8C:54
theorem Th55: :: SCMFSA8C:55
theorem Th56: :: SCMFSA8C:56
theorem Th57: :: SCMFSA8C:57
theorem Th58: :: SCMFSA8C:58
theorem Th59: :: SCMFSA8C:59
theorem :: SCMFSA8C:60
theorem Th61: :: SCMFSA8C:61
theorem Th62: :: SCMFSA8C:62
theorem Th63: :: SCMFSA8C:63
theorem Th64: :: SCMFSA8C:64
theorem Th65: :: SCMFSA8C:65
theorem Th66: :: SCMFSA8C:66
theorem :: SCMFSA8C:67
theorem Th68: :: SCMFSA8C:68
theorem Th69: :: SCMFSA8C:69
theorem Th70: :: SCMFSA8C:70
theorem :: SCMFSA8C:71
theorem Th72: :: SCMFSA8C:72
theorem Th73: :: SCMFSA8C:73
theorem :: SCMFSA8C:74
theorem :: SCMFSA8C:75
theorem :: SCMFSA8C:76
theorem Th77: :: SCMFSA8C:77
theorem Th78: :: SCMFSA8C:78
theorem :: SCMFSA8C:79
theorem :: SCMFSA8C:80
theorem Th81: :: SCMFSA8C:81
theorem Th82: :: SCMFSA8C:82
theorem :: SCMFSA8C:83
theorem :: SCMFSA8C:84
theorem Th85: :: SCMFSA8C:85
theorem Th86: :: SCMFSA8C:86
theorem Th87: :: SCMFSA8C:87
theorem Th88: :: SCMFSA8C:88
theorem Th89: :: SCMFSA8C:89
theorem Th90: :: SCMFSA8C:90
theorem Th91: :: SCMFSA8C:91
theorem Th92: :: SCMFSA8C:92
theorem Th93: :: SCMFSA8C:93
theorem Th94: :: SCMFSA8C:94
theorem Th95: :: SCMFSA8C:95
theorem Th96: :: SCMFSA8C:96
theorem :: SCMFSA8C:97
theorem Th98: :: SCMFSA8C:98
theorem Th99: :: SCMFSA8C:99
theorem Th100: :: SCMFSA8C:100
theorem Th101: :: SCMFSA8C:101
theorem :: SCMFSA8C:102
canceled;
theorem Th103: :: SCMFSA8C:103
:: deftheorem SCMFSA8C:def 1 :
canceled;
:: deftheorem SCMFSA8C:def 2 :
canceled;
:: deftheorem SCMFSA8C:def 3 :
canceled;
:: deftheorem defines loop SCMFSA8C:def 4 :
theorem :: SCMFSA8C:104
canceled;
theorem :: SCMFSA8C:105
theorem :: SCMFSA8C:106
canceled;
theorem Th107: :: SCMFSA8C:107
theorem :: SCMFSA8C:108
canceled;
theorem Th109: :: SCMFSA8C:109
theorem Th110: :: SCMFSA8C:110
Lm3:
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
( CurInstr (Computation (s +* ((loop I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = goto (insloc 0 ) & ( for m being Element of NAT st m <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
CurInstr (Computation (s +* ((loop I) +* (Start-At (insloc 0 )))),m) <> halt SCM+FSA ) )
theorem :: SCMFSA8C:111
theorem :: SCMFSA8C:112
theorem Th113: :: SCMFSA8C:113
theorem :: SCMFSA8C:114
definition
let a be
Int-Location ;
let I be
Program of
SCM+FSA ;
func Times a,
I -> Program of
SCM+FSA equals :: SCMFSA8C:def 5
if>0 a,
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))),
(Stop SCM+FSA );
correctness
coherence
if>0 a,(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))),(Stop SCM+FSA ) is Program of SCM+FSA ;
;
end;
:: deftheorem defines Times SCMFSA8C:def 5 :
theorem Th115: :: SCMFSA8C:115
theorem Th116: :: SCMFSA8C:116
theorem Th117: :: SCMFSA8C:117
theorem :: SCMFSA8C:118
theorem :: SCMFSA8C:119
theorem :: SCMFSA8C:120
theorem :: SCMFSA8C:121
theorem Th122: :: SCMFSA8C:122
for
s being
State of
SCM+FSA for
I being
parahalting good Program of
SCM+FSA for
a being
read-write Int-Location st
I does_not_destroy a &
s . (intloc 0 ) = 1 &
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
k being
Element of
NAT st
(
s2 = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) &
k = (LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 &
(Computation s2,k) . a = (s . a) - 1 &
(Computation s2,k) . (intloc 0 ) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for
f being
FinSeq-Location holds
(Computation s2,k) . f = (IExec I,s) . f ) &
IC (Computation s2,k) = insloc 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
theorem Th123: :: SCMFSA8C:123
theorem Th124: :: SCMFSA8C:124
theorem :: SCMFSA8C:125