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 0 ,SCM+FSA ;
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
begin
Lm1:
for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) & (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
Lm2:
for a being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = UsedIntLoc ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))
Lm3:
for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = UsedInt*Loc ((if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))
theorem
theorem
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:
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:
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s &
s . a = 0 holds
DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))
theorem Th24:
theorem Th25:
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
theorem
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:
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 (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((StepWhile=0 a,I,s) . k) ) );
theorem
theorem
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)))
begin
Lm4:
for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) & (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
Lm5:
for a being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = UsedIntLoc ((if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))
Lm6:
for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = UsedInt*Loc ((if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )))
theorem
theorem
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:
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:
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
I being
Program of
SCM+FSA st
I is_closed_on s &
I is_halting_on s &
s . a > 0 holds
DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))))
theorem Th37:
theorem Th38:
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:
theorem Th40:
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:
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 (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = 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 (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((StepWhile>0 a,I,s) . k) ) );
theorem
theorem Th42:
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:
theorem
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:
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:
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
begin
definition
let N,
result be
Int-Location ;
func Fusc_macro N,
result -> Program of
SCM+FSA 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 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