Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Piotr Rudnicki
- Received June 3, 1998
- MML identifier: SCMFSA9A
- [
Mizar article,
MML identifier index
]
environ
vocabulary AMI_3, INT_1, FUNCT_1, RELAT_1, SQUARE_1, MATRIX_2, ARYTM_1, NAT_1,
ARYTM_3, AMI_1, SCMFSA_2, SCM_1, SF_MASTR, CAT_1, FINSUB_1, PROB_1,
TARSKI, FUNCOP_1, SCMFSA_4, BOOLE, SCMFSA8A, SCMFSA6A, SCMFSA7B,
SCMFSA8B, CARD_1, FUNCT_4, AMI_5, RELOC, SCMFSA_9, UNIALG_2, CARD_3,
SCMFSA6B, AMI_2, SCMFSA6C, SFMASTR1, PRE_FF, ABSVALUE, SCMFSA9A;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
FINSUB_1, FUNCOP_1, CARD_1, CARD_3, INT_1, NAT_1, ABIAN, RELAT_1,
FUNCT_1, FUNCT_2, FUNCT_4, CQC_SIM1, PRE_FF, PROB_1, STRUCT_0, AMI_1,
AMI_3, SCM_1, AMI_5, SCMFSA_2, SCMFSA_4, SCMFSA_5, SCMFSA6A, SCMFSA6B,
SF_MASTR, SCMFSA6C, SCMFSA_7, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA_9,
SFMASTR1, GROUP_1;
constructors ABIAN, SCMFSA_7, SCMFSA_9, SFMASTR1, SCMFSA6B, SCMFSA6C,
SCMFSA8A, SCMFSA8B, SCMFSA_5, CQC_SIM1, PRE_FF, SCM_1, AMI_5, REAL_1,
SCMFSA6A, NAT_1, PROB_1, MEMBERED;
clusters XREAL_0, FINSET_1, FUNCT_1, INT_1, ABIAN, FINSUB_1, AMI_1, SCMFSA_2,
SCMFSA_4, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B,
SCMFSA_9, SFMASTR1, FUNCOP_1, RELSET_1, NAT_1, FRAENKEL, MEMBERED,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Arithmetic preliminaries
reserve k, m, n for Nat,
i, j for Integer,
r for Real;
scheme MinPred { F(Nat)->Nat, P[set]} :
ex k st P[k] & for n st P[n] holds k <= n
provided
for k holds (F(k+1) < F(k) or P[k]);
theorem :: SCMFSA9A:1
n is odd iff ex k being Nat st n = 2*k+1;
theorem :: SCMFSA9A:2
for i being Integer st i <= r holds i <= [\ r /];
theorem :: SCMFSA9A:3 :: Div0:
0 < n implies 0 <= m qua Integer div n;
theorem :: SCMFSA9A:4 :: Div1:
0 < i & 1 < j implies i div j < i;
theorem :: SCMFSA9A:5 :: Div2:
m qua Integer div n = m div n &
m qua Integer mod n = m mod n;
begin :: SCM+FSA preliminaries
reserve l for Instruction-Location of SCM+FSA,
i for Instruction of SCM+FSA;
theorem :: SCMFSA9A:6 :: LifeSpan0:
for N being non empty with_non-empty_elements set,
S being halting IC-Ins-separated definite
(non empty non void AMI-Struct over N),
s being State of S, k being Nat
st CurInstr((Computation s).k) = halt S
holds (Computation s).(LifeSpan s) = (Computation s).k;
theorem :: SCMFSA9A:7 :: singleUsed
UsedIntLoc (l .--> i) = UsedIntLoc i;
theorem :: SCMFSA9A:8 :: singleUsedF:
UsedInt*Loc (l .--> i) = UsedInt*Loc i;
theorem :: SCMFSA9A:9 :: StopUsed:
UsedIntLoc SCM+FSA-Stop = {};
theorem :: SCMFSA9A:10 :: StopUsedF:
UsedInt*Loc SCM+FSA-Stop = {};
theorem :: SCMFSA9A:11 :: GotoUsed:
UsedIntLoc Goto l = {};
theorem :: SCMFSA9A:12 :: GotoUsedF:
UsedInt*Loc Goto l = {};
reserve s, s1, s2 for State of SCM+FSA,
a for read-write Int-Location,
b for Int-Location,
I, J for Macro-Instruction,
Ig for good Macro-Instruction,
i, j, k, m, n for Nat;
:: set D = Int-Locations U FinSeq-Locations;
:: set SAt = Start-At insloc 0;
:: set IL = the Instruction-Locations of SCM+FSA;
theorem :: SCMFSA9A:13 :: eifUsed:
UsedIntLoc if=0(b, I, J) = {b} \/ UsedIntLoc I \/ UsedIntLoc J;
theorem :: SCMFSA9A:14 :: eifUsedF:
for a being Int-Location
holds UsedInt*Loc if=0(a, I, J) = UsedInt*Loc I \/ UsedInt*Loc J;
theorem :: SCMFSA9A:15 :: ifUsed:
UsedIntLoc if>0(b, I, J) = {b} \/ UsedIntLoc I \/ UsedIntLoc J;
theorem :: SCMFSA9A:16 :: ifUsedF:
UsedInt*Loc if>0(b, I, J) = UsedInt*Loc I \/ UsedInt*Loc J;
begin
theorem :: SCMFSA9A:17 :: ewhileUsed:
UsedIntLoc while=0(b, I) = {b} \/ UsedIntLoc I;
theorem :: SCMFSA9A:18 :: ewhileUsedF:
UsedInt*Loc while=0(b, I) = UsedInt*Loc I;
definition
let s be State of SCM+FSA, a be read-write Int-Location,
I be Macro-Instruction;
pred ProperBodyWhile=0 a, I, s means
:: SCMFSA9A:def 1
for k being 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
:: SCMFSA9A:def 2
ex f being Function of product the Object-Kind of SCM+FSA, NAT
st for k being 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;
theorem :: SCMFSA9A:19 :: eParaProper:
for I being parahalting Macro-Instruction holds ProperBodyWhile=0 a, I, s;
theorem :: SCMFSA9A:20 :: SCMFSA_9:24, corrected
ProperBodyWhile=0 a, I, s & WithVariantWhile=0 a, I, s
implies while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s;
theorem :: SCMFSA9A:21 :: SCMFSA_9:25, corrected
for I being parahalting Macro-Instruction
st WithVariantWhile=0 a, I, s
holds while=0(a,I) is_halting_on s & while=0(a,I) is_closed_on s;
theorem :: SCMFSA9A:22 :: based on SCMFSA_9:10
while=0(a, I) +* SAt c= s & s.a <> 0
implies LifeSpan s = 4 & for k being Nat holds (Computation s).k | D = s | D;
theorem :: SCMFSA9A:23 :: based on SCMFSA_9:22
I is_closed_on s & I is_halting_on s & s.a = 0
implies
(Computation (s +* (while=0(a,I) +* Start-At insloc 0))).
(LifeSpan (s +* (I +* Start-At insloc 0)) + 3) | D
= (Computation (s +* (I +* Start-At insloc 0))).
(LifeSpan (s +* (I +* Start-At insloc 0))) | D;
theorem :: SCMFSA9A:24 :: Step_eq0_0:
(StepWhile=0(a, I, s).k).a <> 0
implies StepWhile=0(a, I, s).(k+1) | D = StepWhile=0(a, I, s).k | D;
theorem :: SCMFSA9A:25 :: Step_eq0_1:
( 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
implies StepWhile=0(a, I, s).(k+1) | D
= IExec(I, StepWhile=0(a, I, s).k) | D;
theorem :: SCMFSA9A:26 :: eGoodStep0:
(ProperBodyWhile=0 a, Ig, s or Ig is parahalting) &
s.intloc 0 = 1
implies for k holds StepWhile=0(a, Ig, s).k.intloc 0 = 1;
theorem :: SCMFSA9A:27 :: eSW12:
ProperBodyWhile=0 a, I, s1 & s1 | D = s2 | D implies
for k holds StepWhile=0(a, I, s1).k | D = StepWhile=0(a, I, s2).k | D;
definition
let s be State of SCM+FSA,
a be read-write Int-Location,
I be Macro-Instruction;
assume that
ProperBodyWhile=0 a, I, s or I is parahalting and
WithVariantWhile=0 a, I, s;
func ExitsAtWhile=0(a, I, s) -> Nat means
:: SCMFSA9A:def 3
ex k being Nat st
it = k &
(StepWhile=0(a, I, s).k).a <> 0 &
(for i being Nat st (StepWhile=0(a, I, s).i).a <> 0 holds k <= i) &
(Computation (s +* (while=0(a, I) +* SAt))).
(LifeSpan (s +* (while=0(a, I) +* SAt))) | D
= StepWhile=0(a, I, s).k | D;
end;
theorem :: SCMFSA9A:28 :: IE_while_ne0:
s.intloc 0 = 1 & s.a <> 0 implies IExec(while=0(a, I), s) | D = s | D;
theorem :: SCMFSA9A:29 :: IE_while_eq0:
(ProperBodyWhile=0 a, I, Initialize s or I is parahalting) &
WithVariantWhile=0 a, I, Initialize s
implies IExec(while=0(a, I), s) | D
= StepWhile=0(a, I, Initialize s).ExitsAtWhile=0(a, I, Initialize s) | D
;
begin
theorem :: SCMFSA9A:30 :: whileUsed:
UsedIntLoc while>0(b, I) = {b} \/ UsedIntLoc I;
theorem :: SCMFSA9A:31 :: whileUsedF:
UsedInt*Loc while>0(b, I) = UsedInt*Loc I;
definition
let s be State of SCM+FSA, a be read-write Int-Location,
I be Macro-Instruction;
pred ProperBodyWhile>0 a, I, s means
:: SCMFSA9A:def 4
for k being 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
:: SCMFSA9A:def 5
ex f being Function of product the Object-Kind of SCM+FSA, NAT
st for k being 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;
theorem :: SCMFSA9A:32 :: ParaProper:
for I being parahalting Macro-Instruction holds ProperBodyWhile>0 a, I, s;
theorem :: SCMFSA9A:33 :: SCMFSA_9:42, corrected
ProperBodyWhile>0 a, I, s & WithVariantWhile>0 a, I, s
implies while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s;
theorem :: SCMFSA9A:34 :: SCMFSA_9:43, corrected
for I being parahalting Macro-Instruction
st WithVariantWhile>0 a, I, s
holds while>0(a,I) is_halting_on s & while>0(a,I) is_closed_on s;
theorem :: SCMFSA9A:35 :: based on SCMFSA_9:32
while>0(a, I) +* SAt c= s & s.a <= 0
implies LifeSpan s = 4 & for k being Nat holds (Computation s).k | D = s | D;
theorem :: SCMFSA9A:36 :: based on SCMFSA_9:36
I is_closed_on s & I is_halting_on s & s.a > 0
implies
(Computation (s +* (while>0(a,I) +* Start-At insloc 0))).
(LifeSpan (s +* (I +* Start-At insloc 0)) + 3) | D
= (Computation (s +* (I +* Start-At insloc 0))).
(LifeSpan (s +* (I +* Start-At insloc 0))) | D;
theorem :: SCMFSA9A:37 :: Step_gt0_0:
(StepWhile>0(a, I, s).k).a <= 0
implies StepWhile>0(a, I, s).(k+1) | D = StepWhile>0(a, I, s).k | D;
theorem :: SCMFSA9A:38 :: Step_gt0_1:
( 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
implies StepWhile>0(a, I, s).(k+1) | D
= IExec(I, StepWhile>0(a, I, s).k) | D;
theorem :: SCMFSA9A:39 :: GoodStep0:
(ProperBodyWhile>0 a, Ig, s or Ig is parahalting) &
s.intloc 0 = 1
implies for k holds StepWhile>0(a, Ig, s).k.intloc 0 = 1;
theorem :: SCMFSA9A:40 :: SW12:
ProperBodyWhile>0 a, I, s1 & s1 | D = s2 | D implies
for k holds StepWhile>0(a, I, s1).k | D = StepWhile>0(a, I, s2).k | D;
definition
let s be State of SCM+FSA,
a be read-write Int-Location,
I be Macro-Instruction;
assume that
ProperBodyWhile>0 a, I, s or I is parahalting and
WithVariantWhile>0 a, I, s;
func ExitsAtWhile>0(a, I, s) -> Nat means
:: SCMFSA9A:def 6
ex k being Nat st
it = k &
(StepWhile>0(a, I, s).k).a <= 0 &
(for i being Nat st (StepWhile>0(a, I, s).i).a <= 0 holds k <= i) &
(Computation (s +* (while>0(a, I) +* SAt))).
(LifeSpan (s +* (while>0(a, I) +* SAt))) | D
= StepWhile>0(a, I, s).k | D;
end;
theorem :: SCMFSA9A:41 :: IE_while_le0:
s.intloc 0 = 1 & s.a <= 0 implies IExec(while>0(a, I), s) | D = s | D;
theorem :: SCMFSA9A:42 :: IE_while_gt0:
(ProperBodyWhile>0 a, I, Initialize s or I is parahalting) &
WithVariantWhile>0 a, I, Initialize s
implies IExec(while>0(a, I), s) | D
= StepWhile>0(a, I, Initialize s).ExitsAtWhile>0(a, I, Initialize s) | D
;
theorem :: SCMFSA9A:43
StepWhile>0(a, I, s).k.a <= 0 implies
for n being Nat st k <= n
holds StepWhile>0(a, I, s).n | D = StepWhile>0(a, I, s).k | D;
theorem :: SCMFSA9A:44
s1 | D = s2 | D & ProperBodyWhile>0 a, I, s1
implies ProperBodyWhile>0 a, I, s2;
theorem :: SCMFSA9A:45
s.intloc 0 = 1 & ProperBodyWhile>0 a, Ig, s & WithVariantWhile>0 a, Ig, s
implies
for i, j 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 &
StepWhile>0(a, Ig, s).i | D <> StepWhile>0(a, Ig, s).j | D;
definition
let f be Function of product the Object-Kind of SCM+FSA, NAT;
attr f is on_data_only means
:: SCMFSA9A:def 7
for s1, s2 st s1 | D = s2 | D holds f.s1 = f.s2;
end;
theorem :: SCMFSA9A:46
s.intloc 0 = 1 & ProperBodyWhile>0 a, Ig, s & WithVariantWhile>0 a, Ig, s
implies ex f being Function of product the Object-Kind of SCM+FSA, NAT st
f is on_data_only &
for k being 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
s1.intloc 0 = 1 & s1 | D = s2 | D &
ProperBodyWhile>0 a, Ig, s1 & WithVariantWhile>0 a, Ig, s1
implies WithVariantWhile>0 a, Ig, s2;
begin :: fusc using while>0, bottom-up
definition
let N, result be Int-Location;
:: set next = 1-stRWNotIn {N, result};
:: set aux = 2-ndRWNotIn {N, result};
:: set rem2 = 3-rdRWNotIn {N, result};
:: while and if do not allocate memory, no need to save anything
func Fusc_macro ( N, result ) -> Macro-Instruction equals
:: SCMFSA9A:def 8
SubFrom(result, result) ';'
(next := intloc 0) ';'
(aux := N) ';'
while>0 ( aux,
rem2 := 2 ';'
Divide(aux, rem2) ';'
if=0 ( rem2,
Macro AddTo(next, result),
Macro AddTo(result, next)
)
);
end;
theorem :: SCMFSA9A:48
for N, result being read-write Int-Location
st N <> result
for n being Nat st n = s.N
holds IExec(Fusc_macro(N, result), s).result = Fusc n &
IExec(Fusc_macro(N, result), s).N = n;
Back to top