let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for F being pre-Macro of S st card F = 1 holds
F = Stop S
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of 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: 0 in dom F by AFINSQ_1:69;
then A6: a = 0 by A4;
(card F) -' 1 = (card F) - 1 by PRE_CIRC:25
.= 0 by A1 ;
then LastLoc F = 0 by AFINSQ_1:74;
then F . 0 = halt S by Def25;
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 = {[0,(halt S)]} by A2, A3, A6, TARSKI:def 1
.= 0 .--> (halt S) by FUNCT_4:87 ;
hence F = Stop S ; :: thesis: verum