a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> by SCMFSA_7:1;
hence ( a := k is initial & not a := k is empty & a := k is NAT -defined & a := k is the Instructions of SCM+FSA -valued ) ; :: thesis: verum