let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( I is_closed_onInit s,p iff I is_closed_on Initialized s,p )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds
( I is_closed_onInit s,p iff I is_closed_on Initialized s,p )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_onInit s,p iff I is_closed_on Initialized s,p )
A2: Initialized s = s +* (Initialize (Initialize ((intloc 0) .--> 1)))
.= Initialize (Initialized s) by FUNCT_4:14 ;

hereby :: thesis: ( I is_closed_on Initialized s,p implies I is_closed_onInit s,p )

assume Z: I is_closed_onInit s,p ; :: thesis: I is_closed_on Initialized s,p
thus I is_closed_on Initialized s,p :: thesis: verum

proof

let k be Element of NAT ; :: according to SCMFSA7B:def 6 :: thesis: IC (Comput ((p +* I),(Initialize (Initialized s)),k)) in K230(I)
thus IC (Comput ((p +* I),(Initialize (Initialized s)),k)) in dom I by A2, Z, Def4; :: thesis: verum

end;

end;

assume Z: I is_closed_on Initialized s,p ; :: thesis: I is_closed_onInit s,p
let k be Element of NAT ; :: according to SCM_HALT:def 4 :: thesis: IC (Comput ((p +* I),(Initialized s),k)) in dom I
thus IC (Comput ((p +* I),(Initialized s),k)) in dom I by A2, Z, SCMFSA7B:def 6; :: thesis: verum