:: SCMFSA7B semantic presentation begin set A = NAT ; theorem :: SCMFSA7B:1 for i being Instruction of SCM+FSA holds ( ( i = halt SCM+FSA implies (Directed (Macro i)) . 0 = goto 2 ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) ) proof A1: dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ; let i be Instruction of SCM+FSA; ::_thesis: ( ( i = halt SCM+FSA implies (Directed (Macro i)) . 0 = goto 2 ) & ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) ) A2: (Macro i) . 0 = i by COMPOS_1:58; 0 in {0,1} by TARSKI:def_2; then A3: 0 in dom (Macro i) by COMPOS_1:61; A4: card (Macro i) = 2 by COMPOS_1:56; hereby ::_thesis: ( i <> halt SCM+FSA implies (Directed (Macro i)) . 0 = i ) A5: dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ; assume A6: i = halt SCM+FSA ; ::_thesis: (Directed (Macro i)) . 0 = goto 2 dom ((halt SCM+FSA) .--> (goto 2)) = {(halt SCM+FSA)} by FUNCOP_1:13; then A7: i in dom ((halt SCM+FSA) .--> (goto 2)) by A6, TARSKI:def_1; rng (Macro i) c= the InstructionsF of SCM+FSA by RELAT_1:def_19; hence (Directed (Macro i)) . 0 = (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 2))) * (Macro i)) . 0 by A4, FUNCT_7:116 .= (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) * (Macro i)) . 0 by A5, FUNCT_7:def_3 .= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . i by A3, A2, FUNCT_1:13 .= ((halt SCM+FSA) .--> (goto 2)) . i by A7, FUNCT_4:13 .= goto 2 by A6, FUNCOP_1:72 ; ::_thesis: verum end; A8: dom ((halt SCM+FSA) .--> (goto 2)) = {(halt SCM+FSA)} by FUNCOP_1:13; assume i <> halt SCM+FSA ; ::_thesis: (Directed (Macro i)) . 0 = i then A9: not i in dom ((halt SCM+FSA) .--> (goto 2)) by A8, TARSKI:def_1; rng (Macro i) c= the InstructionsF of SCM+FSA by RELAT_1:def_19; hence (Directed (Macro i)) . 0 = (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 2))) * (Macro i)) . 0 by A4, FUNCT_7:116 .= (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) * (Macro i)) . 0 by A1, FUNCT_7:def_3 .= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . i by A3, A2, FUNCT_1:13 .= (id the InstructionsF of SCM+FSA) . i by A9, FUNCT_4:11 .= i by FUNCT_1:18 ; ::_thesis: verum end; theorem :: SCMFSA7B:2 for i being Instruction of SCM+FSA holds (Directed (Macro i)) . 1 = goto 2 proof let i be Instruction of SCM+FSA; ::_thesis: (Directed (Macro i)) . 1 = goto 2 A1: (Macro i) . 1 = halt SCM+FSA by COMPOS_1:59; 1 in {0,1} by TARSKI:def_2; then A2: 1 in dom (Macro i) by COMPOS_1:61; dom ((halt SCM+FSA) .--> (goto 2)) = {(halt SCM+FSA)} by FUNCOP_1:13; then A3: halt SCM+FSA in dom ((halt SCM+FSA) .--> (goto 2)) by TARSKI:def_1; A4: dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ; ( card (Macro i) = 2 & rng (Macro i) c= the InstructionsF of SCM+FSA ) by COMPOS_1:56, RELAT_1:def_19; hence (Directed (Macro i)) . 1 = (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 2))) * (Macro i)) . 1 by FUNCT_7:116 .= (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) * (Macro i)) . 1 by A4, FUNCT_7:def_3 .= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto 2))) . (halt SCM+FSA) by A2, A1, FUNCT_1:13 .= ((halt SCM+FSA) .--> (goto 2)) . (halt SCM+FSA) by A3, FUNCT_4:13 .= goto 2 by FUNCOP_1:72 ; ::_thesis: verum end; registration let a be Int-Location; let k be Integer; clustera := k -> non empty initial ; coherence ( a := k is initial & not a := k is empty & a := k is NAT -defined & a := k is the InstructionsF of SCM+FSA -valued ) proof 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 InstructionsF of SCM+FSA -valued ) ; ::_thesis: verum end; end; Lm1: for s being State of SCM+FSA st IC s = 0 holds for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st a := k c= P holds P halts_on s proof let s be State of SCM+FSA; ::_thesis: ( IC s = 0 implies for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st a := k c= P holds P halts_on s ) assume A1: IC s = 0 ; ::_thesis: for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st a := k c= P holds P halts_on s let P be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for k being Integer st a := k c= P holds P halts_on s A2: dom P = NAT by PARTFUN1:def_2; let a be Int-Location; ::_thesis: for k being Integer st a := k c= P holds P halts_on s let k be Integer; ::_thesis: ( a := k c= P implies P halts_on s ) assume A3: a := k c= P ; ::_thesis: P halts_on s percases ( k > 0 or k <= 0 ) ; supposeA4: k > 0 ; ::_thesis: P halts_on s then consider k1 being Element of NAT such that A5: k1 + 1 = k and A6: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by SCMFSA_7:def_1; A7: len (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) = (len <%(a := (intloc 0))%>) + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:17 .= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:34 .= k by A5, CARD_1:64 ; set f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>; A8: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . 0 = (<%(a := (intloc 0))%> ^ ((k1 --> (AddTo (a,(intloc 0)))) ^ <%(halt SCM+FSA)%>)) . 0 by AFINSQ_1:27 .= a := (intloc 0) by AFINSQ_1:35 ; reconsider k = k as Element of NAT by A4, INT_1:3; A9: len ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) = (len (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) by AFINSQ_1:17 .= k + 1 by A7, AFINSQ_1:34 ; A10: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_k_holds_ i_in_dom_((<%(a_:=_(intloc_0))%>_^_(k1_-->_(AddTo_(a,(intloc_0)))))_^_<%(halt_SCM+FSA)%>) let i be Element of NAT ; ::_thesis: ( i <= k implies i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) ) assume A11: i <= k ; ::_thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) i < k + 1 by A11, NAT_1:13; hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by A9, NAT_1:44; ::_thesis: verum end; A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_k_holds_ P_._i_=_((<%(a_:=_(intloc_0))%>_^_(k1_-->_(AddTo_(a,(intloc_0)))))_^_<%(halt_SCM+FSA)%>)_._i let i be Element of NAT ; ::_thesis: ( i <= k implies P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i ) assume A13: i <= k ; ::_thesis: P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by A10, A13; hence P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A3, A6, GRFUNC_1:2; ::_thesis: verum end; then A14: P . 0 = a := (intloc 0) by A8; A15: now__::_thesis:_for_n_being_Element_of_NAT_st_n_=_0_holds_ (_Comput_(P,s,n)_=_s_&_CurInstr_(P,(Comput_(P,s,n)))_=_a_:=_(intloc_0)_&_Comput_(P,s,(n_+_1))_=_Exec_((a_:=_(intloc_0)),s)_) let n be Element of NAT ; ::_thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) ) assume n = 0 ; ::_thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) hence A16: Comput (P,s,n) = s by EXTPRO_1:2; ::_thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A1, A14, A2, PARTFUN1:def_6; ::_thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((a := (intloc 0)),s) by A16, A1, A14, A2, PARTFUN1:def_6 ; ::_thesis: verum end; A17: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_k_holds_ ((<%(a_:=_(intloc_0))%>_^_(k1_-->_(AddTo_(a,(intloc_0)))))_^_<%(halt_SCM+FSA)%>)_._i_=_AddTo_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < k implies ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i = AddTo (a,(intloc 0)) ) assume that A18: 1 <= i and A19: i < k ; ::_thesis: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i = AddTo (a,(intloc 0)) reconsider i1 = i - 1 as Element of NAT by A18, INT_1:5; i - 1 < k - 1 by A19, XREAL_1:9; then A20: i1 in k1 by A5, NAT_1:44; A21: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33; A22: len (k1 --> (AddTo (a,(intloc 0)))) = k1 by CARD_1:64; i in dom (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) by A19, A7, NAT_1:44; hence ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) . i by AFINSQ_1:def_3 .= (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A18, A19, A21, A22, A5, AFINSQ_1:18 .= AddTo (a,(intloc 0)) by A20, FUNCOP_1:7 ; ::_thesis: verum end; A23: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<_i_&_i_<_k_holds_ P_._i_=_AddTo_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 0 < i & i < k implies P . i = AddTo (a,(intloc 0)) ) assume that A24: 0 < i and A25: i < k ; ::_thesis: P . i = AddTo (a,(intloc 0)) A26: 0 + 1 <= i by A24, NAT_1:13; thus P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A12, A25 .= AddTo (a,(intloc 0)) by A17, A26, A25 ; ::_thesis: verum end; A27: for i being Element of NAT st i <= k holds IC (Comput (P,s,i)) = i proof defpred S1[ Nat] means ( $1 <= k implies IC (Comput (P,s,$1)) = $1 ); let i be Element of NAT ; ::_thesis: ( i <= k implies IC (Comput (P,s,i)) = i ) assume A28: i <= k ; ::_thesis: IC (Comput (P,s,i)) = i A29: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A30: S1[n] ; ::_thesis: S1[n + 1] assume A31: n + 1 <= k ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 then A32: n < k by NAT_1:13; percases ( n = 0 or n > 0 ) ; supposeA33: n = 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A15 .= succ n by A1, A33, SCMFSA_2:63 .= n + 1 by NAT_1:38 ; ::_thesis: verum end; supposeA34: n > 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 n + 0 <= n + 1 by XREAL_1:7; then A35: CurInstr (P,(Comput (P,s,n))) = P . n by A30, A31, A2, PARTFUN1:def_6, XXREAL_0:2 .= AddTo (a,(intloc 0)) by A23, A32, A34 ; A36: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((AddTo (a,(intloc 0))),(Comput (P,s,n))) by A35 ; thus IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by A36, SCMFSA_2:64 .= n + 1 by A30, A31, NAT_1:13, NAT_1:38 ; ::_thesis: verum end; end; end; A37: S1[ 0 ] by A1; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A37, A29); hence IC (Comput (P,s,i)) = i by A28; ::_thesis: verum end; k < k + (len <%(halt SCM+FSA)%>) by XREAL_1:29; then A38: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . k = <%(halt SCM+FSA)%> . (k - k) by A7, AFINSQ_1:18 .= halt SCM+FSA by AFINSQ_1:34 ; CurInstr (P,(Comput (P,s,k))) = P . (IC (Comput (P,s,k))) by A2, PARTFUN1:def_6 .= P . k by A27 .= halt SCM+FSA by A38, A12 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: verum end; supposeA39: k <= 0 ; ::_thesis: P halts_on s then reconsider mk = - k as Element of NAT by INT_1:3; consider k1 being Element of NAT such that A40: k1 + k = 1 and A41: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by A39, SCMFSA_7:def_1; A42: len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:17 .= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:34 .= (mk + 1) + 1 by A40, CARD_1:64 ; set f = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>; A43: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . 0 = (<%(a := (intloc 0))%> ^ ((k1 --> (SubFrom (a,(intloc 0)))) ^ <%(halt SCM+FSA)%>)) . 0 by AFINSQ_1:27 .= a := (intloc 0) by AFINSQ_1:35 ; A44: len ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) = (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) by AFINSQ_1:17 .= ((mk + 1) + 1) + 1 by A42, AFINSQ_1:34 ; A45: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<=_i_&_i_<=_(mk_+_1)_+_1_holds_ i_in_dom_((<%(a_:=_(intloc_0))%>_^_(k1_-->_(SubFrom_(a,(intloc_0)))))_^_<%(halt_SCM+FSA)%>) let i be Element of NAT ; ::_thesis: ( 0 <= i & i <= (mk + 1) + 1 implies i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) ) assume that 0 <= i and A46: i <= (mk + 1) + 1 ; ::_thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) i < ((mk + 1) + 1) + 1 by A46, NAT_1:13; hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by A44, NAT_1:44; ::_thesis: verum end; A47: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<=_i_&_i_<=_(mk_+_1)_+_1_holds_ P_._i_=_((<%(a_:=_(intloc_0))%>_^_(k1_-->_(SubFrom_(a,(intloc_0)))))_^_<%(halt_SCM+FSA)%>)_._i let i be Element of NAT ; ::_thesis: ( 0 <= i & i <= (mk + 1) + 1 implies P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i ) assume that 0 <= i and A48: i <= (mk + 1) + 1 ; ::_thesis: P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by A45, A48; hence P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A3, A41, GRFUNC_1:2; ::_thesis: verum end; then A49: P . 0 = a := (intloc 0) by A43; A50: now__::_thesis:_for_n_being_Element_of_NAT_st_n_=_0_holds_ (_Comput_(P,s,n)_=_s_&_CurInstr_(P,(Comput_(P,s,n)))_=_a_:=_(intloc_0)_&_Comput_(P,s,(n_+_1))_=_Exec_((a_:=_(intloc_0)),s)_) let n be Element of NAT ; ::_thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) ) assume n = 0 ; ::_thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) hence A51: Comput (P,s,n) = s by EXTPRO_1:2; ::_thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) hence CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) by A1, A49, A2, PARTFUN1:def_6; ::_thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((a := (intloc 0)),s) by A51, A1, A49, A2, PARTFUN1:def_6 ; ::_thesis: verum end; A52: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_(mk_+_1)_+_1_holds_ ((<%(a_:=_(intloc_0))%>_^_(k1_-->_(SubFrom_(a,(intloc_0)))))_^_<%(halt_SCM+FSA)%>)_._i_=_SubFrom_(a,(intloc_0)) A53: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33; let i be Element of NAT ; ::_thesis: ( 1 <= i & i < (mk + 1) + 1 implies ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i = SubFrom (a,(intloc 0)) ) assume that A54: 1 <= i and A55: i < (mk + 1) + 1 ; ::_thesis: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i = SubFrom (a,(intloc 0)) reconsider i1 = i - 1 as Element of NAT by A54, INT_1:5; i - 1 < (k1 + 1) - 1 by A55, A40, XREAL_1:9; then A56: i1 in k1 by NAT_1:44; A57: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 by CARD_1:64; i in dom (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) by A55, A42, NAT_1:44; hence ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) . i by AFINSQ_1:def_3 .= (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A40, A54, A55, A53, A57, AFINSQ_1:18 .= SubFrom (a,(intloc 0)) by A56, FUNCOP_1:7 ; ::_thesis: verum end; A58: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<_i_&_i_<_(mk_+_1)_+_1_holds_ P_._i_=_SubFrom_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 0 < i & i < (mk + 1) + 1 implies P . i = SubFrom (a,(intloc 0)) ) assume that A59: 0 < i and A60: i < (mk + 1) + 1 ; ::_thesis: P . i = SubFrom (a,(intloc 0)) A61: 0 + 1 <= i by A59, NAT_1:13; thus P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A47, A60 .= SubFrom (a,(intloc 0)) by A52, A61, A60 ; ::_thesis: verum end; A62: for i being Element of NAT st i <= (mk + 1) + 1 holds IC (Comput (P,s,i)) = i proof defpred S1[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (P,s,$1)) = $1 ); let i be Element of NAT ; ::_thesis: ( i <= (mk + 1) + 1 implies IC (Comput (P,s,i)) = i ) assume A63: i <= (mk + 1) + 1 ; ::_thesis: IC (Comput (P,s,i)) = i A64: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A65: S1[n] ; ::_thesis: S1[n + 1] assume A66: n + 1 <= (mk + 1) + 1 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 then A67: n < (mk + 1) + 1 by NAT_1:13; percases ( n = 0 or n > 0 ) ; supposeA68: n = 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A50 .= succ n by A1, A68, SCMFSA_2:63 .= n + 1 by NAT_1:38 ; ::_thesis: verum end; supposeA69: n > 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 n + 0 <= n + 1 by XREAL_1:7; then A70: CurInstr (P,(Comput (P,s,n))) = P . n by A65, A66, A2, PARTFUN1:def_6, XXREAL_0:2 .= SubFrom (a,(intloc 0)) by A58, A67, A69 ; A71: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((SubFrom (a,(intloc 0))),(Comput (P,s,n))) by A70 ; thus IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by A71, SCMFSA_2:65 .= n + 1 by A65, A66, NAT_1:13, NAT_1:38 ; ::_thesis: verum end; end; end; A72: S1[ 0 ] by A1; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A72, A64); hence IC (Comput (P,s,i)) = i by A63; ::_thesis: verum end; ( len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) <= (mk + 1) + 1 & (mk + 1) + 1 < (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) implies ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((mk + 1) + 1) = <%(halt SCM+FSA)%> . (((mk + 1) + 1) - (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))))) ) by AFINSQ_1:18; then A73: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((mk + 1) + 1) = halt SCM+FSA by A42, AFINSQ_1:34, XREAL_1:29; CurInstr (P,(Comput (P,s,((mk + 1) + 1)))) = P . (IC (Comput (P,s,((mk + 1) + 1)))) by A2, PARTFUN1:def_6 .= P . ((mk + 1) + 1) by A62 .= halt SCM+FSA by A73, A47 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: verum end; end; end; registration let a be Int-Location; let k be Integer; clustera := k -> parahalting ; correctness coherence a := k is parahalting ; proof A1: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15; let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds ( not a := k c= b1 or b1 halts_on s ) A2: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29; let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not a := k c= P or P halts_on s ) assume A3: a := k c= P ; ::_thesis: P halts_on s IC s = IC (Start-At (0,SCM+FSA)) by A2, A1, GRFUNC_1:2 .= 0 by FUNCOP_1:72 ; hence P halts_on s by Lm1, A3; ::_thesis: verum end; end; theorem :: SCMFSA7B:3 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for a being read-write Int-Location for k being Integer holds ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds (IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) ) proof let P be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA for a being read-write Int-Location for k being Integer holds ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds (IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) ) let s be State of SCM+FSA; ::_thesis: for a being read-write Int-Location for k being Integer holds ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds (IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) ) let a be read-write Int-Location; ::_thesis: for k being Integer holds ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds (IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) ) let k be Integer; ::_thesis: ( (IExec ((a := k),P,s)) . a = k & ( for b being read-write Int-Location st b <> a holds (IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) ) set s1 = s +* (Initialize ((intloc 0) .--> 1)); A1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:13, SCMFSA_M:10 .= 1 by SCMFSA_M:12 ; reconsider s1 = s +* (Initialize ((intloc 0) .--> 1)) as 0 -started State of SCM+FSA ; A2: a := k c= P +* (a := k) by FUNCT_4:25; thus (IExec ((a := k),P,s)) . a = (Result ((P +* (a := k)),s1)) . a .= k by A1, A2, SCMFSA_7:6 ; ::_thesis: ( ( for b being read-write Int-Location st b <> a holds (IExec ((a := k),P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f ) ) hereby ::_thesis: for f being FinSeq-Location holds (IExec ((a := k),P,s)) . f = s . f let b be read-write Int-Location; ::_thesis: ( b <> a implies (IExec ((a := k),P,s)) . b = s . b ) assume A3: b <> a ; ::_thesis: (IExec ((a := k),P,s)) . b = s . b ( b <> intloc 0 & b <> IC ) by SCMFSA_2:56; then A4: not b in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def_2; thus (IExec ((a := k),P,s)) . b = (Result ((P +* (a := k)),s1)) . b .= s1 . b by A1, A2, A3, SCMFSA_7:6 .= s . b by A4, FUNCT_4:11 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (IExec ((a := k),P,s)) . f = s . f ( f <> intloc 0 & f <> IC ) by SCMFSA_2:57, SCMFSA_2:58; then A5: not f in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def_2; thus (IExec ((a := k),P,s)) . f = (Result ((P +* (a := k)),s1)) . f .= s1 . f by A1, A2, SCMFSA_7:6 .= s . f by A5, FUNCT_4:11 ; ::_thesis: verum end; Lm2: for p1, p2, p3, p4 being XFinSequence holds ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) proof let p1, p2, p3, p4 be XFinSequence; ::_thesis: ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) thus ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 by AFINSQ_1:27 .= p1 ^ ((p2 ^ p3) ^ p4) by AFINSQ_1:27 ; ::_thesis: verum end; Lm3: for c0 being Element of NAT for s being b1 -started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i proof let c0 be Element of NAT ; ::_thesis: for s being c0 -started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i let s be c0 -started State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i let P be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i A1: dom P = NAT by PARTFUN1:def_2; A2: IC s = c0 by MEMSTR_0:def_12; let a be Int-Location; ::_thesis: for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i let k be Integer; ::_thesis: ( ( for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ) implies for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i ) assume A3: for c being Element of NAT st c < len (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) ; ::_thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i A4: for c being Element of NAT st c in dom (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (c0 + c) proof let c be Element of NAT ; ::_thesis: ( c in dom (aSeq (a,k)) implies (aSeq (a,k)) . c = P . (c0 + c) ) assume c in dom (aSeq (a,k)) ; ::_thesis: (aSeq (a,k)) . c = P . (c0 + c) then c < len (aSeq (a,k)) by AFINSQ_1:66; hence (aSeq (a,k)) . c = P . (c0 + c) by A3; ::_thesis: verum end; percases ( k > 0 or k <= 0 ) ; supposeA5: k > 0 ; ::_thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i then reconsider k9 = k as Element of NAT by INT_1:3; consider k1 being Element of NAT such that A6: k1 + 1 = k9 and A7: aSeq (a,k9) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) by A5, SCMFSA_7:def_2; defpred S1[ Nat] means ( $1 <= k9 implies IC (Comput (P,s,$1)) = c0 + $1 ); A8: len (aSeq (a,k9)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (AddTo (a,(intloc 0))))) by A7, AFINSQ_1:17 .= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:34 .= k9 by A6, CARD_1:64 ; for i being Element of NAT st i <= len (aSeq (a,k9)) holds IC (Comput (P,s,i)) = c0 + i proof A9: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_k9_holds_ (aSeq_(a,k9))_._i_=_AddTo_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < k9 implies (aSeq (a,k9)) . i = AddTo (a,(intloc 0)) ) assume that A10: 1 <= i and A11: i < k9 ; ::_thesis: (aSeq (a,k9)) . i = AddTo (a,(intloc 0)) reconsider i1 = i - 1 as Element of NAT by A10, INT_1:5; i = i1 + 1 ; then i1 < k1 by A11, A6, XREAL_1:6; then A12: i1 in k1 by NAT_1:44; A13: len (k1 --> (AddTo (a,(intloc 0)))) = k1 by CARD_1:64; len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33; hence (aSeq (a,k9)) . i = (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A10, A7, A13, A6, A11, AFINSQ_1:18 .= AddTo (a,(intloc 0)) by A12, FUNCOP_1:7 ; ::_thesis: verum end; A14: for i being Element of NAT st i < k9 holds i in dom (aSeq (a,k9)) by A8, NAT_1:44; A15: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<_i_&_i_<_k9_holds_ P_._(c0_+_i)_=_AddTo_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 0 < i & i < k9 implies P . (c0 + i) = AddTo (a,(intloc 0)) ) assume that A16: 0 < i and A17: i < k9 ; ::_thesis: P . (c0 + i) = AddTo (a,(intloc 0)) A18: 0 + 1 <= i by A16, NAT_1:13; thus P . (c0 + i) = (aSeq (a,k9)) . i by A4, A14, A17 .= AddTo (a,(intloc 0)) by A9, A18, A17 ; ::_thesis: verum end; A19: P . (c0 + 0) = (aSeq (a,k9)) . 0 by A3, A5, A8 .= a := (intloc 0) by A7, AFINSQ_1:35 ; A20: now__::_thesis:_for_n_being_Element_of_NAT_st_n_=_0_holds_ (_Comput_(P,s,n)_=_s_&_CurInstr_(P,(Comput_(P,s,n)))_=_a_:=_(intloc_0)_&_Comput_(P,s,(n_+_1))_=_Exec_((a_:=_(intloc_0)),s)_) let n be Element of NAT ; ::_thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) ) assume n = 0 ; ::_thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) hence A21: Comput (P,s,n) = s by EXTPRO_1:2; ::_thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def_6 .= a := (intloc 0) by A19, A21, MEMSTR_0:def_12 ; ::_thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((a := (intloc 0)),s) by A21, A2, A19, A1, PARTFUN1:def_6 ; ::_thesis: verum end; A22: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A23: S1[n] ; ::_thesis: S1[n + 1] assume A24: n + 1 <= k9 ; ::_thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1) percases ( n = 0 or n > 0 ) ; supposeA25: n = 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1) hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A20 .= (succ c0) + n by A2, A25, SCMFSA_2:63 .= (c0 + 1) + n by NAT_1:38 .= c0 + (n + 1) ; ::_thesis: verum end; supposeA26: n > 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1) A27: n < k9 by A24, NAT_1:13; A28: n + 0 <= n + 1 by XREAL_1:7; A29: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A23, A24, A28, A1, PARTFUN1:def_6, XXREAL_0:2 .= AddTo (a,(intloc 0)) by A15, A26, A27 ; A30: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((AddTo (a,(intloc 0))),(Comput (P,s,n))) by A29 ; thus IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by A30, SCMFSA_2:64 .= (c0 + n) + 1 by A23, A24, A28, NAT_1:38, XXREAL_0:2 .= c0 + (n + 1) ; ::_thesis: verum end; end; end; let i be Element of NAT ; ::_thesis: ( i <= len (aSeq (a,k9)) implies IC (Comput (P,s,i)) = c0 + i ) assume A31: i <= len (aSeq (a,k9)) ; ::_thesis: IC (Comput (P,s,i)) = c0 + i A32: S1[ 0 ] by A2; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A32, A22); hence IC (Comput (P,s,i)) = c0 + i by A8, A31; ::_thesis: verum end; hence for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i ; ::_thesis: verum end; supposeA33: k <= 0 ; ::_thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i then reconsider mk = - k as Element of NAT by INT_1:3; defpred S1[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (P,s,$1)) = c0 + $1 ); consider k1 being Element of NAT such that A34: k1 + k = 1 and A35: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by A33, SCMFSA_7:def_2; A36: len (aSeq (a,k)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by A35, AFINSQ_1:17 .= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:34 .= (mk + 1) + 1 by A34, CARD_1:64 ; for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i proof A37: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_<_(mk_+_1)_+_1_holds_ (aSeq_(a,k))_._i_=_SubFrom_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 1 <= i & i < (mk + 1) + 1 implies (aSeq (a,k)) . i = SubFrom (a,(intloc 0)) ) assume that A38: 1 <= i and A39: i < (mk + 1) + 1 ; ::_thesis: (aSeq (a,k)) . i = SubFrom (a,(intloc 0)) A40: i - 1 < ((mk + 1) + 1) - 1 by A39, XREAL_1:9; reconsider i1 = i - 1 as Element of NAT by A38, INT_1:5; A41: i1 in k1 by A34, A40, NAT_1:44; A42: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 by CARD_1:64; len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33; hence (aSeq (a,k)) . i = (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A35, A38, A42, A34, A39, AFINSQ_1:18 .= SubFrom (a,(intloc 0)) by A41, FUNCOP_1:7 ; ::_thesis: verum end; A43: for i being Element of NAT st i < (mk + 1) + 1 holds i in dom (aSeq (a,k)) by A36, NAT_1:44; A44: now__::_thesis:_for_i_being_Element_of_NAT_st_0_<_i_&_i_<_(mk_+_1)_+_1_holds_ P_._(c0_+_i)_=_SubFrom_(a,(intloc_0)) let i be Element of NAT ; ::_thesis: ( 0 < i & i < (mk + 1) + 1 implies P . (c0 + i) = SubFrom (a,(intloc 0)) ) assume that A45: 0 < i and A46: i < (mk + 1) + 1 ; ::_thesis: P . (c0 + i) = SubFrom (a,(intloc 0)) A47: 0 + 1 <= i by A45, NAT_1:13; thus P . (c0 + i) = (aSeq (a,k)) . i by A4, A43, A46 .= SubFrom (a,(intloc 0)) by A37, A47, A46 ; ::_thesis: verum end; A48: P . (c0 + 0) = (aSeq (a,k)) . 0 by A3, A36 .= a := (intloc 0) by A35, AFINSQ_1:35 ; A49: for n being Element of NAT st n = 0 holds ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) proof let n be Element of NAT ; ::_thesis: ( n = 0 implies ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) ) assume n = 0 ; ::_thesis: ( Comput (P,s,n) = s & CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) hence A50: Comput (P,s,n) = s by EXTPRO_1:2; ::_thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) ) thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def_6 .= a := (intloc 0) by A48, A50, MEMSTR_0:def_12 ; ::_thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((a := (intloc 0)),s) by A50, A2, A48, A1, PARTFUN1:def_6 ; ::_thesis: verum end; A51: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A52: S1[n] ; ::_thesis: S1[n + 1] assume A53: n + 1 <= (mk + 1) + 1 ; ::_thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1) percases ( n = 0 or n > 0 ) ; supposeA54: n = 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1) hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A49 .= succ (c0 + n) by A2, A54, SCMFSA_2:63 .= (c0 + n) + 1 by NAT_1:38 .= c0 + (n + 1) ; ::_thesis: verum end; supposeA55: n > 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1) A56: n < (mk + 1) + 1 by A53, NAT_1:13; A57: n + 0 <= n + 1 by XREAL_1:7; A58: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A52, A53, A57, A1, PARTFUN1:def_6, XXREAL_0:2 .= SubFrom (a,(intloc 0)) by A44, A55, A56 ; A59: Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3 .= Exec ((SubFrom (a,(intloc 0))),(Comput (P,s,n))) by A58 ; thus IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by A59, SCMFSA_2:65 .= (c0 + n) + 1 by A52, A53, A57, NAT_1:38, XXREAL_0:2 .= c0 + (n + 1) ; ::_thesis: verum end; end; end; let i be Element of NAT ; ::_thesis: ( i <= len (aSeq (a,k)) implies IC (Comput (P,s,i)) = c0 + i ) assume A60: i <= len (aSeq (a,k)) ; ::_thesis: IC (Comput (P,s,i)) = c0 + i A61: S1[ 0 ] by A2; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A61, A51); hence IC (Comput (P,s,i)) = c0 + i by A36, A60; ::_thesis: verum end; hence for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = c0 + i ; ::_thesis: verum end; end; end; Lm4: for s being 0 -started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st aSeq (a,k) c= P holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = i proof let s be 0 -started State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA for a being Int-Location for k being Integer st aSeq (a,k) c= P holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = i let P be Instruction-Sequence of SCM+FSA; ::_thesis: for a being Int-Location for k being Integer st aSeq (a,k) c= P holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = i let a be Int-Location; ::_thesis: for k being Integer st aSeq (a,k) c= P holds for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = i let k be Integer; ::_thesis: ( aSeq (a,k) c= P implies for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = i ) assume A1: aSeq (a,k) c= P ; ::_thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds IC (Comput (P,s,i)) = i A2: now__::_thesis:_for_c_being_Element_of_NAT_st_c_<_len_(aSeq_(a,k))_holds_ P_._(0_+_c)_=_(aSeq_(a,k))_._c let c be Element of NAT ; ::_thesis: ( c < len (aSeq (a,k)) implies P . (0 + c) = (aSeq (a,k)) . c ) assume c < len (aSeq (a,k)) ; ::_thesis: P . (0 + c) = (aSeq (a,k)) . c then c in dom (aSeq (a,k)) by NAT_1:44; hence P . (0 + c) = (aSeq (a,k)) . c by A1, GRFUNC_1:2; ::_thesis: verum end; let i be Element of NAT ; ::_thesis: ( i <= len (aSeq (a,k)) implies IC (Comput (P,s,i)) = i ) assume i <= len (aSeq (a,k)) ; ::_thesis: IC (Comput (P,s,i)) = i then IC (Comput (P,s,i)) = 0 + i by A2, Lm3; hence IC (Comput (P,s,i)) = i ; ::_thesis: verum end; Lm5: for s being 0 -started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds P halts_on s proof set a2 = intloc 2; set a1 = intloc 1; let s be 0 -started State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds P halts_on s let P be Instruction-Sequence of SCM+FSA; ::_thesis: for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds P halts_on s A1: dom P = NAT by PARTFUN1:def_2; set D = the InstructionsF of SCM+FSA; let f be FinSeq-Location ; ::_thesis: for p being FinSequence of INT st f := p c= P holds P halts_on s let p be FinSequence of INT ; ::_thesis: ( f := p c= P implies P halts_on s ) set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; set q0 = (aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>; assume A2: f := p c= P ; ::_thesis: P halts_on s set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; A3: now__::_thesis:_for_i,_k_being_Element_of_NAT_st_i_<_len_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(aSeq_(f,p)))_^_<%(halt_SCM+FSA)%>)_holds_ P_._i_=_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(aSeq_(f,p)))_^_<%(halt_SCM+FSA)%>)_._i let i, k be Element of NAT ; ::_thesis: ( i < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) implies P . i = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i ) assume i < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) ; ::_thesis: P . i = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i then A4: i in dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by NAT_1:44; thus P . i = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i by A2, A4, GRFUNC_1:2; ::_thesis: verum end; consider pp being XFinSequence of such that A5: ( len pp = len p & ( for k being Element of NAT st k < len pp holds ex i being Integer st ( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) ) and A6: aSeq (f,p) = FlattenSeq pp by SCMFSA_7:def_3; len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) = (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) + 1 by A6, AFINSQ_1:75; then A7: len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by NAT_1:13; defpred S1[ XFinSequence] means ( $1 c= pp implies ex pp0 being XFinSequence of st ( pp0 = $1 & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds IC (Comput (P,s,i)) = i ) ) ); A8: for r being XFinSequence for x being set st S1[r] holds S1[r ^ <%x%>] proof let r be XFinSequence; ::_thesis: for x being set st S1[r] holds S1[r ^ <%x%>] let x be set ; ::_thesis: ( S1[r] implies S1[r ^ <%x%>] ) assume A9: S1[r] ; ::_thesis: S1[r ^ <%x%>] set r1 = len r; len <%x%> = 1 by AFINSQ_1:34; then len (r ^ <%x%>) = (len r) + 1 by AFINSQ_1:17; then len r < len (r ^ <%x%>) by XREAL_1:29; then A10: len r in dom (r ^ <%x%>) by NAT_1:44; assume A11: r ^ <%x%> c= pp ; ::_thesis: ex pp0 being XFinSequence of st ( pp0 = r ^ <%x%> & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds IC (Comput (P,s,i)) = i ) ) then A12: dom (r ^ <%x%>) c= dom pp by GRFUNC_1:2; then len r < len pp by A10, NAT_1:44; then consider pr1 being Integer such that pr1 = p . ((len r) + 1) and A13: pp . (len r) = ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%> by A5; r c= r ^ <%x%> by AFINSQ_1:74; then consider pp0 being XFinSequence of such that A14: pp0 = r and A15: for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds IC (Comput (P,s,i)) = i by A9, A11, XBOOLE_1:1; set c2 = len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))); set c1 = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)); IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) by A15; then reconsider s1 = Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) as len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) -started State of SCM+FSA by MEMSTR_0:def_12; A16: x = (r ^ <%x%>) . (len r) by AFINSQ_1:36 .= pp . (len r) by A11, A10, GRFUNC_1:2 ; then x in the InstructionsF of SCM+FSA ^omega by A10, A12, FUNCT_1:102; then reconsider pp1 = pp0 ^ <%x%> as XFinSequence of ; take pp1 ; ::_thesis: ( pp1 = r ^ <%x%> & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds IC (Comput (P,s,i)) = i ) ) thus pp1 = r ^ <%x%> by A14; ::_thesis: for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds IC (Comput (P,s,i)) = i reconsider x = x as Element of the InstructionsF of SCM+FSA ^omega by A10, A12, A16, FUNCT_1:102; A17: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <%x%>) by AFINSQ_2:75 .= (FlattenSeq pp0) ^ x by AFINSQ_2:73 ; set s2 = Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))); A18: x = (aSeq ((intloc 1),((len r) + 1))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>) by A13, A16, AFINSQ_1:27; then A19: (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) = (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>))) by A17, AFINSQ_1:27 .= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>))) by AFINSQ_1:17 .= len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>)) by Lm2 .= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>)) by AFINSQ_1:17 .= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ((len (aSeq ((intloc 2),pr1))) + (len <%((f,(intloc 1)) := (intloc 2))%>)) by AFINSQ_1:17 .= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ((len (aSeq ((intloc 2),pr1))) + 1) by AFINSQ_1:34 .= ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 1 ; then A20: len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) = ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 1 by AFINSQ_1:17; then A21: len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) > (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) by NAT_1:13; A22: FlattenSeq pp1 c= FlattenSeq pp by A11, A14, AFINSQ_2:82; A23: now__::_thesis:_for_p_being_XFinSequence_st_p_c=_x_holds_ (((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_^_p_c=_(((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(aSeq_(f,p)))_^_<%(halt_SCM+FSA)%> let p be XFinSequence; ::_thesis: ( p c= x implies (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> ) assume p c= x ; ::_thesis: (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> then (FlattenSeq pp0) ^ p c= (FlattenSeq pp0) ^ x by AFINSQ_2:81; then (FlattenSeq pp0) ^ p c= FlattenSeq pp by A22, A17, XBOOLE_1:1; then ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((FlattenSeq pp0) ^ p) c= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp) by AFINSQ_2:81; then A24: (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp) by AFINSQ_1:27; ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by A6, AFINSQ_1:74; hence (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by A24, XBOOLE_1:1; ::_thesis: verum end; A25: for c being Element of NAT st c < len (aSeq ((intloc 1),((len r) + 1))) holds (aSeq ((intloc 1),((len r) + 1))) . c = P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) proof let c be Element of NAT ; ::_thesis: ( c < len (aSeq ((intloc 1),((len r) + 1))) implies (aSeq ((intloc 1),((len r) + 1))) . c = P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) ) assume c < len (aSeq ((intloc 1),((len r) + 1))) ; ::_thesis: (aSeq ((intloc 1),((len r) + 1))) . c = P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) then A26: c in dom (aSeq ((intloc 1),((len r) + 1))) by AFINSQ_1:66; then A27: (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c in dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) by AFINSQ_1:23; A28: (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by A18, A23, AFINSQ_1:74; then A29: dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) c= dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by GRFUNC_1:2; thus (aSeq ((intloc 1),((len r) + 1))) . c = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by A26, AFINSQ_1:def_3 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by A28, A27, GRFUNC_1:2 .= P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by A2, A29, A27, GRFUNC_1:2 ; ::_thesis: verum end; set c3 = len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))); A30: len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) = (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (aSeq ((intloc 1),((len r) + 1)))) by AFINSQ_1:17; A31: ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1) = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x by A17, AFINSQ_1:27; then len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by A23, NAT_1:43; then A32: (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by A20, NAT_1:13; A33: len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) = (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) by AFINSQ_1:17; A34: Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))) = Comput (P,s1,(len (aSeq ((intloc 1),((len r) + 1))))) by A30, EXTPRO_1:4; IC (Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))))) = len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) by A30, A34, A25, Lm3; then reconsider s2 = Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))) as len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) -started State of SCM+FSA by MEMSTR_0:def_12; A35: for c being Element of NAT st c < len (aSeq ((intloc 2),pr1)) holds (aSeq ((intloc 2),pr1)) . c = P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) proof let c be Element of NAT ; ::_thesis: ( c < len (aSeq ((intloc 2),pr1)) implies (aSeq ((intloc 2),pr1)) . c = P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) ) assume c < len (aSeq ((intloc 2),pr1)) ; ::_thesis: (aSeq ((intloc 2),pr1)) . c = P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) then A36: c in dom (aSeq ((intloc 2),pr1)) by AFINSQ_1:66; then A37: (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c in dom (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) by AFINSQ_1:23; (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by A13, A16, A23, AFINSQ_1:74; then A38: ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)) c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by AFINSQ_1:27; then A39: dom (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) c= dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by GRFUNC_1:2; thus (aSeq ((intloc 2),pr1)) . c = (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) by A36, AFINSQ_1:def_3 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) by A37, A38, GRFUNC_1:2 .= P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) by A2, A39, A37, GRFUNC_1:2 ; ::_thesis: verum end; A40: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_len_(aSeq_((intloc_2),pr1))_holds_ (len_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_^_(aSeq_((intloc_1),((len_r)_+_1)))))_+_i_=_IC_(Comput_(P,s,((len_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_^_(aSeq_((intloc_1),((len_r)_+_1)))))_+_i))) let i be Element of NAT ; ::_thesis: ( i <= len (aSeq ((intloc 2),pr1)) implies (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i = IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i))) ) assume i <= len (aSeq ((intloc 2),pr1)) ; ::_thesis: (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i = IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i))) hence (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i = IC (Comput (P,s2,i)) by A35, Lm3 .= IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + i))) by EXTPRO_1:4 ; ::_thesis: verum end; A41: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_len_(aSeq_((intloc_1),((len_r)_+_1)))_holds_ (len_(((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0)))_+_i_=_IC_(Comput_(P,s,((len_(((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0)))_+_i))) let i be Element of NAT ; ::_thesis: ( i <= len (aSeq ((intloc 1),((len r) + 1))) implies (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) ) assume i <= len (aSeq ((intloc 1),((len r) + 1))) ; ::_thesis: (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) hence (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i = IC (Comput (P,s1,i)) by A25, Lm3 .= IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + i))) by EXTPRO_1:4 ; ::_thesis: verum end; A42: for i being Element of NAT st i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds IC (Comput (P,s,i)) = i proof let i be Element of NAT ; ::_thesis: ( i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) implies IC (Comput (P,s,i)) = i ) assume A43: i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; ::_thesis: IC (Comput (P,s,i)) = i A44: now__::_thesis:_(_not_i_<=_len_(((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_&_(_not_(len_(((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0)))_+_1_<=_i_or_not_i_<=_len_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_^_(aSeq_((intloc_1),((len_r)_+_1))))_)_implies_(_(len_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_^_(aSeq_((intloc_1),((len_r)_+_1)))))_+_1_<=_i_&_i_<=_(len_((((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_^_(FlattenSeq_pp0))_^_(aSeq_((intloc_1),((len_r)_+_1)))))_+_(len_(aSeq_((intloc_2),pr1)))_)_) A45: i < (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) by A43, AFINSQ_1:17; assume A46: not i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ; ::_thesis: ( ( not (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) implies ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) ) assume ( not (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) ; ::_thesis: ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) hence ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) by A19, A46, A45, NAT_1:13; ::_thesis: verum end; percases ( i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) or ( (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) or ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) ) by A44; suppose i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ; ::_thesis: IC (Comput (P,s,i)) = i hence IC (Comput (P,s,i)) = i by A15; ::_thesis: verum end; supposeA47: ( (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ) ; ::_thesis: IC (Comput (P,s,i)) = i then ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1) - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) <= i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) by XREAL_1:9; then reconsider ii = i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) as Element of NAT by INT_1:3; i - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) - (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) by A47, XREAL_1:9; hence i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ii))) by A30, A41 .= IC (Comput (P,s,i)) ; ::_thesis: verum thus verum ; ::_thesis: verum end; supposeA48: ( (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1 <= i & i <= (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) ) ; ::_thesis: IC (Comput (P,s,i)) = i then ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + 1) - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) <= i - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) by XREAL_1:9; then reconsider ii = i - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) as Element of NAT by INT_1:3; i - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) <= ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) - (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) by A48, XREAL_1:9; hence i = IC (Comput (P,s,((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + ii))) by A40 .= IC (Comput (P,s,i)) ; ::_thesis: verum end; end; end; (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x c= (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by A23; then consider rq being XFinSequence of such that A49: ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) ^ rq = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> by AFINSQ_2:80; len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) = ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1)))) + 1 by A19, AFINSQ_1:17; then A50: len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) > (len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) by NAT_1:13; then A51: len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) in dom ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) by A31, A33, AFINSQ_1:66; dom <%((f,(intloc 1)) := (intloc 2))%> = 1 by AFINSQ_1:33; then A52: 0 in dom <%((f,(intloc 1)) := (intloc 2))%> by CARD_1:49, TARSKI:def_1; len <%((f,(intloc 1)) := (intloc 2))%> = 1 by AFINSQ_1:34; then len (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) = (len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 1 by AFINSQ_1:17; then len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) < len (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) by XREAL_1:29; then A53: len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) in dom (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) by AFINSQ_1:66; A54: len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))) = ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (aSeq ((intloc 1),((len r) + 1))))) + (len (aSeq ((intloc 2),pr1))) by A30, AFINSQ_1:17; A55: P /. (IC (Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = P . (IC (Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) by A1, PARTFUN1:def_6; CurInstr (P,(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = P . (len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))) by A33, A42, A55, A50 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . (len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))) by A3, A33, A32 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ((len (aSeq ((intloc 1),((len r) + 1)))) + (len (aSeq ((intloc 2),pr1))))) by A54, A51, A49, AFINSQ_1:def_3 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))))) by AFINSQ_1:17 ; then A56: CurInstr (P,(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) = (((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%>) . ((len ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1)))) + 0) by A53, A13, A16, AFINSQ_1:def_3 .= <%((f,(intloc 1)) := (intloc 2))%> . 0 by A52, AFINSQ_1:def_3 .= (f,(intloc 1)) := (intloc 2) by AFINSQ_1:34 ; Comput (P,s,((len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))) + 1)) = Following (P,(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) by EXTPRO_1:3 .= Exec (((f,(intloc 1)) := (intloc 2)),(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) by A56 ; then A57: IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) = (Exec (((f,(intloc 1)) := (intloc 2)),(Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))))))) . (IC ) by A20, AFINSQ_1:17 .= succ (IC (Comput (P,s,(len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1))))))) by SCMFSA_2:73 .= succ (len (((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))) ^ (aSeq ((intloc 2),pr1)))) by A33, A42, A21 ; thus for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) holds IC (Comput (P,s,i)) = i ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) implies IC (Comput (P,s,i)) = i ) assume A58: i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; ::_thesis: IC (Comput (P,s,i)) = i percases ( i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) or i = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ) by A58, XXREAL_0:1; suppose i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; ::_thesis: IC (Comput (P,s,i)) = i hence IC (Comput (P,s,i)) = i by A42; ::_thesis: verum end; suppose i = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; ::_thesis: IC (Comput (P,s,i)) = i hence IC (Comput (P,s,i)) = i by A33, A20, A57, NAT_1:38; ::_thesis: verum end; end; end; end; set k = len (aSeq ((intloc 1),(len p))); A59: len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) = (len (aSeq ((intloc 1),(len p)))) + 1 by AFINSQ_1:75; (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> = ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((aSeq (f,p)) ^ <%(halt SCM+FSA)%>) by AFINSQ_1:27 .= (aSeq ((intloc 1),(len p))) ^ (<%(f :=<0,...,0> (intloc 1))%> ^ ((aSeq (f,p)) ^ <%(halt SCM+FSA)%>)) by AFINSQ_1:27 ; then A60: aSeq ((intloc 1),(len p)) c= f := p by AFINSQ_1:74; A61: S1[ {} ] proof assume {} c= pp ; ::_thesis: ex pp0 being XFinSequence of st ( pp0 = {} & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds IC (Comput (P,s,i)) = i ) ) take <%> ( the InstructionsF of SCM+FSA ^omega) ; ::_thesis: ( <%> ( the InstructionsF of SCM+FSA ^omega) = {} & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)))) holds IC (Comput (P,s,i)) = i ) ) thus <%> ( the InstructionsF of SCM+FSA ^omega) = {} ; ::_thesis: for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)))) holds IC (Comput (P,s,i)) = i A62: (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> = ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((aSeq (f,p)) ^ <%(halt SCM+FSA)%>) by AFINSQ_1:27; then len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) = (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len ((aSeq (f,p)) ^ <%(halt SCM+FSA)%>)) by AFINSQ_1:17; then len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) <= len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by NAT_1:11; then A63: len (aSeq ((intloc 1),(len p))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by A59, NAT_1:13; A64: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_holds_ IC_(Comput_(P,s,i))_=_i let i be Element of NAT ; ::_thesis: ( i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies IC (Comput (P,s,i)) = i ) assume i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ; ::_thesis: IC (Comput (P,s,i)) = i then i <= len (aSeq ((intloc 1),(len p))) by A59, NAT_1:13; hence IC (Comput (P,s,i)) = i by A2, A60, Lm4, XBOOLE_1:1; ::_thesis: verum end; A65: len (aSeq ((intloc 1),(len p))) < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A59, NAT_1:13; then A66: len (aSeq ((intloc 1),(len p))) in dom ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by AFINSQ_1:66; A67: IC (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) = len (aSeq ((intloc 1),(len p))) by A64, A65; then A68: CurInstr (P,(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) = P . (len (aSeq ((intloc 1),(len p)))) by A1, PARTFUN1:def_6 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . (len (aSeq ((intloc 1),(len p)))) by A3, A63 .= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) . (len (aSeq ((intloc 1),(len p)))) by A62, A66, AFINSQ_1:def_3 .= f :=<0,...,0> (intloc 1) by AFINSQ_1:36 ; A69: Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>))) = Following (P,(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) by A59, EXTPRO_1:3 .= Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) by A68 ; A70: IC (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) = succ (IC (Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) by A69, SCMFSA_2:75 .= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A59, A67, NAT_1:38 ; A71: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_len_((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>)_holds_ IC_(Comput_(P,s,i))_=_i let i be Element of NAT ; ::_thesis: ( i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies IC (Comput (P,s,i)) = i ) assume i <= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ; ::_thesis: IC (Comput (P,s,i)) = i then ( i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) or i = len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ) by XXREAL_0:1; hence IC (Comput (P,s,i)) = i by A64, A70; ::_thesis: verum end; ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega))) = ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (<%> the InstructionsF of SCM+FSA) by AFINSQ_2:74 .= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ {} .= (aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%> ; hence for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)))) holds IC (Comput (P,s,i)) = i by A71; ::_thesis: verum end; for r being XFinSequence holds S1[r] from AFINSQ_1:sch_3(A61, A8); then ex pp0 being XFinSequence of st ( pp0 = pp & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) holds IC (Comput (P,s,i)) = i ) ) ; then IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) = len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) ; then CurInstr (P,(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) = P . (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) by A1, PARTFUN1:def_6 .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . (len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) by A3, A7 .= halt SCM+FSA by A6, AFINSQ_1:36 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: verum end; registration let f be FinSeq-Location ; let p be FinSequence of INT ; clusterf := p -> non empty initial ; coherence ( f := p is initial & not f := p is empty & f := p is NAT -defined & f := p is the InstructionsF of SCM+FSA -valued ) ; end; registration let f be FinSeq-Location ; let p be FinSequence of INT ; clusterf := p -> parahalting ; correctness coherence f := p is parahalting ; proof let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds ( not f := p c= b1 or b1 halts_on s ) let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not f := p c= P or P halts_on s ) assume A1: f := p c= P ; ::_thesis: P halts_on s thus P halts_on s by Lm5, A1; ::_thesis: verum end; end; theorem :: SCMFSA7B:4 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for f being FinSeq-Location for p being FinSequence of INT holds ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds (IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g ) ) proof let P be Instruction-Sequence of SCM+FSA; ::_thesis: for s being State of SCM+FSA for f being FinSeq-Location for p being FinSequence of INT holds ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds (IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g ) ) let s be State of SCM+FSA; ::_thesis: for f being FinSeq-Location for p being FinSequence of INT holds ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds (IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g ) ) let f be FinSeq-Location ; ::_thesis: for p being FinSequence of INT holds ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds (IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g ) ) let p be FinSequence of INT ; ::_thesis: ( (IExec ((f := p),P,s)) . f = p & ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds (IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g ) ) A1: (s +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by FUNCT_4:13, SCMFSA_M:10 .= 1 by SCMFSA_M:12 ; reconsider s1 = s +* (Initialize ((intloc 0) .--> 1)) as 0 -started State of SCM+FSA ; A2: f := p c= P +* (f := p) by FUNCT_4:25; thus (IExec ((f := p),P,s)) . f = (Result ((P +* (f := p)),s1)) . f .= p by A1, A2, SCMFSA_7:7 ; ::_thesis: ( ( for a being read-write Int-Location st a <> intloc 1 & a <> intloc 2 holds (IExec ((f := p),P,s)) . a = s . a ) & ( for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g ) ) hereby ::_thesis: for g being FinSeq-Location st g <> f holds (IExec ((f := p),P,s)) . g = s . g let a be read-write Int-Location; ::_thesis: ( a <> intloc 1 & a <> intloc 2 implies (IExec ((f := p),P,s)) . a = s . a ) ( a <> intloc 0 & a <> IC ) by SCMFSA_2:56; then A3: not a in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def_2; assume A4: ( a <> intloc 1 & a <> intloc 2 ) ; ::_thesis: (IExec ((f := p),P,s)) . a = s . a thus (IExec ((f := p),P,s)) . a = (Result ((P +* (f := p)),(s +* (Initialize ((intloc 0) .--> 1))))) . a .= s1 . a by A1, A2, A4, SCMFSA_7:7 .= s . a by A3, FUNCT_4:11 ; ::_thesis: verum end; let g be FinSeq-Location ; ::_thesis: ( g <> f implies (IExec ((f := p),P,s)) . g = s . g ) assume A5: g <> f ; ::_thesis: (IExec ((f := p),P,s)) . g = s . g ( g <> intloc 0 & g <> IC ) by SCMFSA_2:57, SCMFSA_2:58; then A6: not g in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA_M:11, TARSKI:def_2; thus (IExec ((f := p),P,s)) . g = (Result ((P +* (f := p)),(s +* (Initialize ((intloc 0) .--> 1))))) . g .= s1 . g by A1, A2, A5, SCMFSA_7:7 .= s . g by A6, FUNCT_4:11 ; ::_thesis: verum end; definition let i be Instruction of SCM+FSA; let a be Int-Location; predi refers a means :: SCMFSA7B:def 1 not for b being Int-Location for l being Element of NAT for f being FinSeq-Location holds ( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ); end; :: deftheorem defines refers SCMFSA7B:def_1_:_ for i being Instruction of SCM+FSA for a being Int-Location holds ( i refers a iff not for b being Int-Location for l being Element of NAT for f being FinSeq-Location holds ( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ) ); definition let I be preProgram of SCM+FSA; let a be Int-Location; predI refers a means :: SCMFSA7B:def 2 ex i being Instruction of SCM+FSA st ( i in rng I & i refers a ); end; :: deftheorem defines refers SCMFSA7B:def_2_:_ for I being preProgram of SCM+FSA for a being Int-Location holds ( I refers a iff ex i being Instruction of SCM+FSA st ( i in rng I & i refers a ) ); definition let i be Instruction of SCM+FSA; let a be Int-Location; predi destroys a means :Def3: :: SCMFSA7B:def 3 not for b being Int-Location for f being FinSeq-Location holds ( a := b <> i & AddTo (a,b) <> i & SubFrom (a,b) <> i & MultBy (a,b) <> i & Divide (a,b) <> i & Divide (b,a) <> i & a := (f,b) <> i & a :=len f <> i ); end; :: deftheorem Def3 defines destroys SCMFSA7B:def_3_:_ for i being Instruction of SCM+FSA for a being Int-Location holds ( i destroys a iff not for b being Int-Location for f being FinSeq-Location holds ( a := b <> i & AddTo (a,b) <> i & SubFrom (a,b) <> i & MultBy (a,b) <> i & Divide (a,b) <> i & Divide (b,a) <> i & a := (f,b) <> i & a :=len f <> i ) ); definition let I be NAT -defined the InstructionsF of SCM+FSA -valued Function; let a be Int-Location; predI destroys a means :Def4: :: SCMFSA7B:def 4 ex i being Instruction of SCM+FSA st ( i in rng I & i destroys a ); end; :: deftheorem Def4 defines destroys SCMFSA7B:def_4_:_ for I being NAT -defined the InstructionsF of SCM+FSA -valued Function for a being Int-Location holds ( I destroys a iff ex i being Instruction of SCM+FSA st ( i in rng I & i destroys a ) ); definition let I be NAT -defined the InstructionsF of SCM+FSA -valued Function; attrI is good means :Def5: :: SCMFSA7B:def 5 not I destroys intloc 0; end; :: deftheorem Def5 defines good SCMFSA7B:def_5_:_ for I being NAT -defined the InstructionsF of SCM+FSA -valued Function holds ( I is good iff not I destroys intloc 0 ); theorem Th5: :: SCMFSA7B:5 for a being Int-Location holds not halt SCM+FSA destroys a proof let a be Int-Location; ::_thesis: not halt SCM+FSA destroys a for b being Int-Location for l being Element of NAT for f being FinSeq-Location holds ( a := b <> halt SCM+FSA & AddTo (a,b) <> halt SCM+FSA & SubFrom (a,b) <> halt SCM+FSA & MultBy (a,b) <> halt SCM+FSA & Divide (a,b) <> halt SCM+FSA & Divide (b,a) <> halt SCM+FSA & a := (f,b) <> halt SCM+FSA & a :=len f <> halt SCM+FSA ) ; hence not halt SCM+FSA destroys a by Def3; ::_thesis: verum end; theorem Th6: :: SCMFSA7B:6 for a, b, c being Int-Location st a <> b holds not b := c destroys a proof let a, b, c be Int-Location; ::_thesis: ( a <> b implies not b := c destroys a ) assume A1: a <> b ; ::_thesis: not b := c destroys a now__::_thesis:_for_e_being_Int-Location for_l_being_Element_of_NAT_ for_f_being_FinSeq-Location_holds_ (_a_:=_e_<>_b_:=_c_&_AddTo_(a,e)_<>_b_:=_c_&_SubFrom_(a,e)_<>_b_:=_c_&_MultBy_(a,e)_<>_b_:=_c_&_Divide_(a,e)_<>_b_:=_c_&_Divide_(e,a)_<>_b_:=_c_&_a_:=_(f,e)_<>_b_:=_c_&_a_:=len_f_<>_b_:=_c_) let e be Int-Location; ::_thesis: for l being Element of NAT for f being FinSeq-Location holds ( a := e <> b := c & AddTo (a,e) <> b := c & SubFrom (a,e) <> b := c & MultBy (a,e) <> b := c & Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) let l be Element of NAT ; ::_thesis: for f being FinSeq-Location holds ( a := e <> b := c & AddTo (a,e) <> b := c & SubFrom (a,e) <> b := c & MultBy (a,e) <> b := c & Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) let f be FinSeq-Location ; ::_thesis: ( a := e <> b := c & AddTo (a,e) <> b := c & SubFrom (a,e) <> b := c & MultBy (a,e) <> b := c & Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) thus a := e <> b := c by A1, SF_MASTR:1; ::_thesis: ( AddTo (a,e) <> b := c & SubFrom (a,e) <> b := c & MultBy (a,e) <> b := c & Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) A2: InsCode (b := c) = 1 by SCMFSA_2:18; hence AddTo (a,e) <> b := c by SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> b := c & MultBy (a,e) <> b := c & Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) thus SubFrom (a,e) <> b := c by A2, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> b := c & Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) thus MultBy (a,e) <> b := c by A2, SCMFSA_2:21; ::_thesis: ( Divide (a,e) <> b := c & Divide (e,a) <> b := c & a := (f,e) <> b := c & a :=len f <> b := c ) thus ( Divide (a,e) <> b := c & Divide (e,a) <> b := c ) by A2, SCMFSA_2:22; ::_thesis: ( a := (f,e) <> b := c & a :=len f <> b := c ) thus a := (f,e) <> b := c by A2, SCMFSA_2:26; ::_thesis: a :=len f <> b := c thus a :=len f <> b := c by A2, SCMFSA_2:28; ::_thesis: verum end; hence not b := c destroys a by Def3; ::_thesis: verum end; theorem Th7: :: SCMFSA7B:7 for a, b, c being Int-Location st a <> b holds not AddTo (b,c) destroys a proof let a, b, c be Int-Location; ::_thesis: ( a <> b implies not AddTo (b,c) destroys a ) assume A1: a <> b ; ::_thesis: not AddTo (b,c) destroys a now__::_thesis:_for_e_being_Int-Location for_l_being_Element_of_NAT_ for_f_being_FinSeq-Location_holds_ (_a_:=_e_<>_AddTo_(b,c)_&_AddTo_(a,e)_<>_AddTo_(b,c)_&_SubFrom_(a,e)_<>_AddTo_(b,c)_&_MultBy_(a,e)_<>_AddTo_(b,c)_&_Divide_(a,e)_<>_AddTo_(b,c)_&_Divide_(e,a)_<>_AddTo_(b,c)_&_a_:=_(f,e)_<>_AddTo_(b,c)_&_a_:=len_f_<>_AddTo_(b,c)_) let e be Int-Location; ::_thesis: for l being Element of NAT for f being FinSeq-Location holds ( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) let l be Element of NAT ; ::_thesis: for f being FinSeq-Location holds ( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) let f be FinSeq-Location ; ::_thesis: ( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) A2: InsCode (AddTo (b,c)) = 2 by SCMFSA_2:19; hence a := e <> AddTo (b,c) by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) thus AddTo (a,e) <> AddTo (b,c) by A1, SF_MASTR:2; ::_thesis: ( SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) thus SubFrom (a,e) <> AddTo (b,c) by A2, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) thus MultBy (a,e) <> AddTo (b,c) by A2, SCMFSA_2:21; ::_thesis: ( Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) thus ( Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) ) by A2, SCMFSA_2:22; ::_thesis: ( a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) ) thus a := (f,e) <> AddTo (b,c) by A2, SCMFSA_2:26; ::_thesis: a :=len f <> AddTo (b,c) thus a :=len f <> AddTo (b,c) by A2, SCMFSA_2:28; ::_thesis: verum end; hence not AddTo (b,c) destroys a by Def3; ::_thesis: verum end; theorem Th8: :: SCMFSA7B:8 for a, b, c being Int-Location st a <> b holds not SubFrom (b,c) destroys a proof let a, b, c be Int-Location; ::_thesis: ( a <> b implies not SubFrom (b,c) destroys a ) assume A1: a <> b ; ::_thesis: not SubFrom (b,c) destroys a now__::_thesis:_for_e_being_Int-Location for_l_being_Element_of_NAT_ for_f_being_FinSeq-Location_holds_ (_a_:=_e_<>_SubFrom_(b,c)_&_AddTo_(a,e)_<>_SubFrom_(b,c)_&_SubFrom_(a,e)_<>_SubFrom_(b,c)_&_MultBy_(a,e)_<>_SubFrom_(b,c)_&_Divide_(a,e)_<>_SubFrom_(b,c)_&_Divide_(e,a)_<>_SubFrom_(b,c)_&_a_:=_(f,e)_<>_SubFrom_(b,c)_&_a_:=len_f_<>_SubFrom_(b,c)_) let e be Int-Location; ::_thesis: for l being Element of NAT for f being FinSeq-Location holds ( a := e <> SubFrom (b,c) & AddTo (a,e) <> SubFrom (b,c) & SubFrom (a,e) <> SubFrom (b,c) & MultBy (a,e) <> SubFrom (b,c) & Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) let l be Element of NAT ; ::_thesis: for f being FinSeq-Location holds ( a := e <> SubFrom (b,c) & AddTo (a,e) <> SubFrom (b,c) & SubFrom (a,e) <> SubFrom (b,c) & MultBy (a,e) <> SubFrom (b,c) & Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) let f be FinSeq-Location ; ::_thesis: ( a := e <> SubFrom (b,c) & AddTo (a,e) <> SubFrom (b,c) & SubFrom (a,e) <> SubFrom (b,c) & MultBy (a,e) <> SubFrom (b,c) & Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) A2: InsCode (SubFrom (b,c)) = 3 by SCMFSA_2:20; hence a := e <> SubFrom (b,c) by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> SubFrom (b,c) & SubFrom (a,e) <> SubFrom (b,c) & MultBy (a,e) <> SubFrom (b,c) & Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) thus AddTo (a,e) <> SubFrom (b,c) by A2, SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> SubFrom (b,c) & MultBy (a,e) <> SubFrom (b,c) & Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) thus SubFrom (a,e) <> SubFrom (b,c) by A1, SF_MASTR:3; ::_thesis: ( MultBy (a,e) <> SubFrom (b,c) & Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) thus MultBy (a,e) <> SubFrom (b,c) by A2, SCMFSA_2:21; ::_thesis: ( Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) & a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) thus ( Divide (a,e) <> SubFrom (b,c) & Divide (e,a) <> SubFrom (b,c) ) by A2, SCMFSA_2:22; ::_thesis: ( a := (f,e) <> SubFrom (b,c) & a :=len f <> SubFrom (b,c) ) thus a := (f,e) <> SubFrom (b,c) by A2, SCMFSA_2:26; ::_thesis: a :=len f <> SubFrom (b,c) thus a :=len f <> SubFrom (b,c) by A2, SCMFSA_2:28; ::_thesis: verum end; hence not SubFrom (b,c) destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:9 for a, b, c being Int-Location st a <> b holds not MultBy (b,c) destroys a proof let a, b, c be Int-Location; ::_thesis: ( a <> b implies not MultBy (b,c) destroys a ) assume A1: a <> b ; ::_thesis: not MultBy (b,c) destroys a now__::_thesis:_for_e_being_Int-Location for_l_being_Element_of_NAT_ for_f_being_FinSeq-Location_holds_ (_a_:=_e_<>_MultBy_(b,c)_&_AddTo_(a,e)_<>_MultBy_(b,c)_&_SubFrom_(a,e)_<>_MultBy_(b,c)_&_MultBy_(a,e)_<>_MultBy_(b,c)_&_Divide_(a,e)_<>_MultBy_(b,c)_&_Divide_(e,a)_<>_MultBy_(b,c)_&_a_:=_(f,e)_<>_MultBy_(b,c)_&_a_:=len_f_<>_MultBy_(b,c)_) let e be Int-Location; ::_thesis: for l being Element of NAT for f being FinSeq-Location holds ( a := e <> MultBy (b,c) & AddTo (a,e) <> MultBy (b,c) & SubFrom (a,e) <> MultBy (b,c) & MultBy (a,e) <> MultBy (b,c) & Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) let l be Element of NAT ; ::_thesis: for f being FinSeq-Location holds ( a := e <> MultBy (b,c) & AddTo (a,e) <> MultBy (b,c) & SubFrom (a,e) <> MultBy (b,c) & MultBy (a,e) <> MultBy (b,c) & Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) let f be FinSeq-Location ; ::_thesis: ( a := e <> MultBy (b,c) & AddTo (a,e) <> MultBy (b,c) & SubFrom (a,e) <> MultBy (b,c) & MultBy (a,e) <> MultBy (b,c) & Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) A2: InsCode (MultBy (b,c)) = 4 by SCMFSA_2:21; hence a := e <> MultBy (b,c) by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> MultBy (b,c) & SubFrom (a,e) <> MultBy (b,c) & MultBy (a,e) <> MultBy (b,c) & Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) thus AddTo (a,e) <> MultBy (b,c) by A2, SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> MultBy (b,c) & MultBy (a,e) <> MultBy (b,c) & Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) thus SubFrom (a,e) <> MultBy (b,c) by A2, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> MultBy (b,c) & Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) thus MultBy (a,e) <> MultBy (b,c) by A1, SF_MASTR:4; ::_thesis: ( Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) & a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) thus ( Divide (a,e) <> MultBy (b,c) & Divide (e,a) <> MultBy (b,c) ) by A2, SCMFSA_2:22; ::_thesis: ( a := (f,e) <> MultBy (b,c) & a :=len f <> MultBy (b,c) ) thus a := (f,e) <> MultBy (b,c) by A2, SCMFSA_2:26; ::_thesis: a :=len f <> MultBy (b,c) thus a :=len f <> MultBy (b,c) by A2, SCMFSA_2:28; ::_thesis: verum end; hence not MultBy (b,c) destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:10 for a, b, c being Int-Location st a <> b & a <> c holds not Divide (b,c) destroys a proof let a, b, c be Int-Location; ::_thesis: ( a <> b & a <> c implies not Divide (b,c) destroys a ) assume A1: ( a <> b & a <> c ) ; ::_thesis: not Divide (b,c) destroys a now__::_thesis:_for_e_being_Int-Location for_l_being_Element_of_NAT_ for_h_being_FinSeq-Location_holds_ (_a_:=_e_<>_Divide_(b,c)_&_AddTo_(a,e)_<>_Divide_(b,c)_&_SubFrom_(a,e)_<>_Divide_(b,c)_&_MultBy_(a,e)_<>_Divide_(b,c)_&_Divide_(e,a)_<>_Divide_(b,c)_&_Divide_(a,e)_<>_Divide_(b,c)_&_a_:=_(h,e)_<>_Divide_(b,c)_&_a_:=len_h_<>_Divide_(b,c)_) let e be Int-Location; ::_thesis: for l being Element of NAT for h being FinSeq-Location holds ( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) let l be Element of NAT ; ::_thesis: for h being FinSeq-Location holds ( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) let h be FinSeq-Location ; ::_thesis: ( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) A2: InsCode (Divide (b,c)) = 5 by SCMFSA_2:22; hence a := e <> Divide (b,c) by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) thus AddTo (a,e) <> Divide (b,c) by A2, SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) thus SubFrom (a,e) <> Divide (b,c) by A2, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) thus MultBy (a,e) <> Divide (b,c) by A2, SCMFSA_2:21; ::_thesis: ( Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) thus ( Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) ) by A1, SF_MASTR:5; ::_thesis: ( a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) ) thus a := (h,e) <> Divide (b,c) by A2, SCMFSA_2:26; ::_thesis: a :=len h <> Divide (b,c) thus a :=len h <> Divide (b,c) by A2, SCMFSA_2:28; ::_thesis: verum end; hence not Divide (b,c) destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:11 for a being Int-Location for l being Element of NAT holds not goto l destroys a proof let a be Int-Location; ::_thesis: for l being Element of NAT holds not goto l destroys a let l be Element of NAT ; ::_thesis: not goto l destroys a for b being Int-Location for t being Element of NAT for f being FinSeq-Location holds ( a := b <> goto l & AddTo (a,b) <> goto l & SubFrom (a,b) <> goto l & MultBy (a,b) <> goto l & Divide (a,b) <> goto l & Divide (b,a) <> goto l & a := (f,b) <> goto l & a :=len f <> goto l ) ; hence not goto l destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:12 for a, b being Int-Location for l being Element of NAT holds not b =0_goto l destroys a proof let a, b be Int-Location; ::_thesis: for l being Element of NAT holds not b =0_goto l destroys a let l be Element of NAT ; ::_thesis: not b =0_goto l destroys a for e being Int-Location for f being FinSeq-Location holds ( a := e <> b =0_goto l & AddTo (a,e) <> b =0_goto l & SubFrom (a,e) <> b =0_goto l & MultBy (a,e) <> b =0_goto l & Divide (a,e) <> b =0_goto l & Divide (e,a) <> b =0_goto l & a := (f,e) <> b =0_goto l & a :=len f <> b =0_goto l ) ; hence not b =0_goto l destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:13 for a, b being Int-Location for l being Element of NAT holds not b >0_goto l destroys a proof let a, b be Int-Location; ::_thesis: for l being Element of NAT holds not b >0_goto l destroys a let l be Element of NAT ; ::_thesis: not b >0_goto l destroys a for e being Int-Location for f being FinSeq-Location holds ( a := e <> b >0_goto l & AddTo (a,e) <> b >0_goto l & SubFrom (a,e) <> b >0_goto l & MultBy (a,e) <> b >0_goto l & Divide (a,e) <> b >0_goto l & Divide (e,a) <> b >0_goto l & a := (f,e) <> b >0_goto l & a :=len f <> b >0_goto l ) ; hence not b >0_goto l destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:14 for a, b, c being Int-Location for f being FinSeq-Location st a <> b holds not b := (f,c) destroys a proof let a, b, c be Int-Location; ::_thesis: for f being FinSeq-Location st a <> b holds not b := (f,c) destroys a let f be FinSeq-Location ; ::_thesis: ( a <> b implies not b := (f,c) destroys a ) assume A1: a <> b ; ::_thesis: not b := (f,c) destroys a now__::_thesis:_for_e_being_Int-Location for_l_being_Element_of_NAT_ for_h_being_FinSeq-Location_holds_ (_a_:=_e_<>_b_:=_(f,c)_&_AddTo_(a,e)_<>_b_:=_(f,c)_&_SubFrom_(a,e)_<>_b_:=_(f,c)_&_MultBy_(a,e)_<>_b_:=_(f,c)_&_Divide_(a,e)_<>_b_:=_(f,c)_&_Divide_(e,a)_<>_b_:=_(f,c)_&_a_:=_(h,e)_<>_b_:=_(f,c)_&_a_:=len_h_<>_b_:=_(f,c)_) let e be Int-Location; ::_thesis: for l being Element of NAT for h being FinSeq-Location holds ( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) let l be Element of NAT ; ::_thesis: for h being FinSeq-Location holds ( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) let h be FinSeq-Location ; ::_thesis: ( a := e <> b := (f,c) & AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) A2: InsCode (b := (f,c)) = 9 by SCMFSA_2:26; hence a := e <> b := (f,c) by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> b := (f,c) & SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) thus AddTo (a,e) <> b := (f,c) by A2, SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> b := (f,c) & MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) thus SubFrom (a,e) <> b := (f,c) by A2, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> b := (f,c) & Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) thus MultBy (a,e) <> b := (f,c) by A2, SCMFSA_2:21; ::_thesis: ( Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) & a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) thus ( Divide (a,e) <> b := (f,c) & Divide (e,a) <> b := (f,c) ) by A2, SCMFSA_2:22; ::_thesis: ( a := (h,e) <> b := (f,c) & a :=len h <> b := (f,c) ) thus a := (h,e) <> b := (f,c) by A1, SF_MASTR:9; ::_thesis: a :=len h <> b := (f,c) thus a :=len h <> b := (f,c) by A2, SCMFSA_2:28; ::_thesis: verum end; hence not b := (f,c) destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:15 for a, b, c being Int-Location for f being FinSeq-Location holds not (f,c) := b destroys a proof let a, b, c be Int-Location; ::_thesis: for f being FinSeq-Location holds not (f,c) := b destroys a let f be FinSeq-Location ; ::_thesis: not (f,c) := b destroys a now__::_thesis:_for_e_being_Int-Location for_h_being_FinSeq-Location_holds_ (_a_:=_e_<>_(f,c)_:=_b_&_AddTo_(a,e)_<>_(f,c)_:=_b_&_SubFrom_(a,e)_<>_(f,c)_:=_b_&_MultBy_(a,e)_<>_(f,c)_:=_b_&_Divide_(e,a)_<>_(f,c)_:=_b_&_Divide_(a,e)_<>_(f,c)_:=_b_&_a_:=_(h,e)_<>_(f,c)_:=_b_&_a_:=len_h_<>_(f,c)_:=_b_) let e be Int-Location; ::_thesis: for h being FinSeq-Location holds ( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) let h be FinSeq-Location ; ::_thesis: ( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) A1: InsCode ((f,c) := b) = 10 by SCMFSA_2:27; hence a := e <> (f,c) := b by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) thus AddTo (a,e) <> (f,c) := b by A1, SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) thus SubFrom (a,e) <> (f,c) := b by A1, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) thus MultBy (a,e) <> (f,c) := b by A1, SCMFSA_2:21; ::_thesis: ( Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) thus ( Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b ) by A1, SCMFSA_2:22; ::_thesis: ( a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b ) thus a := (h,e) <> (f,c) := b by A1, SCMFSA_2:26; ::_thesis: a :=len h <> (f,c) := b thus a :=len h <> (f,c) := b by A1, SCMFSA_2:28; ::_thesis: verum end; hence not (f,c) := b destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:16 for a, b being Int-Location for f being FinSeq-Location st a <> b holds not b :=len f destroys a proof let a, b be Int-Location; ::_thesis: for f being FinSeq-Location st a <> b holds not b :=len f destroys a let f be FinSeq-Location ; ::_thesis: ( a <> b implies not b :=len f destroys a ) assume A1: a <> b ; ::_thesis: not b :=len f destroys a now__::_thesis:_for_c_being_Int-Location for_g_being_FinSeq-Location_holds_ (_a_:=_c_<>_b_:=len_f_&_AddTo_(a,c)_<>_b_:=len_f_&_SubFrom_(a,c)_<>_b_:=len_f_&_MultBy_(a,c)_<>_b_:=len_f_&_Divide_(a,c)_<>_b_:=len_f_&_Divide_(c,a)_<>_b_:=len_f_&_a_:=_(g,c)_<>_b_:=len_f_&_a_:=len_g_<>_b_:=len_f_) let c be Int-Location; ::_thesis: for g being FinSeq-Location holds ( a := c <> b :=len f & AddTo (a,c) <> b :=len f & SubFrom (a,c) <> b :=len f & MultBy (a,c) <> b :=len f & Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f & a := (g,c) <> b :=len f & a :=len g <> b :=len f ) let g be FinSeq-Location ; ::_thesis: ( a := c <> b :=len f & AddTo (a,c) <> b :=len f & SubFrom (a,c) <> b :=len f & MultBy (a,c) <> b :=len f & Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f & a := (g,c) <> b :=len f & a :=len g <> b :=len f ) A2: InsCode (b :=len f) = 11 by SCMFSA_2:28; hence a := c <> b :=len f by SCMFSA_2:18; ::_thesis: ( AddTo (a,c) <> b :=len f & SubFrom (a,c) <> b :=len f & MultBy (a,c) <> b :=len f & Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f & a := (g,c) <> b :=len f & a :=len g <> b :=len f ) thus AddTo (a,c) <> b :=len f by A2, SCMFSA_2:19; ::_thesis: ( SubFrom (a,c) <> b :=len f & MultBy (a,c) <> b :=len f & Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f & a := (g,c) <> b :=len f & a :=len g <> b :=len f ) thus SubFrom (a,c) <> b :=len f by A2, SCMFSA_2:20; ::_thesis: ( MultBy (a,c) <> b :=len f & Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f & a := (g,c) <> b :=len f & a :=len g <> b :=len f ) thus MultBy (a,c) <> b :=len f by A2, SCMFSA_2:21; ::_thesis: ( Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f & a := (g,c) <> b :=len f & a :=len g <> b :=len f ) thus ( Divide (a,c) <> b :=len f & Divide (c,a) <> b :=len f ) by A2, SCMFSA_2:22; ::_thesis: ( a := (g,c) <> b :=len f & a :=len g <> b :=len f ) thus a := (g,c) <> b :=len f by A2, SCMFSA_2:26; ::_thesis: a :=len g <> b :=len f thus a :=len g <> b :=len f by A1, SF_MASTR:11; ::_thesis: verum end; hence not b :=len f destroys a by Def3; ::_thesis: verum end; theorem :: SCMFSA7B:17 for a, b being Int-Location for f being FinSeq-Location holds not f :=<0,...,0> b destroys a proof let a, b be Int-Location; ::_thesis: for f being FinSeq-Location holds not f :=<0,...,0> b destroys a let f be FinSeq-Location ; ::_thesis: not f :=<0,...,0> b destroys a now__::_thesis:_for_e_being_Int-Location for_h_being_FinSeq-Location_holds_ (_a_:=_e_<>_f_:=<0,...,0>_b_&_AddTo_(a,e)_<>_f_:=<0,...,0>_b_&_SubFrom_(a,e)_<>_f_:=<0,...,0>_b_&_MultBy_(a,e)_<>_f_:=<0,...,0>_b_&_Divide_(a,e)_<>_f_:=<0,...,0>_b_&_Divide_(e,a)_<>_f_:=<0,...,0>_b_&_a_:=_(h,e)_<>_f_:=<0,...,0>_b_&_a_:=len_h_<>_f_:=<0,...,0>_b_) let e be Int-Location; ::_thesis: for h being FinSeq-Location holds ( a := e <> f :=<0,...,0> b & AddTo (a,e) <> f :=<0,...,0> b & SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) let h be FinSeq-Location ; ::_thesis: ( a := e <> f :=<0,...,0> b & AddTo (a,e) <> f :=<0,...,0> b & SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) A1: InsCode (f :=<0,...,0> b) = 12 by SCMFSA_2:29; hence a := e <> f :=<0,...,0> b by SCMFSA_2:18; ::_thesis: ( AddTo (a,e) <> f :=<0,...,0> b & SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) thus AddTo (a,e) <> f :=<0,...,0> b by A1, SCMFSA_2:19; ::_thesis: ( SubFrom (a,e) <> f :=<0,...,0> b & MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) thus SubFrom (a,e) <> f :=<0,...,0> b by A1, SCMFSA_2:20; ::_thesis: ( MultBy (a,e) <> f :=<0,...,0> b & Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) thus MultBy (a,e) <> f :=<0,...,0> b by A1, SCMFSA_2:21; ::_thesis: ( Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b & a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) thus ( Divide (a,e) <> f :=<0,...,0> b & Divide (e,a) <> f :=<0,...,0> b ) by A1, SCMFSA_2:22; ::_thesis: ( a := (h,e) <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b ) thus a := (h,e) <> f :=<0,...,0> b by A1, SCMFSA_2:26; ::_thesis: a :=len h <> f :=<0,...,0> b thus a :=len h <> f :=<0,...,0> b by A1, SCMFSA_2:28; ::_thesis: verum end; hence not f :=<0,...,0> b destroys a by Def3; ::_thesis: verum end; definition let I be Program of SCM+FSA; let s be State of SCM+FSA; let P be Instruction-Sequence of SCM+FSA; predI is_closed_on s,P means :Def6: :: SCMFSA7B:def 6 for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I; predI is_halting_on s,P means :Def7: :: SCMFSA7B:def 7 P +* I halts_on Initialize s; end; :: deftheorem Def6 defines is_closed_on SCMFSA7B:def_6_:_ for I being Program of SCM+FSA for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds ( I is_closed_on s,P iff for k being Element of NAT holds IC (Comput ((P +* I),(Initialize s),k)) in dom I ); :: deftheorem Def7 defines is_halting_on SCMFSA7B:def_7_:_ for I being Program of SCM+FSA for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds ( I is_halting_on s,P iff P +* I halts_on Initialize s ); theorem Th18: :: SCMFSA7B:18 for I being Program of SCM+FSA holds ( I is paraclosed iff for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ) proof let I be Program of SCM+FSA; ::_thesis: ( I is paraclosed iff for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ) thus ( I is paraclosed implies for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ) ::_thesis: ( ( for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ) implies I is paraclosed ) proof assume A1: I is paraclosed ; ::_thesis: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P let P be Instruction-Sequence of SCM+FSA; ::_thesis: I is_closed_on s,P let k be Element of NAT ; :: according to SCMFSA7B:def_6 ::_thesis: IC (Comput ((P +* I),(Initialize s),k)) in dom I I c= P +* I by FUNCT_4:25; hence IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, AMISTD_1:def_10; ::_thesis: verum end; assume A2: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_closed_on s,P ; ::_thesis: I is paraclosed let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_10 ::_thesis: for b1 being set holds ( not I c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in K360(NAT,I) ) let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not I c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in K360(NAT,I) ) assume A3: I c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in K360(NAT,I) let n be Element of NAT ; ::_thesis: IC (Comput (P,s,n)) in K360(NAT,I) A4: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29; A5: P = P +* I by A3, FUNCT_4:98; A6: s = Initialize s by A4, FUNCT_4:98; I is_closed_on s,P by A2; hence IC (Comput (P,s,n)) in dom I by A5, A6, Def6; ::_thesis: verum end; theorem :: SCMFSA7B:19 for I being Program of SCM+FSA holds ( I is parahalting iff for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ) proof set SAt = Start-At (0,SCM+FSA); let I be Program of SCM+FSA; ::_thesis: ( I is parahalting iff for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ) thus ( I is parahalting implies for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ) ::_thesis: ( ( for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ) implies I is parahalting ) proof assume A1: I is parahalting ; ::_thesis: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P let P be Instruction-Sequence of SCM+FSA; ::_thesis: I is_halting_on s,P I c= P +* I by FUNCT_4:25; hence P +* I halts_on Initialize s by A1, AMISTD_1:def_11; :: according to SCMFSA7B:def_7 ::_thesis: verum end; assume A2: for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA holds I is_halting_on s,P ; ::_thesis: I is parahalting let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds ( not I c= b1 or b1 halts_on s ) A3: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29; let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not I c= P or P halts_on s ) assume A4: I c= P ; ::_thesis: P halts_on s A5: P = P +* I by A4, FUNCT_4:98; A6: Initialize s = s by A3, FUNCT_4:98; I is_halting_on s,P by A2; hence P halts_on s by A5, A6, Def7; ::_thesis: verum end; theorem Th20: :: SCMFSA7B:20 for i being Instruction of SCM+FSA for a being Int-Location for s being State of SCM+FSA st not i destroys a holds (Exec (i,s)) . a = s . a proof let i be Instruction of SCM+FSA; ::_thesis: for a being Int-Location for s being State of SCM+FSA st not i destroys a holds (Exec (i,s)) . a = s . a let a be Int-Location; ::_thesis: for s being State of SCM+FSA st not i destroys a holds (Exec (i,s)) . a = s . a let s be State of SCM+FSA; ::_thesis: ( not i destroys a implies (Exec (i,s)) . a = s . a ) assume A1: not i destroys a ; ::_thesis: (Exec (i,s)) . a = s . a percases ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 ) by NAT_1:36, SCMFSA_2:16; suppose InsCode i = 0 ; ::_thesis: (Exec (i,s)) . a = s . a then i = halt SCM+FSA by SCMFSA_2:95; hence (Exec (i,s)) . a = s . a by EXTPRO_1:def_3; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: (Exec (i,s)) . a = s . a then consider da, db being Int-Location such that A2: i = da := db by SCMFSA_2:30; da <> a by A1, A2, Def3; hence (Exec (i,s)) . a = s . a by A2, SCMFSA_2:63; ::_thesis: verum end; suppose InsCode i = 2 ; ::_thesis: (Exec (i,s)) . a = s . a then consider da, db being Int-Location such that A3: i = AddTo (da,db) by SCMFSA_2:31; da <> a by A1, A3, Def3; hence (Exec (i,s)) . a = s . a by A3, SCMFSA_2:64; ::_thesis: verum end; suppose InsCode i = 3 ; ::_thesis: (Exec (i,s)) . a = s . a then consider da, db being Int-Location such that A4: i = SubFrom (da,db) by SCMFSA_2:32; da <> a by A1, A4, Def3; hence (Exec (i,s)) . a = s . a by A4, SCMFSA_2:65; ::_thesis: verum end; suppose InsCode i = 4 ; ::_thesis: (Exec (i,s)) . a = s . a then consider da, db being Int-Location such that A5: i = MultBy (da,db) by SCMFSA_2:33; da <> a by A1, A5, Def3; hence (Exec (i,s)) . a = s . a by A5, SCMFSA_2:66; ::_thesis: verum end; suppose InsCode i = 5 ; ::_thesis: (Exec (i,s)) . a = s . a then consider da, db being Int-Location such that A6: i = Divide (da,db) by SCMFSA_2:34; ( da <> a & db <> a ) by A1, A6, Def3; hence (Exec (i,s)) . a = s . a by A6, SCMFSA_2:67; ::_thesis: verum end; suppose InsCode i = 6 ; ::_thesis: (Exec (i,s)) . a = s . a then ex loc being Element of NAT st i = goto loc by SCMFSA_2:35; hence (Exec (i,s)) . a = s . a by SCMFSA_2:69; ::_thesis: verum end; suppose InsCode i = 7 ; ::_thesis: (Exec (i,s)) . a = s . a then ex loc being Element of NAT ex da being Int-Location st i = da =0_goto loc by SCMFSA_2:36; hence (Exec (i,s)) . a = s . a by SCMFSA_2:70; ::_thesis: verum end; suppose InsCode i = 8 ; ::_thesis: (Exec (i,s)) . a = s . a then ex loc being Element of NAT ex da being Int-Location st i = da >0_goto loc by SCMFSA_2:37; hence (Exec (i,s)) . a = s . a by SCMFSA_2:71; ::_thesis: verum end; suppose InsCode i = 9 ; ::_thesis: (Exec (i,s)) . a = s . a then consider db, da being Int-Location, g being FinSeq-Location such that A7: i = da := (g,db) by SCMFSA_2:38; da <> a by A1, A7, Def3; hence (Exec (i,s)) . a = s . a by A7, SCMFSA_2:72; ::_thesis: verum end; suppose InsCode i = 10 ; ::_thesis: (Exec (i,s)) . a = s . a then ex db, da being Int-Location ex g being FinSeq-Location st i = (g,db) := da by SCMFSA_2:39; hence (Exec (i,s)) . a = s . a by SCMFSA_2:73; ::_thesis: verum end; suppose InsCode i = 11 ; ::_thesis: (Exec (i,s)) . a = s . a then consider da being Int-Location, g being FinSeq-Location such that A8: i = da :=len g by SCMFSA_2:40; da <> a by A1, A8, Def3; hence (Exec (i,s)) . a = s . a by A8, SCMFSA_2:74; ::_thesis: verum end; suppose InsCode i = 12 ; ::_thesis: (Exec (i,s)) . a = s . a then ex da being Int-Location ex g being FinSeq-Location st i = g :=<0,...,0> da by SCMFSA_2:41; hence (Exec (i,s)) . a = s . a by SCMFSA_2:75; ::_thesis: verum end; end; end; theorem Th21: :: SCMFSA7B:21 for s being State of SCM+FSA for P being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA for a being Int-Location st not I destroys a & I is_closed_on s,P holds for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a proof let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA for I being Program of SCM+FSA for a being Int-Location st not I destroys a & I is_closed_on s,P holds for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a let P be Instruction-Sequence of SCM+FSA; ::_thesis: for I being Program of SCM+FSA for a being Int-Location st not I destroys a & I is_closed_on s,P holds for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a let I be Program of SCM+FSA; ::_thesis: for a being Int-Location st not I destroys a & I is_closed_on s,P holds for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a let a be Int-Location; ::_thesis: ( not I destroys a & I is_closed_on s,P implies for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a ) assume A1: not I destroys a ; ::_thesis: ( not I is_closed_on s,P or for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a ) defpred S1[ Nat] means (Comput ((P +* I),(Initialize s),$1)) . a = s . a; A2: I c= P +* I by FUNCT_4:25; assume A3: I is_closed_on s,P ; ::_thesis: for k being Element of NAT holds (Comput ((P +* I),(Initialize s),k)) . a = s . a A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] set l = IC (Comput ((P +* I),(Initialize s),k)); A6: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A3, Def6; then (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) = I . (IC (Comput ((P +* I),(Initialize s),k))) by A2, GRFUNC_1:2; then (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) in rng I by A6, FUNCT_1:def_3; then A7: not (P +* I) . (IC (Comput ((P +* I),(Initialize s),k))) destroys a by A1, Def4; A8: dom (P +* I) = NAT by PARTFUN1:def_2; (Comput ((P +* I),(Initialize s),(k + 1))) . a = (Following ((P +* I),(Comput ((P +* I),(Initialize s),k)))) . a by EXTPRO_1:3 .= (Exec (((P +* I) . (IC (Comput ((P +* I),(Initialize s),k)))),(Comput ((P +* I),(Initialize s),k)))) . a by A8, PARTFUN1:def_6 .= (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),k)) . a by A7, Th20 .= s . a by A5 ; hence S1[k + 1] ; ::_thesis: verum end; A9: not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102; (Comput ((P +* I),(Initialize s),0)) . a = (Initialize s) . a .= s . a by A9, FUNCT_4:11 ; then A10: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A10, A4); ::_thesis: verum end; registration cluster Stop SCM+FSA -> parahalting good ; coherence ( Stop SCM+FSA is parahalting & Stop SCM+FSA is good ) proof thus Stop SCM+FSA is parahalting ::_thesis: Stop SCM+FSA is good proof A1: 0 in dom (Stop SCM+FSA) by AFINSQ_1:65; A2: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15; let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def_11 ::_thesis: for b1 being set holds ( not Stop SCM+FSA c= b1 or b1 halts_on s ) A3: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29; let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not Stop SCM+FSA c= P or P halts_on s ) assume A4: Stop SCM+FSA c= P ; ::_thesis: P halts_on s A5: dom P = NAT by PARTFUN1:def_2; CurInstr (P,(Comput (P,s,0))) = CurInstr (P,s) .= P . (IC s) by A5, PARTFUN1:def_6 .= P . (IC (Start-At (0,SCM+FSA))) by A3, A2, GRFUNC_1:2 .= P . 0 by FUNCOP_1:72 .= (Stop SCM+FSA) . 0 by A1, A4, GRFUNC_1:2 .= halt SCM+FSA by AFINSQ_1:34 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: verum end; thus not Stop SCM+FSA destroys intloc 0 :: according to SCMFSA7B:def_5 ::_thesis: verum proof now__::_thesis:_for_i_being_Instruction_of_SCM+FSA_st_i_in_rng_(Stop_SCM+FSA)_holds_ not_i_destroys_intloc_0 let i be Instruction of SCM+FSA; ::_thesis: ( i in rng (Stop SCM+FSA) implies not i destroys intloc 0 ) A6: rng (Stop SCM+FSA) = {(halt SCM+FSA)} by AFINSQ_1:33; assume i in rng (Stop SCM+FSA) ; ::_thesis: not i destroys intloc 0 then i = halt SCM+FSA by A6, TARSKI:def_1; hence not i destroys intloc 0 by Th5; ::_thesis: verum end; hence not Stop SCM+FSA destroys intloc 0 by Def4; ::_thesis: verum end; end; end; registration cluster non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial parahalting good for set ; existence ex b1 being Program of SCM+FSA st ( b1 is parahalting & b1 is good ) proof take Stop SCM+FSA ; ::_thesis: ( Stop SCM+FSA is parahalting & Stop SCM+FSA is good ) thus ( Stop SCM+FSA is parahalting & Stop SCM+FSA is good ) ; ::_thesis: verum end; end; registration cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V29() initial paraclosed good -> keeping_0 for set ; correctness coherence for b1 being Program of SCM+FSA st b1 is paraclosed & b1 is good holds b1 is keeping_0 ; proof let I be Program of SCM+FSA; ::_thesis: ( I is paraclosed & I is good implies I is keeping_0 ) assume A1: ( I is paraclosed & I is good ) ; ::_thesis: I is keeping_0 then A2: not I destroys intloc 0 by Def5; let s be 0 -started State of SCM+FSA; :: according to SCMFSA6B:def_4 ::_thesis: for b1 being set holds ( not I c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) ) A3: Initialize s = s by MEMSTR_0:44; let P be Instruction-Sequence of SCM+FSA; ::_thesis: ( not I c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) ) assume A4: I c= P ; ::_thesis: for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) let k be Element of NAT ; ::_thesis: (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) A5: I is_closed_on s,P by A1, Th18; P +* I = P by A4, FUNCT_4:98; hence (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) by A2, A3, Th21, A5; ::_thesis: verum end; end; theorem Th22: :: SCMFSA7B:22 for a being Int-Location for k being Integer holds rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} proof let a be Int-Location; ::_thesis: for k being Integer holds rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} let k be Integer; ::_thesis: rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (aSeq (a,k)) or x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} ) assume A1: x in rng (aSeq (a,k)) ; ::_thesis: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} percases ( ( k > 0 & k = 0 + 1 ) or ( k > 0 & k <> 1 ) or not k > 0 ) ; supposeA2: ( k > 0 & k = 0 + 1 ) ; ::_thesis: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} then ex k1 being Element of NAT st ( k1 + 1 = k & aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) by SCMFSA_7:def_2; then aSeq (a,k) = <%(a := (intloc 0))%> ^ {} by A2 .= <%(a := (intloc 0))%> ; then rng (aSeq (a,k)) = {(a := (intloc 0))} by AFINSQ_1:33; then x = a := (intloc 0) by A1, TARSKI:def_1; hence x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def_1; ::_thesis: verum end; supposeA3: ( k > 0 & k <> 1 ) ; ::_thesis: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} then consider k1 being Element of NAT such that A4: k1 + 1 = k and A5: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) by SCMFSA_7:def_2; A6: k1 <> 0 by A3, A4; rng (aSeq (a,k)) = (rng <%(a := (intloc 0))%>) \/ (rng (k1 --> (AddTo (a,(intloc 0))))) by A5, AFINSQ_1:26 .= {(a := (intloc 0))} \/ (rng (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:33 .= {(a := (intloc 0))} \/ {(AddTo (a,(intloc 0)))} by A6, FUNCOP_1:8 ; then ( x in {(a := (intloc 0))} or x in {(AddTo (a,(intloc 0)))} ) by A1, XBOOLE_0:def_3; then ( x = a := (intloc 0) or x = AddTo (a,(intloc 0)) ) by TARSKI:def_1; hence x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def_1; ::_thesis: verum end; supposeA7: not k > 0 ; ::_thesis: x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} then consider k1 being Element of NAT such that A8: k1 + k = 1 and A9: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by SCMFSA_7:def_2; A10: k1 <> 0 by A7, A8; rng (aSeq (a,k)) = (rng <%(a := (intloc 0))%>) \/ (rng (k1 --> (SubFrom (a,(intloc 0))))) by A9, AFINSQ_1:26 .= {(a := (intloc 0))} \/ (rng (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:33 .= {(a := (intloc 0))} \/ {(SubFrom (a,(intloc 0)))} by A10, FUNCOP_1:8 ; then ( x in {(a := (intloc 0))} or x in {(SubFrom (a,(intloc 0)))} ) by A1, XBOOLE_0:def_3; then ( x = a := (intloc 0) or x = SubFrom (a,(intloc 0)) ) by TARSKI:def_1; hence x in {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def_1; ::_thesis: verum end; end; end; theorem Th23: :: SCMFSA7B:23 for a being Int-Location for k being Integer holds rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} proof let a be Int-Location; ::_thesis: for k being Integer holds rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} let k be Integer; ::_thesis: rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} now__::_thesis:_for_x_being_set_st_x_in_rng_(a_:=_k)_holds_ x_in_{(halt_SCM+FSA),(a_:=_(intloc_0)),(AddTo_(a,(intloc_0))),(SubFrom_(a,(intloc_0)))} let x be set ; ::_thesis: ( x in rng (a := k) implies x in {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} ) A1: rng (aSeq (a,k)) c= {(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by Th22; A2: rng (a := k) = rng ((aSeq (a,k)) ^ <%(halt SCM+FSA)%>) by SCMFSA_7:1 .= (rng (aSeq (a,k))) \/ (rng <%(halt SCM+FSA)%>) by AFINSQ_1:26 .= (rng (aSeq (a,k))) \/ {(halt SCM+FSA)} by AFINSQ_1:33 ; assume x in rng (a := k) ; ::_thesis: x in {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} then ( x in rng (aSeq (a,k)) or x in {(halt SCM+FSA)} ) by A2, XBOOLE_0:def_3; then ( x = a := (intloc 0) or x = AddTo (a,(intloc 0)) or x = SubFrom (a,(intloc 0)) or x = halt SCM+FSA ) by A1, ENUMSET1:def_1, TARSKI:def_1; hence x in {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by ENUMSET1:def_2; ::_thesis: verum end; hence rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by TARSKI:def_3; ::_thesis: verum end; registration let a be read-write Int-Location; let k be Integer; clustera := k -> good ; correctness coherence a := k is good ; proof now__::_thesis:_for_i_being_Instruction_of_SCM+FSA_st_i_in_rng_(a_:=_k)_holds_ not_i_destroys_intloc_0 let i be Instruction of SCM+FSA; ::_thesis: ( i in rng (a := k) implies not b1 destroys intloc 0 ) A1: rng (a := k) c= {(halt SCM+FSA),(a := (intloc 0)),(AddTo (a,(intloc 0))),(SubFrom (a,(intloc 0)))} by Th23; assume A2: i in rng (a := k) ; ::_thesis: not b1 destroys intloc 0 percases ( i = halt SCM+FSA or i = a := (intloc 0) or i = AddTo (a,(intloc 0)) or i = SubFrom (a,(intloc 0)) ) by A2, A1, ENUMSET1:def_2; suppose i = halt SCM+FSA ; ::_thesis: not b1 destroys intloc 0 hence not i destroys intloc 0 by Th5; ::_thesis: verum end; suppose i = a := (intloc 0) ; ::_thesis: not b1 destroys intloc 0 hence not i destroys intloc 0 by Th6; ::_thesis: verum end; suppose i = AddTo (a,(intloc 0)) ; ::_thesis: not b1 destroys intloc 0 hence not i destroys intloc 0 by Th7; ::_thesis: verum end; suppose i = SubFrom (a,(intloc 0)) ; ::_thesis: not b1 destroys intloc 0 hence not i destroys intloc 0 by Th8; ::_thesis: verum end; end; end; then not a := k destroys intloc 0 by Def4; hence a := k is good by Def5; ::_thesis: verum end; end; registration let a be read-write Int-Location; let k be Integer; clustera := k -> keeping_0 ; correctness coherence a := k is keeping_0 ; ; end;