:: Externally Programmed Machines
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received June 30, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, CARD_1,
FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, FSM_1, GLIB_000, CIRCUIT2, NAT_1,
ARYTM_3, XXREAL_0, MSUALG_1, TURING_1, PARTFUN1, ZFMISC_1, GRAPHSP,
ARYTM_1, AMI_1, PBOOLE, EXTPRO_1, GROUP_9, COMPOS_1, MEMSTR_0, GOBRD13,
QUANTAL1, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, SETFAM_1,
ORDINAL1, CARD_1, PBOOLE, NUMBERS, FUNCT_7, CARD_3, XCMPLX_0, RELAT_1,
FUNCT_1, PARTFUN1, NAT_1, FUNCOP_1, FUNCT_4, FINSEQ_1, FUNCT_2, DOMAIN_1,
MEASURE6, STRUCT_0, XXREAL_0, MEMSTR_0, COMPOS_0, COMPOS_1;
constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, FUNCT_7, GRAPH_2,
RELSET_1, PRE_POLY, PBOOLE, COMPOS_1, MEMSTR_0, MEASURE6, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, XREAL_0, CARD_3, STRUCT_0, INT_1, COMPOS_1, MEMSTR_0,
CARD_1, MEASURE6, COMPOS_0, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions FUNCT_1, COMPOS_1, MEMSTR_0;
equalities STRUCT_0, FUNCOP_1, COMPOS_1, MEMSTR_0, CARD_3, COMPOS_0;
expansions STRUCT_0, COMPOS_1;
theorems ZFMISC_1, FUNCT_2, TARSKI, NAT_1, CARD_3, FUNCT_4, FUNCOP_1, FUNCT_1,
GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_1, XXREAL_0, INT_1, PARTFUN1, PBOOLE,
COMPOS_1, MEMSTR_0, MEASURE6;
schemes NAT_1;
begin :: General concepts
definition
let N be set;
struct (Mem-Struct over N, COM-Struct) AMI-Struct over N
(# carrier -> set,
ZeroF -> Element of the carrier,
InstructionsF -> Instructions,
Object-Kind -> Function of the carrier, N,
ValuesF -> ManySortedSet of N,
Execution -> Action of the InstructionsF,
product((the ValuesF)*the Object-Kind)
#);
end;
reserve N for with_zero set;
definition
let N;
func Trivial-AMI N -> strict AMI-Struct over N means
:Def1:
the carrier of it = {0} & the ZeroF of it = 0 &
the InstructionsF of it = {[0,{},{}]} &
the Object-Kind of it = 0 .--> 0 &
the ValuesF of it = N --> NAT &
the Execution of it = [0,{},{}] .--> id product((N --> NAT)*(0 .--> 0));
existence
proof
set I = {[0,{},{}]};
reconsider i = [0,{},{}] as Element of I by TARSKI:def 1;
set f = 0 .--> 0;
A1: dom f = dom(0 .--> 0)
.= { 0 };
A2: rng f c= { 0} by FUNCOP_1:13;
0 in N by MEASURE6:def 2;
then { 0 } c= N by ZFMISC_1:31;
then rng f c= N by A2,XBOOLE_1:1;
then reconsider f as Function of {0}, N by A1,RELSET_1:4;
reconsider y = 0 as Element of {0} by TARSKI:def 1;
set E = id product((N-->NAT)*f);
E in Funcs(product((N-->NAT)*f),product((N-->NAT)*f)) by FUNCT_2:9;
then reconsider F = I-->E as Action of I, product((N-->NAT)*f)
by FUNCOP_1:45;
take AMI-Struct(#{0},y,I,f,N-->NAT,F#);
thus thesis;
end;
uniqueness;
end;
registration
let N;
cluster Trivial-AMI N -> 1-element;
coherence
by Def1;
end;
registration
let N;
cluster non empty for AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
registration let N;
cluster Trivial-AMI N ->with_non-empty_values;
coherence
proof let n be object;
set S = Trivial-AMI N, F = the_Values_of S;
assume
A1: n in dom F;
then
A2: (the Object-Kind of S).n in dom the ValuesF of S by FUNCT_1:11;
A3: the ValuesF of S = N --> NAT by Def1;
then
A4: (the Object-Kind of S).n in N by A2;
F.n =(the ValuesF of S).((the Object-Kind of S).n) by A1,FUNCT_1:12
.= NAT by A4,A3,FUNCOP_1:7;
hence F.n is non empty;
end;
end;
registration let N;
cluster with_non-empty_values 1-element for AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
definition
let N;
let S be with_non-empty_values AMI-Struct over N;
let I be Instruction of S, s be State of S;
func Exec(I,s) -> State of S equals
((the Execution of S).I).s;
coherence
proof
consider f being Function such that
A1: (the Execution of S).I = f & dom f = product the_Values_of S and
A2: rng f c= product the_Values_of S by FUNCT_2:def 2;
reconsider s as Element of product the_Values_of S by CARD_3:107;
(the Execution of S).I.s in rng f by A1,FUNCT_1:def 3;
hence thesis by A2;
end;
end;
reserve N for with_zero set;
definition
let N;
let S be with_non-empty_values AMI-Struct over N;
let I be Instruction of S;
attr I is halting means
:Def3:
for s being State of S holds Exec(I,s) = s;
end;
definition
let N;
let S be with_non-empty_values AMI-Struct over N;
attr S is halting means
:Def4: halt S is halting;
end;
registration
let N;
cluster Trivial-AMI N -> halting;
coherence
proof
set T = Trivial-AMI N;
set f = (N --> NAT)*(0 .--> 0);
A1: the Object-Kind of T = 0 .--> 0 &
the ValuesF of T = N --> NAT by Def1;
set I = halt T;
let s be State of T;
reconsider ss=s as Element of product the_Values_of T by CARD_3:107;
(I .--> id product f).I = id product f by FUNCOP_1:72;
hence Exec(I,s) = (id product f).ss by Def1
.= s by A1;
end;
end;
registration
let N;
cluster halting
for with_non-empty_values non empty AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
registration
let N;
let S be halting with_non-empty_values AMI-Struct over N;
cluster halt S -> halting;
coherence by Def4;
end;
registration
let N;
let S be halting with_non-empty_values AMI-Struct over N;
cluster halting for Instruction of S;
existence
proof
take halt S;
thus thesis;
end;
end;
theorem
for s being State of Trivial-AMI N, i being Instruction of
Trivial-AMI N holds Exec(i,s) = s
proof
set T = Trivial-AMI N;
let s be State of Trivial-AMI N, i be Instruction of Trivial-AMI N;
set f = (N --> NAT)*(0 .--> 0);
A1: the Object-Kind of T = 0 .--> 0 &
the ValuesF of T = N --> NAT by Def1;
reconsider ss=s as Element of product the_Values_of T by CARD_3:107;
the InstructionsF of T = {[0,{},{}]} by Def1;
then (i .--> id product f).i = id product f & i = [0,{},{}] by FUNCOP_1:72
,TARSKI:def 1;
hence Exec(i,s) = (id product f).ss by Def1
.= s by A1;
end;
registration
let E be with_zero set;
cluster Trivial-AMI E -> IC-Ins-separated;
coherence
proof set S = Trivial-AMI E;
A1: the Object-Kind of Trivial-AMI E = 0 .--> 0 &
the ValuesF of Trivial-AMI E = E --> NAT by Def1;
A2: 0 in E by MEASURE6:def 2;
A3: 0 in dom(0 .--> 0) by FUNCOP_1:73;
thus Values IC Trivial-AMI E
= (the_Values_of Trivial-AMI E).0 by Def1
.= ((E --> NAT)*(0 .--> 0)).0 by A1
.= (E --> NAT).((0 .--> 0).0) by A3,FUNCT_1:13
.= (E --> NAT).0 by FUNCOP_1:72
.= NAT by A2,FUNCOP_1:7;
end;
end;
registration
let M be with_zero set;
cluster IC-Ins-separated strict trivial
for non empty with_non-empty_values AMI-Struct over M;
existence
proof
take Trivial-AMI M;
thus thesis;
end;
end;
registration
let N;
cluster IC-Ins-separated halting strict
for 1-element with_non-empty_values AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
begin :: General theory
reserve x,y,z,A,B for set,
f,g,h for Function,
i,j,k for Nat;
reserve S for IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
s for State of S;
definition
let N,S;
let p be (the InstructionsF of S)-valued Function;
let s be State of S;
func CurInstr(p,s) -> Instruction of S equals
p/.IC s;
coherence;
end;
definition
let N,S;
let s be State of S;
let p be (the InstructionsF of S)-valued Function;
func Following(p,s) -> State of S equals
Exec(CurInstr(p,s),s);
correctness;
end;
definition
let N,S;
let p be NAT-defined (the InstructionsF of S)-valued Function;
deffunc F(set,State of S) = down Following(p,$2);
let s be State of S, k be Nat;
func Comput(p,s,k) -> State of S means
:Def7:
ex f being sequence of product the_Values_of S st
it = f.k & f.0 = s & for i being Nat holds f.(i+1) = Following(p,f.i);
existence
proof
reconsider ss=s as Element of product the_Values_of S by CARD_3:107;
consider f being sequence of product the_Values_of S such that
A1: f.0 = ss and
A2: for n being Nat holds f.(n+1) = F(n,f.n) from NAT_1:sch 12;
take f.k, f;
thus f.k = f.k;
thus f.0 = s by A1;
let i be Nat;
thus f.(i+1) = F(i,f.i) by A2
.= Following(p,f.i);
end;
uniqueness
proof
let s1,s2 be State of S;
given f1 being sequence of product the_Values_of S such that
A3: s1 = f1.k and
A4: f1.0 = s and
A5: for i being Nat holds f1.(i+1) = Following(p,f1.i);
given f2 being sequence of product the_Values_of S such that
A6: s2 = f2.k and
A7: f2.0 = s and
A8: for i being Nat holds f2.(i+1) = Following(p,f2.i);
reconsider s as Element of product the_Values_of S by CARD_3:107;
A9: f1.0 = s by A4;
A10: for i being Nat holds f1.(i+1) = F(i,f1.i) by A5;
A11: f2.0 = s by A7;
A12: for i being Nat holds f2.(i+1) = F(i,f2.i) by A8;
f1 = f2 from NAT_1:sch 16(A9,A10,A11,A12);
hence thesis by A3,A6;
end;
end;
definition
let N;
let S be halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S;
pred p halts_on s means
ex k being Nat
st IC Comput(p,s,k) in dom p & CurInstr(p,Comput(p,s,k)) = halt S;
end;
registration
let N be non empty with_zero set;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s be State of S;
reduce Comput(p,s,0) to s;
reducibility
proof
ex f being sequence of product the_Values_of S st
Comput(p,s,0) = f.0 & f.0 = s & for i being Nat holds
f.(i+1) = Following(p,f.i) by Def7;
hence thesis;
end;
end;
theorem
for N be non empty with_zero set
for S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s be State of S holds Comput(p,s,0) = s;
theorem Th3:
for N be non empty with_zero set
for S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s be State of S, k be Nat holds
Comput(p,s,k+1) = Following(p,Comput(p,s,k))
proof let N;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s be State of S, k be Nat;
deffunc F(set,State of S) = down Following(p,$2);
reconsider s as Element of product the_Values_of S by CARD_3:107;
consider f being sequence of product the_Values_of S such that
A1: Comput(p,s,k+1) = f.(k+1) and
A2: f.0 = s and
A3: for i being Nat holds f.(i+1) = Following(p,f.i) by Def7;
consider g being sequence of product the_Values_of S such that
A4: Comput(p,s,k) = g.k and
A5: g.0 = s and
A6: for i being Nat holds g.(i+1) = Following(p,g.i) by Def7;
A7: for i being Nat holds f.(i+1) = F(i,f.i) by A3;
A8: for i being Nat holds g.(i+1) = F(i,g.i) by A6;
f = g from NAT_1:sch 16(A2,A7,A5,A8);
hence thesis by A1,A4,A6;
end;
reserve N for non empty with_zero set,
S for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
s for State of S;
theorem Th4:
for p being NAT-defined (the InstructionsF of S)-valued Function
for k holds Comput(p,s,i+k) = Comput(p,Comput(p,s,i),k)
proof let p be NAT-defined (the InstructionsF of S)-valued Function;
defpred P[Nat] means Comput(p,s,i+$1)
= Comput(p, Comput(p,s,i),$1);
A1: now
let k;
assume
A2: P[k];
Comput(p,s,i+(k+1)) = Comput(p,s,i+k+1)
.= Following(p, Comput(p,s,i+k)) by Th3
.= Comput(p, Comput(p,s,i),k+1) by A2,Th3;
hence P[k+1];
end;
A3: P[ 0];
thus for k holds P[k] from NAT_1:sch 2(A3,A1);
end;
theorem Th5:
i <= j implies
for N for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for p being NAT-defined (the InstructionsF of S)-valued Function
for s being State of S st CurInstr(p,Comput(p,s,i)) = halt S
holds Comput(p,s,j) = Comput(p,s,i)
proof
assume i <= j;
then consider k being Nat such that
A1: j = i + k by NAT_1:10;
reconsider k as Nat;
A2: j = i + k by A1;
let N;
let S be halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S such that
A3: CurInstr(p,Comput(p,s,i))
= halt S;
defpred P[Nat] means Comput(p,s,i+$1)
= Comput(p,s,i);
A4: now
let k;
assume
A5: P[k];
Comput(p,s,i+(k+1)) = Comput(p,s,i+k+1)
.= Following(p,Comput(p,s,i+k)) by Th3
.= Comput(p,s,i) by A3,A5,Def3;
hence P[k+1];
end;
A6: P[ 0];
for k holds P[k] from NAT_1:sch 2(A6,A4);
hence thesis by A2;
end;
reserve n for Nat;
definition
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S such that
A1: p halts_on s;
func Result(p,s) -> State of S means
:Def9:
ex k st it = Comput(p,s,k) & CurInstr(p,it) = halt S;
uniqueness
proof
let s1,s2 be State of S;
given k1 being Nat such that
A2: s1 = Comput(p,s,k1) & CurInstr(p, s1) = halt S;
given k2 being Nat such that
A3: s2 = Comput(p,s,k2) & CurInstr(p, s2) = halt S;
k1 <= k2 or k2 <= k1;
hence thesis by A2,A3,Th5;
end;
correctness
by A1;
end;
theorem
for S being IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S
holds Comput(P,s,k+1) = Exec(P.IC Comput(P,s,k),Comput(P,s,k))
proof
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
let P be Instruction-Sequence of S;
let s be State of S;
A1: dom P = NAT by PARTFUN1:def 2;
thus Comput(P,s,k+1) = Following(P,Comput(P,s,k)) by Th3
.= Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by A1,PARTFUN1:def 6;
end;
theorem Th7:
for S being IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S, k st P.IC Comput(P,s,k) = halt S
holds Result(P,s) = Comput(P,s,k)
proof
let S be IC-Ins-separated halting non empty with_non-empty_values
AMI-Struct over N;
let P be Instruction-Sequence of S;
let s be State of S, k;
A1: dom P = NAT by PARTFUN1:def 2;
assume P.IC Comput(P,s,k) = halt S;
then
A2: CurInstr(P,Comput(P,s,k)) = halt S by A1,PARTFUN1:def 6;
then P halts_on s by A1;
hence thesis by A2,Def9;
end;
theorem Th8:
for S being IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st ex k st P.IC Comput(P,s,k) = halt S
for i holds Result(P,s) = Result(P,Comput(P,s,i))
proof
let S be IC-Ins-separated halting non empty
with_non-empty_values AMI-Struct over N;
let P be Instruction-Sequence of S;
let s be State of S;
given k such that
A1: P.IC Comput(P,s,k) = halt S;
let i;
A2: dom P = NAT by PARTFUN1:def 2;
set s9 = Comput(P,s,k);
A3: CurInstr(P, s9) = halt S by A1,A2,PARTFUN1:def 6;
now
per cases;
suppose
i <= k;
then consider j being Nat such that
A4: k = i + j by NAT_1:10;
reconsider j as Nat;
A5: Comput(P,s,k) = Comput(P,Comput(P,s,i),j) by A4,Th4;
A6: P halts_on Comput(P,s,i) by A3,A5,A2;
thus Result(P,s) = s9 by A1,Th7
.= Result(P,Comput(P,s,i)) by A3,A5,A6,Def9;
end;
suppose
A7: i >= k;
A8: Comput(P,Comput(P,s,k),0) = Comput(P,s,k);
A9: Comput(P,s,i) = s9 by A3,A7,Th5;
A10: P halts_on Comput(P,s,i) by A2,A9,A3,A8;
thus Result(P,s) = s9 by A1,Th7
.= Result(P,Comput(P,s,i)) by A3,A9,A8,A10,Def9;
end;
end;
hence thesis;
end;
definition
let N;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be (the InstructionsF of S)-valued NAT-defined Function;
let IT be PartState of S;
attr IT is p-autonomic means
for P,Q being Instruction-Sequence of S
st p c= P & p c= Q
for s1,s2 being State of S st IT c= s1 & IT c= s2
for i holds Comput(P,s1,i)|dom IT = Comput(Q,s2,i)|dom IT;
end;
definition
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be (the InstructionsF of S)-valued NAT-defined Function;
let IT be PartState of S;
attr IT is p-halted means
for s being State of S st IT c= s
for P being Instruction-Sequence of S
st p c= P
holds P halts_on s;
end;
registration
let N;
cluster halting strict
for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
begin :: Preprograms
theorem Th9:
for S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N
for l being Nat, I being Instruction of S
for P being NAT-defined (the InstructionsF of S)-valued Function
st l .--> I c= P
for s being State of S st IC S .--> l c= s
holds CurInstr(P,s) = I
proof
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
let l be Nat, I be Instruction of S;
let P be NAT-defined (the InstructionsF of S)-valued Function such that
A1: l .--> I c= P;
let s be State of S such that
A2: IC S .--> l c= s;
IC S in dom(IC S .--> l) by TARSKI:def 1;
then
A3: IC s = (IC S .--> l).IC S by A2,GRFUNC_1:2
.= l by FUNCOP_1:72;
A4: IC s in dom(l.--> I) by A3,TARSKI:def 1;
dom(l.--> I) c= dom P by A1,RELAT_1:11;
hence CurInstr(P,s) = P.IC s by A4,PARTFUN1:def 6
.= (l .--> I).IC s by A4,A1,GRFUNC_1:2
.= I by A3,FUNCOP_1:72;
end;
theorem Th10:
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for l being Nat
for P being NAT-defined (the InstructionsF of S)-valued Function
st l .--> halt S c= P
for p being l-started PartState of S
holds p is P-halted
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let l be Nat;
let P be NAT-defined (the InstructionsF of S)-valued Function such that
A1: l .--> halt S c= P;
let p be l-started PartState of S;
set h = halt S;
set I = p +* P;
let s be State of S such that
A2: p c= s;
let Q be Instruction-Sequence of S such that
A3: P c= Q;
take 0;
dom Q = NAT by PARTFUN1:def 2;
hence IC Comput(Q,s,0) in dom Q;
Start-At(l,S) c= p by MEMSTR_0:29;
then
A4: Start-At(l,S) c= s by A2,XBOOLE_1:1;
A5: l.-->h c= Q by A1,A3,XBOOLE_1:1;
IC S in dom Start-At(l,S) by MEMSTR_0:15;
then
A7: IC s = IC Start-At(l,S) by A4,GRFUNC_1:2
.= l by FUNCOP_1:72;
A8: IC s in dom(l.-->h) by A7,TARSKI:def 1;
A9: dom(l.-->h) c= dom Q by A5,RELAT_1:11;
thus CurInstr(Q, Comput(Q,s,0))
= CurInstr(Q, s)
.= Q.IC s by A9,A8,PARTFUN1:def 6
.= (l.-->h).IC s by A8,A5,GRFUNC_1:2
.= CurInstr(l .--> h,s) by A8,PARTFUN1:def 6
.= halt S by A4,A5,Th9;
end;
theorem Th11:
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for l being Nat
for P being NAT-defined (the InstructionsF of S)-valued Function
st l .--> halt S c= P
for p being l-started PartState of S
for s being State of S st p c= s
for i holds Comput(P,s,i) = s
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let l be Nat;
let P be NAT-defined (the InstructionsF of S)-valued Function such that
A1: l .--> halt S c= P;
let p be l-started PartState of S;
set h = halt S;
let s be State of S such that
A2: p c= s;
A3: Start-At(l,S) c= p by MEMSTR_0:29;
defpred P[Nat] means Comput(P,s,$1) = s;
A4: Start-At(l,S) c= s by A3,A2,XBOOLE_1:1;
A5: now
let i;
assume
A6: P[i];
Comput(P,s,i+1)
= Following(P, s) by A6,Th3
.= Exec(halt S,s) by A4,A1,Th9
.= s by Def3;
hence P[i+1];
end;
A7: P[ 0];
thus for i holds P[i] from NAT_1:sch 2(A7,A5);
end;
theorem Th12:
for S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for l being Nat
for P being NAT-defined (the InstructionsF of S)-valued Function
st l .--> halt S c= P
for p being l-started PartState of S
holds p is P-autonomic
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let l be Nat;
set h = halt S;
set p = Start-At(l,S);
let P be NAT-defined (the InstructionsF of S)-valued Function such that
A1: l .--> halt S c= P;
let p be l-started PartState of S;
set I = p +* P;
let Q1,Q2 be Instruction-Sequence of S such that
A2: P c= Q1 & P c= Q2;
let s1,s2 be State of S;
assume that
A3: p c= s1 and
A4: p c= s2;
let i;
A5: l .--> halt S c= Q1 & l .--> halt S c= Q2 by A1,A2,XBOOLE_1:1;
hence Comput(Q1,s1,i)|dom p
= s1|dom p by A3,Th11
.= p by A3,GRFUNC_1:23
.= s2|dom p by A4,GRFUNC_1:23
.= Comput(Q2,s2,i)|dom p by A4,Th11,A5;
end;
registration
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let P be non halt-free (the InstructionsF of S)-valued NAT-defined Function;
cluster P-autonomic P-halted non empty for FinPartState of S;
existence
proof
halt S in rng P by COMPOS_1:def 11;
then consider i being object such that
A1: i in dom P and
A2: P.i = halt S by FUNCT_1:def 3;
dom P c= NAT by RELAT_1:def 18;
then reconsider i as Nat by A1;
take p = Start-At(i,S);
i .--> halt S c= P by A1,A2,FUNCT_4:85;
hence thesis by Th10,Th12;
end;
end;
definition
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let P be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
mode Autonomy of P -> FinPartState of S means
:Def12: it is P-autonomic P-halted;
existence
proof
halt S in rng P by COMPOS_1:def 11;
then consider x being object such that
A1: x in dom P and
A2: P.x = halt S by FUNCT_1:def 3;
dom P c= NAT by RELAT_1:def 18;
then reconsider m = x as Nat by A1;
[m,halt S] in P by A1,A2,FUNCT_1:def 2;
then {[m,halt S]} c= P by ZFMISC_1:31;
then
A3: m .--> halt S c= P by FUNCT_4:82;
take d = Start-At(m,S);
thus d is P-autonomic by A3,Th12;
thus d is P-halted by A3,Th10;
end;
end;
definition
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
let d be FinPartState of S;
assume
A1: d is Autonomy of p;
func Result(p,d) -> FinPartState of S means
for P being Instruction-Sequence of S
st p c= P
for s being State of S st d c= s
holds it = Result(P,s)|dom d;
existence
proof
consider h being State of S such that
A2: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S
such that
A3: p c= H by PBOOLE:145;
A4: d is p-halted p-autonomic by A1,Def12;
then H halts_on h by A2,A3;
then consider k1 being Nat such that
A5: Result(H,h) = Comput(H,h,k1) and
A6: CurInstr(H, Result(H,h)) = halt S by Def9;
reconsider R = (Result(H,h))|dom d as FinPartState of S;
take R;
let P be Instruction-Sequence of S such that
A7: p c= P;
let s be State of S;
assume
A8: d c= s;
then P halts_on s by A4,A7;
then consider k2 being Nat such that
A9: Result(P,s) = Comput(P,s,k2) and
A10: CurInstr(P, Result(P,s)) = halt S by Def9;
per cases;
suppose
k1 <= k2;
then Result(H,h) = Comput(H,h,k2) by A5,A6,Th5;
hence R = (Result(P,s))|dom d by A9,A4,A3,A7,A8,A2;
end;
suppose
k1 >= k2;
then Result(P,s) = Comput(P,s,k1) by A9,A10,Th5;
hence thesis by A5,A4,A3,A7,A8,A2;
end;
end;
correctness
proof
consider h being State of S such that
A11: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S
such that
A12: p c= H by PBOOLE:145;
let p1,p2 be FinPartState of S such that
A13: for P being Instruction-Sequence of S
st p c= P
for s being State of S st d c= s
holds p1 = (Result(P,s))|dom d and
A14: for P being Instruction-Sequence of S
st p c= P
for s being State of S st d c= s
holds p2 = (Result(P,s))|dom d;
thus p1 = (Result(H,h))|dom d by A13,A11,A12
.= p2 by A14,A11,A12;
end;
end;
begin :: Computability
definition
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
let d be FinPartState of S, F be Function;
pred p,d computes F means
for x being set st x in dom F
ex s being FinPartState of S
st x = s & d +* s is Autonomy of p & F.s c= Result(p,d+* s);
end;
theorem
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for p being non halt-free
NAT-defined (the InstructionsF of S)-valued Function
for d being FinPartState of S holds
p,d computes {};
theorem
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for p being non halt-free
NAT-defined (the InstructionsF of S)-valued Function
for d being FinPartState of S
holds d is Autonomy of p iff p,d computes {} .--> Result(p,d)
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
let d be FinPartState of S;
thus d is Autonomy of p implies p,d computes {} .--> Result(p,d)
proof
assume
A2: d is Autonomy of p;
let x be set;
assume
A3: x in dom({} .--> Result(p,d));
then
A4: x = {} by TARSKI:def 1;
then reconsider s = x as FinPartState of S by FUNCT_1:104,RELAT_1:171;
take s;
thus x = s;
d +* {} = d;
hence d +* s is Autonomy of p by A2,A3,TARSKI:def 1;
thus thesis by A4,FUNCOP_1:72;
end;
A5: {} in dom({} .--> Result(p,d)) by TARSKI:def 1;
assume p,d computes {} .--> Result(p,d);
then ex s being FinPartState of S
st {} = s & d +* s is Autonomy of p &
({} .--> Result(p,d)).s c= Result(p,d+* s)
by A5;
hence thesis;
end;
theorem
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for p being non halt-free
NAT-defined (the InstructionsF of S)-valued Function
for d being FinPartState of S
holds d is Autonomy of p iff p,d computes {} .--> {}
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be non halt-free
NAT-defined (the InstructionsF of S)-valued Function;
let d be FinPartState of S;
thus d is Autonomy of p implies p,d computes {} .--> {}
proof
assume
A2: d is Autonomy of p;
let x be set;
assume
A3: x in dom({} .--> {});
then
x = {} by TARSKI:def 1;
then reconsider s = x as FinPartState of S by FUNCT_1:104,RELAT_1:171;
take s;
A5: d +* {} = d;
thus x = s;
thus d +* s is Autonomy of p by A2,A3,A5,TARSKI:def 1;
({} .--> {}).s = {};
hence thesis by XBOOLE_1:2;
end;
A6: {} in dom({} .--> {}) by TARSKI:def 1;
assume p,d computes {} .--> {};
then ex s being FinPartState of S
st {} = s & d +* s is Autonomy of p &
({} .--> {}).s c= Result(p,d+* s) by A6;
hence thesis;
end;
begin :: InsType & InsCode
registration
let N;
cluster IC-Ins-separated for non empty AMI-Struct over N;
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
begin :: Some Remarks on AMI-Struct
reserve N for with_zero non empty set;
theorem Th16:
for S being IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s being State of S holds p halts_on s
iff ex i st p halts_at IC Comput(p,s,i)
proof
let S be IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S;
hereby
assume p halts_on s;
then consider i being Nat such that
A1: IC Comput(p,s,i) in dom p and
A2: CurInstr(p,Comput(p,s,i)) = halt S;
reconsider i as Nat;
take i;
p.IC Comput(p,s,i) = halt S by A1,A2,PARTFUN1:def 6;
hence p halts_at IC Comput(p,s,i) by A1;
end;
given i being Nat such that
A3: p halts_at IC Comput(p,s,i);
A4: IC Comput(p,s,i) in dom p by A3;
A5: p.IC Comput(p,s,i) = halt S by A3;
take i;
thus IC Comput(p,s,i) in dom p by A3;
thus CurInstr(p,Comput(p,s,i)) = halt S by A4,A5,PARTFUN1:def 6;
end;
theorem Th17:
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s being State of S,
k being Nat st p halts_on s
holds Result(p,s) = Comput(p,s,k) iff p halts_at IC Comput(p,s,k)
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S, k being Nat;
assume
A1: p halts_on s;
then consider n being Nat such that
A2: IC Comput(p,s,n) in dom p and
A3: CurInstr(p,Comput(p,s,n)) = halt S;
hereby
assume
A4: Result(p,s) = Comput(p,s,k);
consider i being Nat such that
A5: Result(p,s) = Comput(p,s,i) and
A6: CurInstr(p,Result(p,s)) = halt S by A1,Def9;
reconsider i,n as Nat;
A7: now per cases;
suppose i <= n;
hence Comput(p,s,i) = Comput(p,s,n) by A5,A6,Th5;
end;
suppose n <= i;
hence Comput(p,s,i) = Comput(p,s,n) by A3,Th5;
end;
end;
p.IC Comput(p,s,k) = halt S by A7,A6,A4,A2,A5,PARTFUN1:def 6;
hence p halts_at IC Comput(p,s,k) by A7,A2,A5,A4;
end;
assume that
A8: IC Comput(p,s,k) in dom p and
A9: p.IC Comput(p,s,k) = halt S;
A10: CurInstr(p,Comput(p,s,k)) = halt S by A8,A9,PARTFUN1:def 6;
reconsider k,n as Nat;
now per cases;
suppose n <= k;
hence Comput(p,s,k) = Comput(p,s,n) by A3,Th5;
end;
suppose k <= n;
hence Comput(p,s,k) = Comput(p,s,n) by A10,Th5;
end;
end;
hence thesis by A3,Def9,A1;
end;
theorem Th18:
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for P being (the InstructionsF of S)-valued NAT-defined Function,
s being State of S, k st P halts_at IC Comput(P,s,k)
holds Result(P,s) = Comput(P,s,k)
proof
let S be halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
P be (the InstructionsF of S)-valued NAT-defined Function,
s be State of S, k;
assume
A1: P halts_at IC Comput(P,s,k);
then P halts_on s by Th16;
hence thesis by A1,Th17;
end;
theorem Th19:
i <= j implies for S being halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for P being (the InstructionsF of S)-valued NAT-defined Function
for s being State of S st P halts_at IC Comput(P,s,i)
holds P halts_at IC Comput(P,s,j)
proof
assume
A1: i <= j;
let S be halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S;
assume that
A2: IC Comput(p,s,i) in dom p and
A3: p.IC Comput(p,s,i) = halt S;
A4: CurInstr(p,Comput(p,s,i)) = halt S by A2,A3,PARTFUN1:def 6;
hence IC Comput(p,s,j) in dom p by A2,A1,Th5;
thus p.IC Comput(p,s,j) = halt S by A1,A3,A4,Th5;
end;
theorem
i <= j implies for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for P being (the InstructionsF of S)-valued NAT-defined Function
for s being State of S st P halts_at IC Comput(P,s,i)
holds Comput(P,s,j) = Comput(P,s,i)
proof
assume
A1: i <= j;
let S be halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
P be (the InstructionsF of S)-valued NAT-defined Function,
s be State of S;
assume
A2: P halts_at IC Comput(P,s,i);
then P halts_at IC Comput(P,s,j) by A1,Th19;
hence Comput(P,s,j) = Result(P,s) by Th18
.= Comput(P,s,i) by A2,Th18;
end;
theorem
for S being IC-Ins-separated halting non empty with_non-empty_values
AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S st ex k st P halts_at IC Comput(P,s,k)
for i holds Result(P,s) = Result(P,Comput(P,s,i))
by Th8;
definition
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S such that
A1: p halts_on s;
func LifeSpan(p,s) -> Nat means
:Def15:
CurInstr(p,Comput(p,s,it)) = halt S &
for k being Nat st
CurInstr(p,Comput(p,s,k)) = halt S
holds it <= k;
existence
proof
defpred X[Nat] means
CurInstr(p,Comput(p,s,$1))=halt S;
consider k being Nat such that IC Comput(p,s,k) in dom p and
A2: CurInstr(p, Comput(p,s,k)) = halt S by A1;
A3: ex k being Nat st X[k] by A2;
consider k being Nat such that
A4: X[k] & for n being Nat st X[n] holds k <= n from NAT_1:sch 5(A3);
reconsider k as Nat;
take k;
thus thesis by A4;
end;
uniqueness
proof
let it1, it2 be Nat;
assume
A5: not thesis;
then it1 <= it2 & it2 <= it1;
hence contradiction by A5,XXREAL_0:1;
end;
end;
theorem Th22:
for N be non empty with_zero set,
S be IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N,
p being NAT-defined (the InstructionsF of S)-valued Function,
s being State of S, m being Nat
holds p halts_on s iff p halts_on Comput(p,s,m)
proof
let N;
let S be IC-Ins-separated halting
non empty
with_non-empty_values AMI-Struct over N,
p be NAT-defined (the InstructionsF of S)-valued Function,
s be State of S, m be Nat;
hereby
assume p halts_on s;
then consider n being Nat such that
A1: IC Comput(p,s,n) in dom p and
A2: CurInstr(p, Comput(p,s,n)) = halt S;
reconsider n as Nat;
per cases;
suppose
n <= m;
then
Comput(p,s,n) = Comput(p,s,m+0) by A2,Th5
.= Comput(p,Comput(p,s,m),0);
hence p halts_on Comput(p,s,m) by A2,A1;
end;
suppose
n >= m;
then reconsider k = n - m as Element of NAT by INT_1:5;
Comput(p,Comput(p,s,m),k)
= Comput(p,s,m+k) by Th4
.= Comput(p,s,n);
hence p halts_on Comput(p,s,m)
by A1,A2;
end;
end;
given n being Nat such that
A3: IC Comput(p, Comput(p,s,m),n) in dom p and
A4: CurInstr(p, Comput(p,Comput(p,s,m),n)) = halt S;
reconsider nn=n as Nat;
take m+nn;
thus IC Comput(p,s,m+nn) in dom p &
CurInstr(p, Comput(p,s,m+nn)) = halt S by A3,A4,Th4;
end;
reserve N for with_zero non empty set,
S for IC-Ins-separated non empty AMI-Struct over N;
reserve m,n for Nat;
theorem
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p being NAT-defined (the InstructionsF of S)-valued Function,
s being State of S
st p halts_on s
holds Result(p,s) = Comput(p,s,LifeSpan(p,s))
proof
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let p be NAT-defined (the InstructionsF of S)-valued Function;
let s be State of S;
assume
A1: p halts_on s;
then
A2: CurInstr(p,Comput(p,s,LifeSpan(p,s))) = halt S by Def15;
consider m such that
A3: Result(p,s) = Comput(p,s,m) and
A4: CurInstr(p, Result(p,s)) = halt S by A1,Def9;
LifeSpan(p,s) <= m by A1,A3,A4,Def15;
hence thesis by A2,A3,Th5;
end;
theorem
for N be non empty with_zero set,
S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
P being Instruction-Sequence of S,
s being State of S, k being Nat
st CurInstr(P,Comput(P,s,k)) = halt S
holds Comput(P,s,LifeSpan(P,s)) = Comput(P,s,k)
proof
let N;
let S be halting
IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
P being Instruction-Sequence of S,
s be State of S, k be Nat such that
A1: CurInstr(P,Comput(P,s,k)) = halt S;
A2: dom P = NAT by PARTFUN1:def 2;
A3: P halts_on s by A2,A1;
set Ls = LifeSpan(P,s);
A4: CurInstr(P,Comput(P,s,Ls)) = halt S by A3,Def15;
Ls <= k by A1,A3,Def15;
hence thesis by A4,Th5;
end;
theorem
for N be non empty with_zero set
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for p being NAT-defined (the InstructionsF of S)-valued Function
for s being State of S st LifeSpan(p,s) <= j & p halts_on s
holds Comput(p,s,j) = Comput(p,s,LifeSpan(p,s))
proof
let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
p being NAT-defined (the InstructionsF of S)-valued Function,
s be State of S;
assume that
A1: LifeSpan(p,s) <= j and
A2: p halts_on s;
CurInstr(p,Comput(p,s,LifeSpan(p,s))) = halt S by A2,Def15;
hence thesis by A1,Th5;
end;
theorem
for N being with_zero non empty set,
S being IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
e being Nat,
I being Instruction of S,
t being e-started State of S,
u being Instruction-Sequence of S
st e .--> I c= u
holds Following(u,t) = Exec(I, t)
proof
let N;
let S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
e be Nat,
I be Instruction of S,
t be e-started State of S,
u be Instruction-Sequence of S such that
A1: e .--> I c= u;
A2: e in dom(e .--> I) by TARSKI:def 1;
IC t = e by MEMSTR_0:def 11;
then CurInstr(u,t) = u.e by PBOOLE:143
.= (e .--> I).e by A1,A2,GRFUNC_1:2
.= I by FUNCOP_1:72;
hence thesis;
end;
theorem
for S being halting IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N,
P being Instruction-Sequence of S,
s being State of S st s = Following(P,s)
holds for n holds Comput(P,s,n) = s
proof
let S be halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N,
P be Instruction-Sequence of S,
s be State of S;
defpred X[Nat] means Comput(P,s,$1) = s;
assume s = Following(P,s);
then
A1: for n st X[n] holds X[n+1] by Th3;
A2: X[ 0];
thus for n holds X[n] from NAT_1:sch 2(A2, A1);
end;
theorem
for N being with_zero non empty set,
S being IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
P being Instruction-Sequence of S,
s being State of S, i being Instruction of S
holds Exec(P.IC s,s).IC S = IC Following(P,s)
proof
let N;
let S be IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N,
P be Instruction-Sequence of S,
s be State of S, i being Instruction of S;
NAT = dom P by PARTFUN1:def 2;
hence Exec(P.IC s,s).IC S = IC Following(P,s) by PARTFUN1:def 6;
end;
theorem
for S being IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N
for P being Instruction-Sequence of S
for s being State of S holds P halts_on s
iff ex k st CurInstr(P,Comput(P,s,k)) = halt S
proof
let S be IC-Ins-separated halting non empty with_non-empty_values
AMI-Struct over N;
let P be Instruction-Sequence of S;
let s be State of S;
thus P halts_on s
implies ex k st CurInstr(P,Comput(P,s,k))
= halt S;
given k such that
A1: CurInstr(P,Comput(P,s,k)) = halt S;
take k;
IC Comput(P,s,k) in NAT;
hence IC Comput(P,s,k) in dom P by PARTFUN1:def 2;
thus CurInstr(P, Comput(P,s,k)) = halt S by A1;
end;
reserve S for IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N;
theorem Th30:
for F being Instruction-Sequence of S
for s being State of S st ex k being Nat st F.(IC
Comput(F,s,k)) = halt S holds F halts_on s
proof
let F be Instruction-Sequence of S;
let s be State of S;
given k being Nat such that
A1: F.(IC Comput(F,s,k)) = halt S;
take k;
A2: dom F = NAT by PARTFUN1:def 2;
hence IC Comput(F,s,k) in dom F;
thus CurInstr(F, Comput(F,s,k)) = halt S by A1,A2,PARTFUN1:def 6;
end;
::$CT
theorem Th31:
for F being Instruction-Sequence of S
for s being State of S, k being Nat
holds F.(IC Comput(F,s,k)) <> halt S &
F.(IC Comput(F,s,k+1)) = halt S iff LifeSpan(F,s) = k+1 & F halts_on s
proof
let F be Instruction-Sequence of S;
let s be State of S, k be Nat;
A1: dom F = NAT by PARTFUN1:def 2;
hereby
assume that
A2: F.(IC Comput(F,s,k)) <> halt S and
A3: F.(IC Comput(F,s,k+1)) = halt S;
A4: CurInstr(F,Comput(F,s,k)) <> halt S by A2,A1,PARTFUN1:def 6;
A5: now
let i be Nat;
assume that
A6: CurInstr(F,Comput(F,s,i)) = halt S and
A7: k+1 > i;
i <= k by A7,NAT_1:13;
hence contradiction by A4,A6,Th5;
end;
A8: F halts_on s by A3,Th30;
CurInstr(F,Comput(F,s,k+1)) = halt S by A3,A1,PARTFUN1:def 6;
hence LifeSpan(F,s) = k+1 & F halts_on s by A5,Def15,A8;
end;
assume
A9: LifeSpan(F,s) = k+1 & F halts_on s;
A10: now
assume CurInstr(F,Comput(F,s,k)) = halt S;
then k+1 <= k by A9,Def15;
hence contradiction by NAT_1:13;
end;
CurInstr(F,Comput(F,s,k+1)) = halt S by A9,Def15;
hence thesis by A10,A1,PARTFUN1:def 6;
end;
theorem
for F being Instruction-Sequence of S
for s being State of S, k being Nat st IC
Comput(F,s,k) <> IC Comput(F,s,k+1) & F.(IC Comput(F,s,k+1)) = halt S
holds LifeSpan(F,s) = k+1
proof
let F be Instruction-Sequence of S;
let s be State of S, k be Nat;
assume that
A1: IC Comput(F,s,k) <> IC Comput(F,s,k+1) and
A2: F.(IC Comput(F,s,k+1)) = halt S;
A3: dom F = NAT by PARTFUN1:def 2;
now
assume F.(IC Comput(F,s,k)) = halt S;
then CurInstr(F,Comput(F,s,k)) = halt S by A3,PARTFUN1:def 6;
hence contradiction by A1,Th5,NAT_1:11;
end;
hence thesis by A2,Th31;
end;
theorem
for F being Instruction-Sequence of S
for s being State of S, k being Nat st
F halts_on Comput(F,s,k) & 0 < LifeSpan(F,Comput(F,s,k))
holds LifeSpan(F,s) = k+LifeSpan(F,Comput(F,s,k))
proof
let F be Instruction-Sequence of S;
let s be State of S, k be Nat;
set s2 = Comput(F,s,k), c = LifeSpan(F,Comput(F,s,k));
assume that
A1: F halts_on s2 and
A2: 0 < c;
consider l being Nat such that
A3: c = l+1 by A2,NAT_1:6;
reconsider l as Nat;
F.(IC Comput(F,s2,l+1)) = halt S by A1,A3,Th31;
then
A4: F.(IC Comput(F,s,k+(l+1))) = halt S by Th4;
F.(IC Comput(F,s2,l)) <> halt S by A1,A3,Th31;
then F.(IC Comput(F,s,k+l)) <> halt S by Th4;
hence LifeSpan(F,s) = (k+l)+1 by A4,Th31
.= k+c by A3;
end;
theorem
for F being Instruction-Sequence of S
for s being State of S, k being Nat
st F halts_on Comput(F,s,k)
holds Result(F,Comput(F,s,k)) = Result(F,s)
proof
let F be Instruction-Sequence of S;
let s be State of S, k be Nat;
set s2 = Comput(F,s,k);
assume
A1: F halts_on s2;
then consider l being Nat such that
A2: Result(F,s2) = Comput(F,s2,l) &
CurInstr(F,Result(F,s2)) = halt S by Def9;
A3: F halts_on s by A1,Th22;
Comput(F,Comput(F,s,k),l) = Comput(F,s,k+l) by Th4;
hence thesis by A3,A2,Def9;
end;
reserve S for halting IC-Ins-separated non empty
with_non-empty_values AMI-Struct over N;
reserve P for Instruction-Sequence of S;
theorem
for s being State of S st P halts_on s for k being Nat
st LifeSpan(P,s) <= k
holds CurInstr(P, Comput(P,s,k)) = halt S
proof
let s be State of S;
assume
P halts_on s;
then
A1: CurInstr(P,Comput(P,s,LifeSpan(P,s))) = halt S by Def15;
let k be Nat;
assume
LifeSpan(P,s) <= k;
hence thesis by A1,Th5;
end;