let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: I ';' () is really-closed
A1: dom (Macro ()) = {0,1} by COMPOS_1:61;
A2: ( 1 in dom (Macro ()) & 0 in dom (Macro ()) ) by COMPOS_1:60;
set F = Macro ();
Macro () is really-closed
proof
let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not l in K543(NAT,(Macro ())) or NIC (((Macro ()) /. l),l) c= K543(NAT,(Macro ())) )
assume A3: l in dom (Macro ()) ; :: thesis: NIC (((Macro ()) /. l),l) c= K543(NAT,(Macro ()))
per cases then ( l = 0 or l = 1 ) by ;
suppose A4: l = 0 ; :: thesis: NIC (((Macro ()) /. l),l) c= K543(NAT,(Macro ()))
then (Macro ()) /. l = (Macro ()) . l by
.= goto 0 by ;
then NIC (((Macro ()) /. l),l) = by SCMFSA10:33;
hence NIC (((Macro ()) /. l),l) c= dom (Macro ()) by ; :: thesis: verum
end;
suppose A5: l = 1 ; :: thesis: NIC (((Macro ()) /. l),l) c= K543(NAT,(Macro ()))
then (Macro ()) /. l = (Macro ()) . l by
.= halt SCM+FSA by ;
then NIC (((Macro ()) /. l),l) = {l} by AMISTD_1:2;
hence NIC (((Macro ()) /. l),l) c= dom (Macro ()) by ; :: thesis: verum
end;
end;
end;
then I ';' (Macro ()) is really-closed ;
hence I ';' () is really-closed ; :: thesis: verum