let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for n, k being Nat st n < card I & k < card I holds
I +* (n,(goto k)) is really-closed
let n, k be Nat; :: thesis: ( n < card I & k < card I implies I +* (n,(goto k)) is really-closed )
assume that
A1: n < card I and
A2: k < card I ; :: thesis: I +* (n,(goto k)) is really-closed
set F = I +* (n,(goto k));
A3: n in dom I by A1, AFINSQ_1:66;
A4: k in dom I by A2, AFINSQ_1:66;
A5: dom (I +* (n,(goto k))) = dom I by FUNCT_7:30;
let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not l in K543(NAT,(I +* (n,(goto k)))) or NIC (((I +* (n,(goto k))) /. l),l) c= K543(NAT,(I +* (n,(goto k)))) )
assume A6: l in dom (I +* (n,(goto k))) ; :: thesis: NIC (((I +* (n,(goto k))) /. l),l) c= K543(NAT,(I +* (n,(goto k))))
A7: (I +* (n,(goto k))) /. l = (I +* (n,(goto k))) . l by A6, PARTFUN1:def 6;
per cases ( n = l or n <> l ) ;
suppose n = l ; :: thesis: NIC (((I +* (n,(goto k))) /. l),l) c= K543(NAT,(I +* (n,(goto k))))
then (I +* (n,(goto k))) . l = goto k by A3, FUNCT_7:31;
then NIC (((I +* (n,(goto k))) /. l),l) = {k} by A7, SCMFSA10:33;
hence NIC (((I +* (n,(goto k))) /. l),l) c= dom (I +* (n,(goto k))) by A5, ZFMISC_1:31, A4; :: thesis: verum
end;
suppose n <> l ; :: thesis: NIC (((I +* (n,(goto k))) /. l),l) c= K543(NAT,(I +* (n,(goto k))))
then (I +* (n,(goto k))) . l = I . l by FUNCT_7:32;
then (I +* (n,(goto k))) /. l = I . l by A6, PARTFUN1:def 6
.= I /. l by A6, A5, PARTFUN1:def 6 ;
hence NIC (((I +* (n,(goto k))) /. l),l) c= dom (I +* (n,(goto k))) by A5, A6, AMISTD_1:def 9; :: thesis: verum
end;
end;