environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, AMI_1, FSM_1, FUNCT_4, FUNCOP_1, RELAT_1, TARSKI, FUNCT_1, CARD_3, ZFMISC_1, CIRCUIT2, NAT_1, GLIB_000, XXREAL_0, PARTFUN1, FINSEQ_1, ARYTM_3, GRAPH_2, CARD_1, FUNCT_2, FINSEQ_4, ARYTM_1, FINSET_1, FRECHET, WAYBEL_0, MEMBERED, AMISTD_1, EXTPRO_1, AMI_WSTD, STRUCT_0, COMPOS_1, QUANTAL1, GOBRD13, MEMSTR_0, FUNCT_7, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, ORDINAL1, CARD_1, XXREAL_0, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, FUNCT_1, RELSET_1, PARTFUN1, DOMAIN_1, CARD_3, FINSEQ_1, FINSEQ_4, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_7, MEASURE6, STRUCT_0, GRAPH_2, NAT_D, XXREAL_2, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_2, AMISTD_1;
definitions TARSKI, XBOOLE_0, AMISTD_1;
theorems TARSKI, FINSEQ_4, FINSEQ_1, GRAPH_2, NAT_1, FUNCT_4, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1, FUNCOP_1, ORDINAL1, GRFUNC_1, FINSEQ_3, INT_1, REVROT_1, FUNCT_7, XBOOLE_0, MEMBERED, XREAL_1, XXREAL_0, FINSEQ_6, PARTFUN1, XXREAL_2, XREAL_0, NAT_D, PBOOLE, AMISTD_1, MEMSTR_0, CARD_3;
schemes NAT_1, FUNCT_7, FINSEQ_2, FRAENKEL, DOMAIN_1, FINSEQ_4;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CARD_3, FUNCT_7, JORDAN1J, CARD_1, XXREAL_2, RELSET_1, FUNCT_4, AMISTD_1, EXTPRO_1, PRE_POLY, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0, ORDINAL1;
constructors HIDDEN, WELLORD2, REAL_1, FINSEQ_4, REALSET1, NAT_D, XXREAL_2, RELSET_1, PRE_POLY, GRAPH_2, AMISTD_1, FUNCT_7, FUNCT_4, PBOOLE, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, REAL, SUBSET, ARITHM;
equalities STRUCT_0, EXTPRO_1, XBOOLE_0, FUNCOP_1, NAT_1, AMISTD_1, MEMSTR_0, CARD_1, ORDINAL1;
expansions XBOOLE_0;
Lm1:
for k being Element of NAT
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds k <= k,S
set III = {[1,0,0],[0,0,0]};
Lm2:
for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = (IC s) + 1
Lm3:
for z being Nat
for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
Lm4:
now for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )
let N be
with_zero set ;
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )let S be non
empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over
N;
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )set F =
(il. (S,0)) .--> (halt S);
dom ((il. (S,0)) .--> (halt S)) = {(il. (S,0))}
by FUNCOP_1:13;
then A1:
card (dom ((il. (S,0)) .--> (halt S))) = 1
by CARD_1:30;
(il. (S,0)) .--> (halt S) is
NAT -defined the
InstructionsF of
S -valued finite lower Function
by Th25;
then A2:
LastLoc ((il. (S,0)) .--> (halt S)) =
il. (
S,
((card ((il. (S,0)) .--> (halt S))) -' 1))
by Th32
.=
il. (
S,
((card (dom ((il. (S,0)) .--> (halt S)))) -' 1))
by CARD_1:62
.=
il. (
S,
0)
by A1, XREAL_1:232
;
hence
((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S
by FUNCOP_1:72;
for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S))let l be
Element of
NAT ;
( ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) )assume
((il. (S,0)) .--> (halt S)) . l = halt S
;
( l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) )assume
l in dom ((il. (S,0)) .--> (halt S))
;
l = LastLoc ((il. (S,0)) .--> (halt S))hence
l = LastLoc ((il. (S,0)) .--> (halt S))
by A2, TARSKI:def 1;
verum
end;