environ
vocabularies HIDDEN, NUMBERS, AMI_1, SCMFSA_2, CARD_1, SCMFSA8B, SCMFSA8A, AMISTD_2, ARYTM_3, SUBSET_1, FUNCT_4, AMI_3, RELAT_1, TARSKI, XBOOLE_0, NAT_1, SCMFSA6A, FUNCT_1, XXREAL_0, VALUED_1, CARD_3, ARYTM_1, FSM_1, SF_MASTR, SCMFSA7B, CIRCUIT2, GRAPHSP, SCMFSA6B, SCMFSA_9, PBOOLE, PARTFUN1, EXTPRO_1, RELOC, SCMFSA6C, COMPOS_1, MEMSTR_0, AMISTD_1, TURING_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, AFINSQ_1, FUNCOP_1, FUNCT_4, CARD_3, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, COMPOS_2, EXTPRO_1, VALUED_1, PBOOLE, NAT_1, NAT_D, AMISTD_1, AMISTD_2, SCMFSA_2, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA7B, SCMFSA8A, SCMFSA8B, XXREAL_0, SCMFSA_M, SCMFSA_X;
definitions AFINSQ_1;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_4, SCMFSA_2, SCMFSA6A, GRFUNC_1, SCMFSA7B, SCMFSA8A, XBOOLE_0, XBOOLE_1, XREAL_1, ORDINAL1, XXREAL_0, VALUED_1, FUNCOP_1, PBOOLE, AFINSQ_1, PARTFUN1, RELAT_1, COMPOS_1, EXTPRO_1, MEMSTR_0, CARD_3, SCMFSA_M, FUNCT_7, SCMFSA_X, AMISTD_1, SCMFSA8C, COMPOS_2;
schemes NAT_1, FUNCT_7;
registrations RELSET_1, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SCMFSA6B, SCMFSA7B, SCMFSA8A, ORDINAL1, XBOOLE_0, FINSET_1, VALUED_1, FUNCT_4, VALUED_0, AFINSQ_1, FUNCOP_1, COMPOS_1, EXTPRO_1, MEMSTR_0, AMI_3, COMPOS_0, SCMFSA_M, SCMFSA6A;
constructors HIDDEN, XXREAL_0, SCMFSA6A, SF_MASTR, SCMFSA6B, SCMFSA8A, FUNCT_4, SCMFSA8B, AMISTD_2, RELSET_1, PRE_POLY, PBOOLE, SCMFSA7B, DOMAIN_1, AMISTD_1, MEMSTR_0, SCMFSA_M, FUNCT_7, SCMFSA_X, COMPOS_2, NAT_D;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SCMFSA6A, FUNCOP_1, COMPOS_1, EXTPRO_1, MEMSTR_0, CARD_3, SF_MASTR, SCMFSA_X, SCMFSA8B, FUNCT_7, COMPOS_2;
expansions AFINSQ_1, EXTPRO_1, MEMSTR_0;
set SA0 = Start-At (0,SCM+FSA);
canceled;
canceled;
canceled;
theorem Th2:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
really-closed MacroInstruction of
SCM+FSA for
s being
State of
SCM+FSA for
k being
Nat st
I is_halting_on s,
P &
k < LifeSpan (
(P +* I),
(Initialize s)) &
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 &
DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
(
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 &
DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )
theorem Th3:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
really-closed MacroInstruction of
SCM+FSA for
s being
State of
SCM+FSA st
I is_halting_on s,
P &
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 holds
CurInstr (
(P +* (while=0 (a,I))),
(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))))
= goto 0
theorem Th4:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
really-closed MacroInstruction of
SCM+FSA for
a being
read-write Int-Location st
I is_halting_on s,
P &
s . a = 0 holds
(
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for
k being
Nat st
k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )
definition
let s be
State of
SCM+FSA;
let I be
MacroInstruction of
SCM+FSA ;
let a be
read-write Int-Location;
let P be
Instruction-Sequence of
SCM+FSA;
deffunc H1(
Nat,
State of
SCM+FSA)
-> set =
Comput (
(P +* (while=0 (a,I))),
(Initialize $2),
((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize $2))) + 2));
deffunc H2(
Nat,
State of
SCM+FSA)
-> Element of
product (the_Values_of SCM+FSA) =
down H1($1,$2);
existence
ex b1 being sequence of (product (the_Values_of SCM+FSA)) st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b1 . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b1 . i)))) + 2)) ) )
uniqueness
for b1, b2 being sequence of (product (the_Values_of SCM+FSA)) st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b1 . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b1 . i)))) + 2)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b2 . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b2 . i)))) + 2)) ) holds
b1 = b2
end;
theorem Th7:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA for
k,
n being
Nat st
IC ((StepWhile=0 (a,I,P,s)) . k) = 0 &
(StepWhile=0 (a,I,P,s)) . k = Comput (
(P +* (while=0 (a,I))),
(Initialize s),
n) holds
(
(StepWhile=0 (a,I,P,s)) . k = Initialize ((StepWhile=0 (a,I,P,s)) . k) &
(StepWhile=0 (a,I,P,s)) . (k + 1) = Comput (
(P +* (while=0 (a,I))),
(Initialize s),
(n + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . k)))) + 2))) )
theorem Th8:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
really-closed MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ( for
k being
Nat holds
I is_halting_on (StepWhile=0 (a,I,P,s)) . k,
P +* (while=0 (a,I)) ) & ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & (
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
while=0 (
a,
I)
is_halting_on s,
P
theorem Th9:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
really-closed parahalting MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & (
((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies
f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
while=0 (
a,
I)
is_halting_on s,
P
theorem Th13:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
really-closed MacroInstruction of
SCM+FSA for
s being
State of
SCM+FSA for
k being
Nat st
I is_halting_on s,
P &
k < LifeSpan (
(P +* I),
(Initialize s)) &
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 &
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
(
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 3 &
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )
theorem Th14:
for
P being
Instruction-Sequence of
SCM+FSA for
a being
Int-Location for
I being
really-closed MacroInstruction of
SCM+FSA for
s being
State of
SCM+FSA st
I is_halting_on s,
P &
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 3 holds
CurInstr (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))))
= goto 0
theorem Th15:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I being
really-closed MacroInstruction of
SCM+FSA for
a being
read-write Int-Location st
I is_halting_on s,
P &
s . a > 0 holds
(
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for
k being
Nat st
k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
definition
let s be
State of
SCM+FSA;
let I be
MacroInstruction of
SCM+FSA ;
let a be
read-write Int-Location;
let P be
Instruction-Sequence of
SCM+FSA;
deffunc H1(
Nat,
State of
SCM+FSA)
-> set =
Comput (
(P +* (while>0 (a,I))),
(Initialize $2),
((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize $2))) + 2));
deffunc H2(
Nat,
State of
SCM+FSA)
-> Element of
product (the_Values_of SCM+FSA) =
down H1($1,$2);
existence
ex b1 being sequence of (product (the_Values_of SCM+FSA)) st
( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b1 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b1 . i)))) + 2)) ) )
uniqueness
for b1, b2 being sequence of (product (the_Values_of SCM+FSA)) st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b1 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b1 . i)))) + 2)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b2 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b2 . i)))) + 2)) ) holds
b1 = b2
end;
theorem Th18:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA for
k,
n being
Nat st
IC ((StepWhile>0 (a,I,P,s)) . k) = 0 &
(StepWhile>0 (a,I,P,s)) . k = Comput (
(P +* (while>0 (a,I))),
(Initialize s),
n) holds
(
(StepWhile>0 (a,I,P,s)) . k = Initialize ((StepWhile>0 (a,I,P,s)) . k) &
(StepWhile>0 (a,I,P,s)) . (k + 1) = Comput (
(P +* (while>0 (a,I))),
(Initialize s),
(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . k)))) + 2))) )
theorem Th19:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
really-closed MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ( for
k being
Nat holds
I is_halting_on (StepWhile>0 (a,I,P,s)) . k,
P +* (while>0 (a,I)) ) & ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
while>0 (
a,
I)
is_halting_on s,
P
theorem Th20:
for
P being
Instruction-Sequence of
SCM+FSA for
I being
really-closed parahalting MacroInstruction of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st ex
f being
Function of
(product (the_Values_of SCM+FSA)),
NAT st
for
k being
Nat holds
( (
f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) & (
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & (
((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies
f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
while>0 (
a,
I)
is_halting_on s,
P