environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions STRUCT_0, FUNCT_1, COMPOS_1, MEMSTR_0;
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;
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;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, FUNCT_7, GRAPH_2, RELSET_1, PRE_POLY, PBOOLE, COMPOS_1, MEMSTR_0, MEASURE6, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, FUNCOP_1, COMPOS_1, MEMSTR_0, CARD_3, COMPOS_0;
expansions STRUCT_0, COMPOS_1;
definition
let N be
with_zero set ;
existence
ex b1 being strict AMI-Struct over N st
( the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,{},{}]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) )
uniqueness
for b1, b2 being strict AMI-Struct over N st the carrier of b1 = {0} & the ZeroF of b1 = 0 & the InstructionsF of b1 = {[0,{},{}]} & the Object-Kind of b1 = 0 .--> 0 & the ValuesF of b1 = N --> NAT & the Execution of b1 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) & the carrier of b2 = {0} & the ZeroF of b2 = 0 & the InstructionsF of b2 = {[0,{},{}]} & the Object-Kind of b2 = 0 .--> 0 & the ValuesF of b2 = N --> NAT & the Execution of b2 = [0,{},{}] .--> (id (product ((N --> NAT) * (0 .--> 0)))) holds
b1 = b2
;
end;
definition
let N be non
empty with_zero set ;
let S be non
empty with_non-empty_values IC-Ins-separated halting 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
;
uniqueness
for b1, b2 being State of S st ex k being Nat st
( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S ) & ex k being Nat st
( b2 = Comput (p,s,k) & CurInstr (p,b2) = halt S ) holds
b1 = b2
correctness
existence
ex b1 being State of S ex k being Nat st
( b1 = Comput (p,s,k) & CurInstr (p,b1) = halt S );
by A1;
end;
definition
let N be non
empty with_zero set ;
let S be non
empty with_non-empty_values IC-Ins-separated halting 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
;
existence
ex b1 being Nat st
( CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
b1 <= k ) )
uniqueness
for b1, b2 being Nat st CurInstr (p,(Comput (p,s,b1))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
b1 <= k ) & CurInstr (p,(Comput (p,s,b2))) = halt S & ( for k being Nat st CurInstr (p,(Comput (p,s,k))) = halt S holds
b2 <= k ) holds
b1 = b2
end;