:: deftheorem Def13 defines with_while-instruction AOFA_000:def 13 :
for S being non empty UAStr holds
( S is with_while-instruction iff ( 4 in dom the charact of S & the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S ) );