set I = <%i%>;
A1:
ProgramPart <%i%> = <%i%>
by RELAT_1:209;
let s be State of SCM+FSA; SCMFSA8A:def 4 for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds <%i%> is_pseudo-closed_on s,P
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; <%i%> is_pseudo-closed_on s,P
set s1 = Initialize s;
dom <%i%> = 1
by AFINSQ_1:36;
then A2:
0 in dom <%i%>
by CARD_1:87, TARSKI:def 1;
dom (P +* <%i%>) = (dom P) \/ (dom <%i%>)
by FUNCT_4:def 1;
then A3:
0 in dom (P +* <%i%>)
by A2, XBOOLE_0:def 3;
A4: CurInstr ((P +* <%i%>),(Initialize s)) =
(P +* <%i%>) /. 0
by COMPOS_1:def 16
.=
(P +* <%i%>) . 0
by A3, PARTFUN1:def 8
.=
<%i%> . 0
by A2, FUNCT_4:14
.=
i
by AFINSQ_1:38
;
take
1
; SCMFSA8A:def 3 ( IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),1)) = card (ProgramPart <%i%>) & ( for n being Element of NAT st n < 1 holds
IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),n)) in dom <%i%> ) )
thus IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),1)) =
IC (Comput ((P +* <%i%>),(Initialize s),(0 + 1)))
by RELAT_1:209
.=
IC (Following ((P +* <%i%>),(Comput ((P +* <%i%>),(Initialize s),0))))
by EXTPRO_1:4
.=
IC (Following ((P +* <%i%>),(Initialize s)))
by EXTPRO_1:3
.=
succ (IC (Initialize s))
by A4, AMISTD_1:def 16
.=
succ 0
by COMPOS_1:def 16
.=
card <%i%>
by AFINSQ_1:38
.=
card (ProgramPart <%i%>)
by RELAT_1:209
; for n being Element of NAT st n < 1 holds
IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),n)) in dom <%i%>
let n be Element of NAT ; ( n < 1 implies IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),n)) in dom <%i%> )
assume
n < 1
; IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),n)) in dom <%i%>
then
n = 0
by NAT_1:14;
then A5: IC (Comput ((P +* <%i%>),(Initialize s),n)) =
IC (Initialize s)
by EXTPRO_1:3
.=
0
by COMPOS_1:def 16
;
dom <%i%> = 1
by AFINSQ_1:36;
hence
IC (Comput ((P +* (ProgramPart <%i%>)),(Initialize s),n)) in dom <%i%>
by A5, CARD_1:87, TARSKI:def 1, A1; verum