let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being pre-Macro of S st card F = 1 holds
F = Stop S
let S be non empty stored-program halting IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being pre-Macro of S st card F = 1 holds
F = Stop S
let F be pre-Macro of S; :: thesis: ( card F = 1 implies F = Stop S )
assume A1: card F = 1 ; :: thesis: F = Stop S
then consider x being set such that
A2: F = {x} by CARD_2:60;
x in F by A2, TARSKI:def 1;
then consider a, b being set such that
A3: [a,b] = x by RELAT_1:def 1;
A4: dom F = {a} by A2, A3, RELAT_1:23;
A5: il. S,0 in dom F by AMISTD_1:49;
then A6: a = il. S,0 by A4, TARSKI:def 1;
(card F) -' 1 = (card F) - 1 by PRE_CIRC:25
.= 0 by A1 ;
then LastLoc F = il. S,0 by AMISTD_1:55;
then F . (il. S,0 ) = halt S by AMISTD_1:def 22;
then halt S in rng F by A5, FUNCT_1:def 5;
then halt S in {b} by A2, A3, RELAT_1:23;
then F = {[(il. S,0 ),(halt S)]} by A2, A3, A6, TARSKI:def 1
.= (il. S,0 ) .--> (halt S) by FUNCT_4:87 ;
hence F = Stop S ; :: thesis: verum