set Ma = Macro (Divide (a,b));
let s be State of SCM+FSA; :: according to EXTPRO_1:def 10,SCMFSA6B:def 3,SCMFSA6C:def 1 :: thesis: ( not Initialize (Macro (Divide (a,b))) c= s or for b₁ being set holds
( not ProgramPart (Initialize (Macro (Divide (a,b)))) c= b₁ or b₁ halts_on s ) )
assume A45: Initialize (Macro (Divide (a,b))) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize (Macro (Divide (a,b)))) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialize (Macro (Divide (a,b)))) c= P or P halts_on s )
assume A46: ProgramPart (Initialize (Macro (Divide (a,b)))) c= P ; :: thesis: P halts_on s
A47: Macro (Divide (a,b)) c= P by A46, COMPOS_1:144;
take 1 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A48: dom P = NAT by PARTFUN1:def 4;
thus IC (Comput (P,s,1)) in dom P by A48; :: thesis: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then A49: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
Start-At (0,SCM+FSA) c= Initialize (Macro (Divide (a,b))) by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= s by A45, XBOOLE_1:1;
then A50: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A49, GRFUNC_1:8
.= 0 by FUNCOP_1:87 ;
then A51: IC (Exec ((Divide (a,b)),s)) = succ 0 by SCMFSA_2:93
.= 0 + 1 ;
A52: 1 in dom (Macro (Divide (a,b))) by COMPOS_1:147;
A53: 0 in dom (Macro (Divide (a,b))) by COMPOS_1:147;
A54: P . 0 = (Macro (Divide (a,b))) . 0 by A47, A53, GRFUNC_1:8
.= Divide (a,b) by COMPOS_1:148 ;
A55: P . 1 = (Macro (Divide (a,b))) . 1 by A47, A52, GRFUNC_1:8
.= halt SCM+FSA by COMPOS_1:148 ;
Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:4
.= Following (P,s) by EXTPRO_1:3
.= Exec ((Divide (a,b)),s) by A50, A48, PARTFUN1:def 8, A54 ;
hence CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A51, A48, PARTFUN1:def 8, A55; :: thesis: verum