:: The { \bf while } macro instructions of SCM+FSA, Part { II }
:: by Piotr Rudnicki
::
:: Received June 3, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: SCMFSA9A:1
canceled;
theorem :: SCMFSA9A:2
canceled;
theorem :: SCMFSA9A:3
canceled;
theorem :: SCMFSA9A:4
canceled;
theorem :: SCMFSA9A:5
canceled;
theorem :: SCMFSA9A:6
canceled;
theorem Th7: :: SCMFSA9A:7
theorem Th8: :: SCMFSA9A:8
theorem Th9: :: SCMFSA9A:9
theorem Th10: :: SCMFSA9A:10
theorem Th11: :: SCMFSA9A:11
theorem Th12: :: SCMFSA9A:12
set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At (insloc 0 );
set IL = NAT ;
theorem Th13: :: SCMFSA9A:13
theorem Th14: :: SCMFSA9A:14
theorem Th15: :: SCMFSA9A:15
theorem Th16: :: SCMFSA9A:16
Lm1:
for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) & (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4)) )
Lm2:
for a being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedIntLoc ((if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))
Lm3:
for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedInt*Loc ((if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))
theorem :: SCMFSA9A:17
theorem :: SCMFSA9A:18
definition
let s be
State of
SCM+FSA ;
let a be
read-write Int-Location ;
let I be
Program of
SCM+FSA ;
pred ProperBodyWhile=0 a,
I,
s means :
Def1:
:: SCMFSA9A:def 1
for
k being
Element of
NAT st
((StepWhile=0 a,I,s) . k) . a = 0 holds
(
I is_closed_on (StepWhile=0 a,I,s) . k &
I is_halting_on (StepWhile=0 a,I,s) . k );
pred WithVariantWhile=0 a,
I,
s means :
Def2:
:: SCMFSA9A:def 2
ex
f being
Function of
product the
Object-Kind of
SCM+FSA ,
NAT st
for
k being
Element of
NAT holds
(
f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or
((StepWhile=0 a,I,s) . k) . a <> 0 );
end;
:: deftheorem Def1 defines ProperBodyWhile=0 SCMFSA9A:def 1 :
:: deftheorem Def2 defines WithVariantWhile=0 SCMFSA9A:def 2 :
theorem Th19: :: SCMFSA9A:19
theorem Th20: :: SCMFSA9A:20
theorem Th21: :: SCMFSA9A:21
theorem Th22: :: SCMFSA9A:22
theorem Th23: :: SCMFSA9A:23
theorem Th24: :: SCMFSA9A:24
theorem Th25: :: SCMFSA9A:25
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA for
k being
Element of
NAT st ( (
I is_halting_on Initialize ((StepWhile=0 a,I,s) . k) &
I is_closed_on Initialize ((StepWhile=0 a,I,s) . k) ) or
I is
parahalting ) &
((StepWhile=0 a,I,s) . k) . a = 0 &
((StepWhile=0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile=0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile=0 a,I,s) . k))
theorem :: SCMFSA9A:26
theorem :: SCMFSA9A:27
definition
let s be
State of
SCM+FSA ;
let a be
read-write Int-Location ;
let I be
Program of
SCM+FSA ;
assume that A1:
(
ProperBodyWhile=0 a,
I,
s or
I is
parahalting )
and A2:
WithVariantWhile=0 a,
I,
s
;
func ExitsAtWhile=0 a,
I,
s -> Element of
NAT means :
Def3:
:: SCMFSA9A:def 3
ex
k being
Element of
NAT st
(
it = k &
((StepWhile=0 a,I,s) . k) . a <> 0 & ( for
i being
Element of
NAT st
((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) &
DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) );
existence
ex b1, k being Element of NAT st
( b1 = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) )
uniqueness
for b1, b2 being Element of NAT st ex k being Element of NAT st
( b1 = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) ) & ex k being Element of NAT st
( b2 = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) ) holds
b1 = b2
end;
:: deftheorem Def3 defines ExitsAtWhile=0 SCMFSA9A:def 3 :
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st (
ProperBodyWhile=0 a,
I,
s or
I is
parahalting ) &
WithVariantWhile=0 a,
I,
s holds
for
b4 being
Element of
NAT holds
(
b4 = ExitsAtWhile=0 a,
I,
s iff ex
k being
Element of
NAT st
(
b4 = k &
((StepWhile=0 a,I,s) . k) . a <> 0 & ( for
i being
Element of
NAT st
((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) &
DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) ) );
theorem :: SCMFSA9A:28
theorem :: SCMFSA9A:29
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st (
ProperBodyWhile=0 a,
I,
Initialize s or
I is
parahalting ) &
WithVariantWhile=0 a,
I,
Initialize s holds
DataPart (IExec (while=0 a,I),s) = DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s)))
Lm4:
for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) & (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4)) )
Lm5:
for a being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedIntLoc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))
Lm6:
for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) = UsedInt*Loc ((if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))))
theorem :: SCMFSA9A:30
theorem :: SCMFSA9A:31
definition
let s be
State of
SCM+FSA ;
let a be
read-write Int-Location ;
let I be
Program of
SCM+FSA ;
pred ProperBodyWhile>0 a,
I,
s means :
Def4:
:: SCMFSA9A:def 4
for
k being
Element of
NAT st
((StepWhile>0 a,I,s) . k) . a > 0 holds
(
I is_closed_on (StepWhile>0 a,I,s) . k &
I is_halting_on (StepWhile>0 a,I,s) . k );
pred WithVariantWhile>0 a,
I,
s means :
Def5:
:: SCMFSA9A:def 5
ex
f being
Function of
product the
Object-Kind of
SCM+FSA ,
NAT st
for
k being
Element of
NAT holds
(
f . ((StepWhile>0 a,I,s) . (k + 1)) < f . ((StepWhile>0 a,I,s) . k) or
((StepWhile>0 a,I,s) . k) . a <= 0 );
end;
:: deftheorem Def4 defines ProperBodyWhile>0 SCMFSA9A:def 4 :
:: deftheorem Def5 defines WithVariantWhile>0 SCMFSA9A:def 5 :
theorem Th32: :: SCMFSA9A:32
theorem Th33: :: SCMFSA9A:33
theorem Th34: :: SCMFSA9A:34
theorem Th35: :: SCMFSA9A:35
theorem Th36: :: SCMFSA9A:36
theorem Th37: :: SCMFSA9A:37
theorem Th38: :: SCMFSA9A:38
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA for
k being
Element of
NAT st ( (
I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) &
I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or
I is
parahalting ) &
((StepWhile>0 a,I,s) . k) . a > 0 &
((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k))
theorem Th39: :: SCMFSA9A:39
theorem Th40: :: SCMFSA9A:40
definition
let s be
State of
SCM+FSA ;
let a be
read-write Int-Location ;
let I be
Program of
SCM+FSA ;
assume that A1:
(
ProperBodyWhile>0 a,
I,
s or
I is
parahalting )
and A2:
WithVariantWhile>0 a,
I,
s
;
func ExitsAtWhile>0 a,
I,
s -> Element of
NAT means :
Def6:
:: SCMFSA9A:def 6
ex
k being
Element of
NAT st
(
it = k &
((StepWhile>0 a,I,s) . k) . a <= 0 & ( for
i being
Element of
NAT st
((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) &
DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) );
existence
ex b1, k being Element of NAT st
( b1 = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) )
uniqueness
for b1, b2 being Element of NAT st ex k being Element of NAT st
( b1 = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) ) & ex k being Element of NAT st
( b2 = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) ) holds
b1 = b2
end;
:: deftheorem Def6 defines ExitsAtWhile>0 SCMFSA9A:def 6 :
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st (
ProperBodyWhile>0 a,
I,
s or
I is
parahalting ) &
WithVariantWhile>0 a,
I,
s holds
for
b4 being
Element of
NAT holds
(
b4 = ExitsAtWhile>0 a,
I,
s iff ex
k being
Element of
NAT st
(
b4 = k &
((StepWhile>0 a,I,s) . k) . a <= 0 & ( for
i being
Element of
NAT st
((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) &
DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) ) );
theorem :: SCMFSA9A:41
theorem Th42: :: SCMFSA9A:42
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st (
ProperBodyWhile>0 a,
I,
Initialize s or
I is
parahalting ) &
WithVariantWhile>0 a,
I,
Initialize s holds
DataPart (IExec (while>0 a,I),s) = DataPart ((StepWhile>0 a,I,(Initialize s)) . (ExitsAtWhile>0 a,I,(Initialize s)))
theorem Th43: :: SCMFSA9A:43
theorem :: SCMFSA9A:44
Lm7:
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
( I is_closed_on s iff I is_closed_on Initialize s )
Lm8:
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0 ) = 1 holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialize s & I is_halting_on Initialize s ) )
theorem Th45: :: SCMFSA9A:45
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
Ig being
good Program of
SCM+FSA st
s . (intloc 0 ) = 1 &
ProperBodyWhile>0 a,
Ig,
s &
WithVariantWhile>0 a,
Ig,
s holds
for
i,
j being
Element of
NAT st
i <> j &
i <= ExitsAtWhile>0 a,
Ig,
s &
j <= ExitsAtWhile>0 a,
Ig,
s holds
(
(StepWhile>0 a,Ig,s) . i <> (StepWhile>0 a,Ig,s) . j &
DataPart ((StepWhile>0 a,Ig,s) . i) <> DataPart ((StepWhile>0 a,Ig,s) . j) )
:: deftheorem Def7 defines on_data_only SCMFSA9A:def 7 :
theorem Th46: :: SCMFSA9A:46
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
Ig being
good Program of
SCM+FSA st
s . (intloc 0 ) = 1 &
ProperBodyWhile>0 a,
Ig,
s &
WithVariantWhile>0 a,
Ig,
s holds
ex
f being
Function of
product the
Object-Kind of
SCM+FSA ,
NAT st
(
f is
on_data_only & ( for
k being
Element of
NAT holds
(
f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or
((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )
theorem :: SCMFSA9A:47
definition
let N,
result be
Int-Location ;
func Fusc_macro N,
result -> Program of
SCM+FSA equals :: SCMFSA9A:def 8
(((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)) ';' (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))));
correctness
coherence
(((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)) ';' (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result})))))) is Program of SCM+FSA ;
;
end;
:: deftheorem defines Fusc_macro SCMFSA9A:def 8 :
for
N,
result being
Int-Location holds
Fusc_macro N,
result = (((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0 ))) ';' ((2 -ndRWNotIn {N,result}) := N)) ';' (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))));
theorem :: SCMFSA9A:48