begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
set D = Int-Locations \/ FinSeq-Locations ;
set SAt = Start-At (insloc 0 );
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
begin
Lm1:
for a being Int-Location
for I being Program of 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 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 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
theorem
definition
let s be
State of ;
let a be
read-write Int-Location ;
let I be
Program of ;
pred ProperBodyWhile=0 a,
I,
s means :
Def1:
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:
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:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
for
s being
State of
for
a being
read-write Int-Location for
I being
Program of
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
theorem
definition
let s be
State of ;
let a be
read-write Int-Location ;
let I be
Program of ;
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:
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
for
a being
read-write Int-Location for
I being
Program of 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
theorem
for
s being
State of
for
a being
read-write Int-Location for
I being
Program of 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)))
begin
Lm4:
for a being Int-Location
for I being Program of 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 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 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
theorem
definition
let s be
State of ;
let a be
read-write Int-Location ;
let I be
Program of ;
pred ProperBodyWhile>0 a,
I,
s means :
Def4:
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:
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:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
for
s being
State of
for
a being
read-write Int-Location for
I being
Program of
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:
theorem Th40:
definition
let s be
State of ;
let a be
read-write Int-Location ;
let I be
Program of ;
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:
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
for
a being
read-write Int-Location for
I being
Program of 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
theorem Th42:
for
s being
State of
for
a being
read-write Int-Location for
I being
Program of 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:
theorem
Lm7:
for s being State of
for I being Program of st s . (intloc 0 ) = 1 holds
( I is_closed_on s iff I is_closed_on Initialize s )
Lm8:
for s being State of
for I being Program of 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:
for
s being
State of
for
a being
read-write Int-Location for
Ig being
good Program of 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:
for
s being
State of
for
a being
read-write Int-Location for
Ig being
good Program of 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
begin
definition
let N,
result be
Int-Location ;
func Fusc_macro N,
result -> Program of
equals
(((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 ;
;
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