set Ma = Macro (Divide (a,b));
let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def 4,SCMFSA6C:def 1 :: thesis: for b₁ being set holds
( not Macro (Divide (a,b)) c= b₁ or for b₂ being set holds (Comput (b₁,s,b₂)) . (intloc 0) = s . (intloc 0) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not Macro (Divide (a,b)) c= P or for b₁ being set holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0) )
assume A2: Macro (Divide (a,b)) c= P ; :: thesis: for b₁ being set holds (Comput (P,s,b₁)) . (intloc 0) = s . (intloc 0)
let k be Nat; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A3: IC in dom (Start-At (0,SCM+FSA)) by TARSKI:def 1;
A4: IC s = (Start-At (0,SCM+FSA)) . (IC ) by A3, A1, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
0 in dom (Macro (Divide (a,b))) by COMPOS_1:60;
then A5: (Macro (Divide (a,b))) . 0 = P . 0 by A2, GRFUNC_1:2;
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: Comput (P,s,(0 + 1)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Exec ((Divide (a,b)),s) by A4, A5, A6, COMPOS_1:58 ;
1 in dom (Macro (Divide (a,b))) by COMPOS_1:60;
then (Macro (Divide (a,b))) . 1 = P . 1 by A2, GRFUNC_1:2;
then A8: P . 1 = halt SCM+FSA by COMPOS_1:59;
IC (Exec ((Divide (a,b)),s)) = 0 + 1 by A4, SCMFSA_2:67;
then A9: CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA by A8, A7, PBOOLE:143;

per cases ( k = 0 or 1 <= k ) by NAT_1:14;

suppose k = 0 ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) ; :: thesis: verum

end;

suppose A10: 1 <= k ; :: thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0)

(Comput (P,s,1)) . (intloc 0) = s . (intloc 0) by A7, SCMFSA_2:67;
hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A9, A10, EXTPRO_1:5; :: thesis: verum

end;

end;