:: SCMFSA_7 semantic presentation begin Lm1: for p1, p2, p3, p4 being XFinSequence holds ( ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((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) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 ) thus ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ p2) ^ (p3 ^ p4) by AFINSQ_1:27; ::_thesis: ( ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ ((p2 ^ p3) ^ p4) & ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((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: ( ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) & ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 ) hence ((p1 ^ p2) ^ p3) ^ p4 = p1 ^ (p2 ^ (p3 ^ p4)) by AFINSQ_1:27; ::_thesis: ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 thus ((p1 ^ p2) ^ p3) ^ p4 = (p1 ^ (p2 ^ p3)) ^ p4 by AFINSQ_1:27; ::_thesis: verum end; Lm2: for p1, p2, p3, p4, p5 being XFinSequence holds ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) proof let p1, p2, p3, p4, p5 be XFinSequence; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ p3) ^ (p4 ^ p5) by AFINSQ_1:27; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ ((p3 ^ p4) ^ p5) by Lm1; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ p2) ^ (p3 ^ (p4 ^ p5)) by Lm1; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (((p2 ^ p3) ^ p4) ^ p5) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus A1: (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 by Lm1 .= p1 ^ (((p2 ^ p3) ^ p4) ^ p5) by AFINSQ_1:27 ; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) hence (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ p3) ^ (p4 ^ p5)) by AFINSQ_1:27; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ ((p3 ^ p4) ^ p5)) by A1, Lm1; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ (p2 ^ (p3 ^ (p4 ^ p5))) by A1, Lm1; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = ((p1 ^ p2) ^ (p3 ^ p4)) ^ p5 by Lm1; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ ((p2 ^ p3) ^ p4)) ^ p5 by Lm1; ::_thesis: ( (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 & (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) ) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = (p1 ^ (p2 ^ (p3 ^ p4))) ^ p5 by Lm1; ::_thesis: (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) thus (((p1 ^ p2) ^ p3) ^ p4) ^ p5 = p1 ^ ((p2 ^ (p3 ^ p4)) ^ p5) by A1, Lm1; ::_thesis: verum end; deffunc H1( Element of NAT ) -> Element of NAT = $1 -' 1; definition let a be Int-Location; let k be Integer; funca := k -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function means :Def1: :: SCMFSA_7:def 1 ex k1 being Element of NAT st ( k1 + 1 = k & it = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) if k > 0 otherwise ex k1 being Element of NAT st ( k1 + k = 1 & it = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ); existence ( ( k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + 1 = k & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) & ( not k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) proof thus ( k > 0 implies ex f being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + 1 = k & f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ::_thesis: ( not k > 0 implies ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) proof assume k > 0 ; ::_thesis: ex f being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + 1 = k & f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) then 0 + 1 <= k by INT_1:7; then reconsider k1 = k - 1 as Element of NAT by INT_1:5; set xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>; reconsider xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> as NAT -defined the InstructionsF of SCM+FSA -valued finite Function ; take xx ; ::_thesis: ex k1 being Element of NAT st ( k1 + 1 = k & xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) take k1 ; ::_thesis: ( k1 + 1 = k & xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) thus k1 + 1 = k ; ::_thesis: xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> thus xx = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ; ::_thesis: verum end; assume k <= 0 ; ::_thesis: ex b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function ex k1 being Element of NAT st ( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) then reconsider k1 = 1 - k as Element of NAT by INT_1:5; set xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>; reconsider xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> as NAT -defined the InstructionsF of SCM+FSA -valued finite Function ; take xx ; ::_thesis: ex k1 being Element of NAT st ( k1 + k = 1 & xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) take k1 ; ::_thesis: ( k1 + k = 1 & xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) thus k1 + k = 1 ; ::_thesis: xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> thus xx = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ; ::_thesis: verum end; uniqueness for b1, b2 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds ( ( k > 0 & ex k1 being Element of NAT st ( k1 + 1 = k & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) & ex k1 being Element of NAT st ( k1 + 1 = k & b2 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Element of NAT st ( k1 + k = 1 & b1 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) & ex k1 being Element of NAT st ( k1 + k = 1 & b2 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) implies b1 = b2 ) ) ; correctness consistency for b1 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds verum; ; end; :: deftheorem Def1 defines := SCMFSA_7:def_1_:_ for a being Int-Location for k being Integer for b3 being NAT -defined the InstructionsF of SCM+FSA -valued finite Function holds ( ( k > 0 implies ( b3 = a := k iff ex k1 being Element of NAT st ( k1 + 1 = k & b3 = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) & ( not k > 0 implies ( b3 = a := k iff ex k1 being Element of NAT st ( k1 + k = 1 & b3 = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) ) ) ); definition let a be Int-Location; let k be Integer; func aSeq (a,k) -> XFinSequence of means :Def2: :: SCMFSA_7:def 2 ex k1 being Element of NAT st ( k1 + 1 = k & it = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) if k > 0 otherwise ex k1 being Element of NAT st ( k1 + k = 1 & it = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ); existence ( ( k > 0 implies ex b1 being XFinSequence of ex k1 being Element of NAT st ( k1 + 1 = k & b1 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) & ( not k > 0 implies ex b1 being XFinSequence of ex k1 being Element of NAT st ( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) ) proof thus ( k > 0 implies ex s being XFinSequence of ex k1 being Element of NAT st ( k1 + 1 = k & s = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) ::_thesis: ( not k > 0 implies ex b1 being XFinSequence of ex k1 being Element of NAT st ( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) proof assume k > 0 ; ::_thesis: ex s being XFinSequence of ex k1 being Element of NAT st ( k1 + 1 = k & s = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) then 0 + 1 <= k by INT_1:7; then reconsider k1 = k - 1 as Element of NAT by INT_1:5; take <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ; ::_thesis: ex k1 being Element of NAT st ( k1 + 1 = k & <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) take k1 ; ::_thesis: ( k1 + 1 = k & <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) thus k1 + 1 = k ; ::_thesis: <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) thus <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ; ::_thesis: verum end; assume k <= 0 ; ::_thesis: ex b1 being XFinSequence of ex k1 being Element of NAT st ( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) then reconsider k1 = 1 - k as Element of NAT by INT_1:5; take <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ; ::_thesis: ex k1 being Element of NAT st ( k1 + k = 1 & <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) take k1 ; ::_thesis: ( k1 + k = 1 & <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) thus k1 + k = 1 ; ::_thesis: <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) thus <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence of holds ( ( k > 0 & ex k1 being Element of NAT st ( k1 + 1 = k & b1 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) & ex k1 being Element of NAT st ( k1 + 1 = k & b2 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) implies b1 = b2 ) & ( not k > 0 & ex k1 being Element of NAT st ( k1 + k = 1 & b1 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) & ex k1 being Element of NAT st ( k1 + k = 1 & b2 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) implies b1 = b2 ) ) ; correctness consistency for b1 being XFinSequence of holds verum; ; end; :: deftheorem Def2 defines aSeq SCMFSA_7:def_2_:_ for a being Int-Location for k being Integer for b3 being XFinSequence of holds ( ( k > 0 implies ( b3 = aSeq (a,k) iff ex k1 being Element of NAT st ( k1 + 1 = k & b3 = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) ) ) ) & ( not k > 0 implies ( b3 = aSeq (a,k) iff ex k1 being Element of NAT st ( k1 + k = 1 & b3 = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) ) ) ) ); theorem :: SCMFSA_7:1 for a being Int-Location for k being Integer holds a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> proof let a be Int-Location; ::_thesis: for k being Integer holds a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> let k be Integer; ::_thesis: a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> percases ( k > 0 or k <= 0 ) ; suppose k > 0 ; ::_thesis: a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> then ex k1 being Element of NAT st ( k1 + 1 = k & a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) by Def1; hence a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> by Def2; ::_thesis: verum end; supposeA1: k <= 0 ; ::_thesis: a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> then ex k1 being Element of NAT st ( k1 + k = 1 & a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) by Def1; hence a := k = (aSeq (a,k)) ^ <%(halt SCM+FSA)%> by A1, Def2; ::_thesis: verum end; end; end; definition let f be FinSeq-Location ; let p be FinSequence of INT ; func aSeq (f,p) -> XFinSequence of means :Def3: :: SCMFSA_7:def 3 ex pp being XFinSequence of st ( 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))%> ) ) & it = FlattenSeq pp ); existence ex b1 being XFinSequence of ex pp being XFinSequence of st ( 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))%> ) ) & b1 = FlattenSeq pp ) proof defpred S1[ Integer, set ] means ex i being Integer st ( i = p . ($1 + 1) & $2 = ((aSeq ((intloc 1),($1 + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ); set D = the InstructionsF of SCM+FSA ^omega ; A1: for k being Nat st k in len p holds ex d being Element of the InstructionsF of SCM+FSA ^omega st S1[k,d] proof let k be Nat; ::_thesis: ( k in len p implies ex d being Element of the InstructionsF of SCM+FSA ^omega st S1[k,d] ) assume k in len p ; ::_thesis: ex d being Element of the InstructionsF of SCM+FSA ^omega st S1[k,d] then k < len p by NAT_1:44; then ( 1 <= k + 1 & k + 1 <= len p ) by NAT_1:12, NAT_1:13; then k + 1 in dom p by FINSEQ_3:25; then p . (k + 1) in INT by FINSEQ_2:11; then reconsider i = p . (k + 1) as Integer ; reconsider d = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> as Element of the InstructionsF of SCM+FSA ^omega by AFINSQ_1:def_7; take d ; ::_thesis: S1[k,d] thus S1[k,d] ; ::_thesis: verum end; consider pp being XFinSequence of such that A2: dom pp = len p and A3: for k being Nat st k in len p holds S1[k,pp . k] from STIRL2_1:sch_5(A1); reconsider tt = FlattenSeq pp as XFinSequence of by AFINSQ_1:def_7; take tt ; ::_thesis: ex pp being XFinSequence of st ( 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))%> ) ) & tt = FlattenSeq pp ) take pp ; ::_thesis: ( 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))%> ) ) & tt = FlattenSeq pp ) thus len pp = len p by A2; ::_thesis: ( ( 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))%> ) ) & tt = FlattenSeq pp ) hereby ::_thesis: tt = FlattenSeq pp let k be Element of NAT ; ::_thesis: ( k < len pp implies ex i being Integer st ( i = p . (k + 1) & ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k ) ) assume A4: k < len pp ; ::_thesis: ex i being Integer st ( i = p . (k + 1) & ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k ) then ( 1 <= k + 1 & k + 1 <= len p ) by A2, NAT_1:12, NAT_1:13; then k + 1 in dom p by FINSEQ_3:25; then p . (k + 1) in INT by FINSEQ_2:11; then reconsider i = p . (k + 1) as Integer ; take i = i; ::_thesis: ( i = p . (k + 1) & ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k ) thus i = p . (k + 1) ; ::_thesis: ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k k in len p by A2, A4, NAT_1:44; then ( k in dom pp & S1[k,pp . k] ) by A2, A3; hence ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> = pp . k ; ::_thesis: verum end; thus tt = FlattenSeq pp ; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence of st ex pp being XFinSequence of st ( 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))%> ) ) & b1 = FlattenSeq pp ) & ex pp being XFinSequence of st ( 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))%> ) ) & b2 = FlattenSeq pp ) holds b1 = b2 proof reconsider i = len p as Element of NAT ; let s1, s2 be XFinSequence of ; ::_thesis: ( ex pp being XFinSequence of st ( 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))%> ) ) & s1 = FlattenSeq pp ) & ex pp being XFinSequence of st ( 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))%> ) ) & s2 = FlattenSeq pp ) implies s1 = s2 ) assume that A5: ex pp being XFinSequence of st ( 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))%> ) ) & s1 = FlattenSeq pp ) and A6: ex pp being XFinSequence of st ( 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))%> ) ) & s2 = FlattenSeq pp ) ; ::_thesis: s1 = s2 consider pp1 being XFinSequence of such that A7: len pp1 = len p and A8: for k being Element of NAT st k < len pp1 holds ex i being Integer st ( i = p . (k + 1) & pp1 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) and A9: s1 = FlattenSeq pp1 by A5; consider pp2 being XFinSequence of such that A10: len pp2 = len p and A11: for k being Element of NAT st k < len pp2 holds ex i being Integer st ( i = p . (k + 1) & pp2 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) and A12: s2 = FlattenSeq pp2 by A6; for k being Nat st k < len pp1 holds pp1 . k = pp2 . k proof let k be Nat; ::_thesis: ( k < len pp1 implies pp1 . k = pp2 . k ) assume A13: k < len pp1 ; ::_thesis: pp1 . k = pp2 . k k in NAT by ORDINAL1:def_12; then ( ex i1 being Integer st ( i1 = p . (k + 1) & pp1 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i1))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) & ex i2 being Integer st ( i2 = p . (k + 1) & pp2 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i2))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) by A8, A11, A13, A7, A10; hence pp1 . k = pp2 . k ; ::_thesis: verum end; hence s1 = s2 by A9, A12, A7, A10, AFINSQ_1:9; ::_thesis: verum end; correctness ; end; :: deftheorem Def3 defines aSeq SCMFSA_7:def_3_:_ for f being FinSeq-Location for p being FinSequence of INT for b3 being XFinSequence of holds ( b3 = aSeq (f,p) iff ex pp being XFinSequence of st ( 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))%> ) ) & b3 = FlattenSeq pp ) ); definition let f be FinSeq-Location ; let p be FinSequence of INT ; funcf := p -> NAT -defined the InstructionsF of SCM+FSA -valued finite Function equals :: SCMFSA_7:def 4 (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; correctness coherence (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%> is NAT -defined the InstructionsF of SCM+FSA -valued finite Function; ; end; :: deftheorem defines := SCMFSA_7:def_4_:_ for f being FinSeq-Location for p being FinSequence of INT holds f := p = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; theorem :: SCMFSA_7:2 for a being Int-Location holds a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> proof let a be Int-Location; ::_thesis: a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> A: 0 + 1 = 1 ; <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> = (<%(a := (intloc 0))%> ^ {}) ^ <%(halt SCM+FSA)%> .= (<%(a := (intloc 0))%> ^ (0 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ; hence a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> by Def1, A; ::_thesis: verum end; theorem :: SCMFSA_7:3 for a being Int-Location holds a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ <%(halt SCM+FSA)%> proof let a be Int-Location; ::_thesis: a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ <%(halt SCM+FSA)%> ( 1 + 0 = 1 & (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ <%(halt SCM+FSA)%> = (<%(a := (intloc 0))%> ^ (1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) by CARD_1:49; hence a := 0 = (<%(a := (intloc 0))%> ^ <%(SubFrom (a,(intloc 0)))%>) ^ <%(halt SCM+FSA)%> by Def1; ::_thesis: verum end; theorem Th4: :: SCMFSA_7:4 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for c0 being Element of NAT for s being b2 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) proof let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; ::_thesis: for c0 being Element of NAT for s being b1 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) let c0 be Element of NAT ; ::_thesis: for s being c0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) let s be c0 -started State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies for a being Int-Location for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) ) assume A1: s . (intloc 0) = 1 ; ::_thesis: for a being Int-Location for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) A2: IC s = c0 by MEMSTR_0:def_11; let a be Int-Location; ::_thesis: for k being Integer st a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) let k be Integer; ::_thesis: ( a <> intloc 0 & ( for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) ) assume that A3: a <> intloc 0 and A4: for c being Element of NAT st c in dom (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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) 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 & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) 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, Def2; defpred S1[ Nat] means ( $1 <= k9 implies ( IC (Comput (P,s,$1)) = c0 + $1 & ( 1 <= $1 implies (Comput (P,s,$1)) . a = $1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) ); 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:33 .= k9 by A6, CARD_1:64 ; A9: for i being Element of NAT st i <= len (aSeq (a,k9)) holds ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = i ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) proof A10: for i being Element of NAT st i < k9 holds i in dom (aSeq (a,k9)) by A8, NAT_1:44; A11: P . (c0 + 0) = (aSeq (a,k9)) . 0 by A5, A4, A10 .= a := (intloc 0) by A7, AFINSQ_1:35 ; A12: 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 A13: 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 A2, A11, PBOOLE:143; ::_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 A2, A11, A13, PBOOLE:143 ; ::_thesis: verum end; A14: 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 A15: 1 <= i and A16: i < k9 ; ::_thesis: (aSeq (a,k9)) . i = AddTo (a,(intloc 0)) reconsider i1 = i - 1 as Element of NAT by A15, INT_1:5; i = i1 + 1 ; then i1 < k1 by A16, A6, XREAL_1:6; then A17: i1 in k1 by NAT_1:44; A18: 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 A15, A7, A18, A6, A16, AFINSQ_1:18 .= AddTo (a,(intloc 0)) by A17, FUNCOP_1:7 ; ::_thesis: verum end; A19: 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 A20: 0 < i and A21: i < k9 ; ::_thesis: P . (c0 + i) = AddTo (a,(intloc 0)) A22: 0 + 1 <= i by A20, NAT_1:13; thus P . (c0 + i) = (aSeq (a,k9)) . i by A4, A10, A21 .= AddTo (a,(intloc 0)) by A14, A22, A21 ; ::_thesis: verum end; A23: 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 A24: S1[n] ; ::_thesis: S1[n + 1] assume A25: n + 1 <= k9 ; ::_thesis: ( IC (Comput (P,s,(n + 1))) = c0 + (n + 1) & ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) percases ( n = 0 or n > 0 ) ; supposeA26: n = 0 ; ::_thesis: ( IC (Comput (P,s,(n + 1))) = c0 + (n + 1) & ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A12 .= succ (c0 + n) by A2, A26, SCMFSA_2:63 .= (c0 + n) + 1 by NAT_1:38 .= c0 + (n + 1) ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = n + 1 thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A12, A26 .= n + 1 by A1, A26, SCMFSA_2:63 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A27: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A12, A26 .= s . b by A27, SCMFSA_2:63 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A12, A26 .= s . f by SCMFSA_2:63 ; ::_thesis: verum end; supposeA28: n > 0 ; ::_thesis: ( IC (Comput (P,s,(n + 1))) = c0 + (n + 1) & ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) A29: n < k9 by A25, NAT_1:13; A31: n + 0 <= n + 1 by XREAL_1:7; then A32: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A24, A25, PBOOLE:143, XXREAL_0:2 .= AddTo (a,(intloc 0)) by A19, A28, A29 ; A33: 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 A32 ; hence IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by SCMFSA_2:64 .= (c0 + n) + 1 by A24, A25, A31, NAT_1:38, XXREAL_0:2 .= c0 + (n + 1) ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) A34: 0 + 1 <= n by A28, INT_1:7; hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = n + 1 thus (Comput (P,s,(n + 1))) . a = n + ((Comput (P,s,n)) . (intloc 0)) by A24, A25, A34, A31, A33, SCMFSA_2:64, XXREAL_0:2 .= n + 1 by A1, A3, A24, A25, A31, XXREAL_0:2 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A35: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A33, SCMFSA_2:64 .= s . b by A24, A25, A31, A35, XXREAL_0:2 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A33, SCMFSA_2:64 .= s . f by A24, A25, A31, XXREAL_0:2 ; ::_thesis: verum end; end; end; A36: S1[ 0 ] by A2, EXTPRO_1:2; A37: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A36, A23); let i be Element of NAT ; ::_thesis: ( i <= len (aSeq (a,k9)) implies ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = i ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) assume i <= len (aSeq (a,k9)) ; ::_thesis: ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = i ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) hence ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = i ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) by A8, A37; ::_thesis: verum end; hence for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = c0 + i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ; ::_thesis: (Comput (P,s,(len (aSeq (a,k))))) . a = k 1 <= len (aSeq (a,k)) by A6, A8, NAT_1:11; hence (Comput (P,s,(len (aSeq (a,k))))) . a = k by A8, A9; ::_thesis: verum end; supposeA38: k <= 0 ; ::_thesis: ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = c0 + i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) 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 & ( 1 <= $1 implies (Comput (P,s,$1)) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) ); consider k1 being Element of NAT such that A39: k1 + k = 1 and A40: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by A38, Def2; A41: len (aSeq (a,k)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by A40, AFINSQ_1:17 .= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:33 .= (mk + 1) + 1 by A39, CARD_1:64 ; A42: for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) proof A43: for i being Element of NAT st i < (mk + 1) + 1 holds i in dom (aSeq (a,k)) by A41, NAT_1:44; A44: P . (c0 + 0) = (aSeq (a,k)) . 0 by A4, A43 .= a := (intloc 0) by A40, AFINSQ_1:35 ; A45: 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 A46: 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 A2, A44, PBOOLE:143; ::_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 A2, A44, A46, PBOOLE:143 ; ::_thesis: verum end; A47: 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 A48: 1 <= i and A49: i < (mk + 1) + 1 ; ::_thesis: (aSeq (a,k)) . i = SubFrom (a,(intloc 0)) A50: i - 1 < ((mk + 1) + 1) - 1 by A49, XREAL_1:9; reconsider i1 = i - 1 as Element of NAT by A48, INT_1:5; A51: i1 in k1 by A39, A50, NAT_1:44; A52: 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 A40, A48, A52, A39, A49, AFINSQ_1:18 .= SubFrom (a,(intloc 0)) by A51, FUNCOP_1:7 ; ::_thesis: verum end; A53: 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 A54: 0 < i and A55: i < (mk + 1) + 1 ; ::_thesis: P . (c0 + i) = SubFrom (a,(intloc 0)) A56: 0 + 1 <= i by A54, NAT_1:13; thus P . (c0 + i) = (aSeq (a,k)) . i by A4, A43, A55 .= SubFrom (a,(intloc 0)) by A47, A56, A55 ; ::_thesis: verum end; A57: 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 A58: S1[n] ; ::_thesis: S1[n + 1] assume A59: n + 1 <= (mk + 1) + 1 ; ::_thesis: ( IC (Comput (P,s,(n + 1))) = c0 + (n + 1) & ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) percases ( n = 0 or n > 0 ) ; supposeA60: n = 0 ; ::_thesis: ( IC (Comput (P,s,(n + 1))) = c0 + (n + 1) & ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A45 .= succ (c0 + n) by A2, A60, SCMFSA_2:63 .= (c0 + n) + 1 by NAT_1:38 .= c0 + (n + 1) ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A45, A60 .= ((- (n + 1)) + 1) + 1 by A1, A60, SCMFSA_2:63 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A61: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A45, A60 .= s . b by A61, SCMFSA_2:63 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A45, A60 .= s . f by SCMFSA_2:63 ; ::_thesis: verum end; supposeA62: n > 0 ; ::_thesis: ( IC (Comput (P,s,(n + 1))) = c0 + (n + 1) & ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) A63: n < (mk + 1) + 1 by A59, NAT_1:13; A65: n + 0 <= n + 1 by XREAL_1:7; then A66: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A58, A59, PBOOLE:143, XXREAL_0:2 .= SubFrom (a,(intloc 0)) by A53, A62, A63 ; A67: 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 A66 ; hence IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by SCMFSA_2:65 .= (c0 + n) + 1 by A58, A59, A65, NAT_1:38, XXREAL_0:2 .= c0 + (n + 1) ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) A68: 0 + 1 < n + 1 by A62, XREAL_1:6; hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 thus (Comput (P,s,(n + 1))) . a = (((- n) + 1) + 1) - ((Comput (P,s,n)) . (intloc 0)) by A58, A59, A68, A67, NAT_1:13, SCMFSA_2:65 .= (((- n) + 1) + 1) - (s . (intloc 0)) by A3, A58, A59, A65, XXREAL_0:2 .= ((- (n + 1)) + 1) + 1 by A1 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A69: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A67, SCMFSA_2:65 .= s . b by A58, A59, A65, A69, XXREAL_0:2 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A67, SCMFSA_2:65 .= s . f by A58, A59, A65, XXREAL_0:2 ; ::_thesis: verum end; end; end; A70: S1[ 0 ] by A2, EXTPRO_1:2; A71: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A70, A57); let i be Element of NAT ; ::_thesis: ( i <= len (aSeq (a,k)) implies ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) assume i <= len (aSeq (a,k)) ; ::_thesis: ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) hence ( IC (Comput (P,s,i)) = c0 + i & ( 1 <= i implies (Comput (P,s,i)) . a = ((- i) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) by A41, A71; ::_thesis: verum end; hence for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = c0 + i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ; ::_thesis: (Comput (P,s,(len (aSeq (a,k))))) . a = k 1 <= len (aSeq (a,k)) by A41, NAT_1:11; hence (Comput (P,s,(len (aSeq (a,k))))) . a = ((- ((- k) + (1 + 1))) + 1) + 1 by A41, A42 .= k ; ::_thesis: verum end; end; end; theorem Th5: :: SCMFSA_7:5 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) proof let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; ::_thesis: for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) let s be 0 -started State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies for a being Int-Location for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) ) assume A1: s . (intloc 0) = 1 ; ::_thesis: for a being Int-Location for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) let a be Int-Location; ::_thesis: for k being Integer st aSeq (a,k) c= P & a <> intloc 0 holds ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) let k be Integer; ::_thesis: ( aSeq (a,k) c= P & a <> intloc 0 implies ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) ) assume that A2: aSeq (a,k) c= P and A3: a <> intloc 0 ; ::_thesis: ( ( for i being Element of NAT st i <= len (aSeq (a,k)) holds ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k ) A4: for c being Element of NAT st c in dom (aSeq (a,k)) holds (aSeq (a,k)) . c = P . (0 + c) by A2, GRFUNC_1:2; hereby ::_thesis: (Comput (P,s,(len (aSeq (a,k))))) . a = k let i be Element of NAT ; ::_thesis: ( i <= len (aSeq (a,k)) implies ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) assume A5: i <= len (aSeq (a,k)) ; ::_thesis: ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) then IC (Comput (P,s,i)) = 0 + i by A1, A3, A4, Th4; hence ( IC (Comput (P,s,i)) = i & ( for b being Int-Location st b <> a holds (Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) by A1, A3, A4, A5, Th4; ::_thesis: verum end; thus (Comput (P,s,(len (aSeq (a,k))))) . a = k by A1, A3, A4, Th4; ::_thesis: verum end; theorem :: SCMFSA_7:6 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a := k c= P & a <> intloc 0 holds ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) proof let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; ::_thesis: for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for a being Int-Location for k being Integer st a := k c= P & a <> intloc 0 holds ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) let s be 0 -started State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies for a being Int-Location for k being Integer st a := k c= P & a <> intloc 0 holds ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) ) assume A1: s . (intloc 0) = 1 ; ::_thesis: for a being Int-Location for k being Integer st a := k c= P & a <> intloc 0 holds ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) A2: IC s = 0 by MEMSTR_0:def_11; let a be Int-Location; ::_thesis: for k being Integer st a := k c= P & a <> intloc 0 holds ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) let k be Integer; ::_thesis: ( a := k c= P & a <> intloc 0 implies ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) ) assume that A3: a := k c= P and A4: a <> intloc 0 ; ::_thesis: ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) percases ( k > 0 or k <= 0 ) ; supposeA5: k > 0 ; ::_thesis: ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) then consider k1 being Element of NAT such that A6: k1 + 1 = k and A7: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by Def1; A8: 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:33 .= k by A6, CARD_1:64 ; reconsider k = k as Element of NAT by A5, INT_1:3; defpred S1[ Nat] means ( $1 <= k implies ( ( 1 <= $1 implies (Comput (P,s,$1)) . a = $1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) ); set f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>; A9: ((<%(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 ; A10: 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 A8, AFINSQ_1:33 ; A11: 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 A12: i <= k ; ::_thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) i < k + 1 by A12, NAT_1:13; hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by A10, NAT_1:44; ::_thesis: verum end; A13: 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 A14: 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 A11, A14; hence P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A3, A7, GRFUNC_1:2; ::_thesis: verum end; then A15: P . 0 = a := (intloc 0) by A9; A16: 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 A17: 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 A2, A15, PBOOLE:143; ::_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 A2, A15, A17, PBOOLE:143 ; ::_thesis: verum end; A18: 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 A19: 1 <= i and A20: 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 A19, INT_1:5; i - 1 < k - 1 by A20, XREAL_1:9; then A21: i1 in k1 by A6, NAT_1:44; A22: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33; A23: len (k1 --> (AddTo (a,(intloc 0)))) = k1 by CARD_1:64; i in dom (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) by A20, A8, 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 A19, A20, A22, A23, A6, AFINSQ_1:18 .= AddTo (a,(intloc 0)) by A21, FUNCOP_1:7 ; ::_thesis: verum end; A24: 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 A25: 0 < i and A26: i < k ; ::_thesis: P . i = AddTo (a,(intloc 0)) A27: 0 + 1 <= i by A25, NAT_1:13; thus P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A13, A26 .= AddTo (a,(intloc 0)) by A18, A27, A26 ; ::_thesis: verum end; A28: for i being Element of NAT st i <= k holds IC (Comput (P,s,i)) = i proof defpred S2[ 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 A29: i <= k ; ::_thesis: IC (Comput (P,s,i)) = i A30: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A31: S2[n] ; ::_thesis: S2[n + 1] assume A32: n + 1 <= k ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 then A33: n < k by NAT_1:13; percases ( n = 0 or n > 0 ) ; supposeA34: 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 A16 .= succ n by A2, A34, SCMFSA_2:63 .= n + 1 by NAT_1:38 ; ::_thesis: verum end; supposeA35: n > 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 n + 0 <= n + 1 by XREAL_1:7; then A37: CurInstr (P,(Comput (P,s,n))) = P . n by A31, A32, PBOOLE:143, XXREAL_0:2 .= AddTo (a,(intloc 0)) by A24, A33, A35 ; 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 A37 ; hence IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by SCMFSA_2:64 .= n + 1 by A31, A32, NAT_1:13, NAT_1:38 ; ::_thesis: verum end; end; end; A38: S2[ 0 ] by A2, EXTPRO_1:2; for i being Element of NAT holds S2[i] from NAT_1:sch_1(A38, A30); hence IC (Comput (P,s,i)) = i by A29; ::_thesis: verum end; A39: 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 A40: S1[n] ; ::_thesis: S1[n + 1] assume A41: n + 1 <= k ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) percases ( n = 0 or n > 0 ) ; supposeA42: n = 0 ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = n + 1 thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A16, A42 .= n + 1 by A1, A42, SCMFSA_2:63 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A43: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A16, A42 .= s . b by A43, SCMFSA_2:63 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A16, A42 .= s . f by SCMFSA_2:63 ; ::_thesis: verum end; supposeA44: n > 0 ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) A45: n < k by A41, NAT_1:13; A46: P /. (IC (Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by PBOOLE:143; A47: n + 0 <= n + 1 by XREAL_1:7; then A48: CurInstr (P,(Comput (P,s,n))) = P . n by A28, A41, A46, XXREAL_0:2 .= P . n .= AddTo (a,(intloc 0)) by A24, A44, A45 ; A49: 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 A48 ; A50: 0 + 1 <= n by A44, INT_1:7; hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = n + 1 thus (Comput (P,s,(n + 1))) . a = n + ((Comput (P,s,n)) . (intloc 0)) by A40, A41, A50, A47, A49, SCMFSA_2:64, XXREAL_0:2 .= n + 1 by A1, A4, A40, A41, A47, XXREAL_0:2 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A51: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A49, SCMFSA_2:64 .= s . b by A40, A41, A47, A51, XXREAL_0:2 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A49, SCMFSA_2:64 .= s . f by A40, A41, A47, XXREAL_0:2 ; ::_thesis: verum end; end; end; k < k + (len <%(halt SCM+FSA)%>) by XREAL_1:29; then B52: ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . k = <%(halt SCM+FSA)%> . (k - k) by A8, AFINSQ_1:18 .= halt SCM+FSA by AFINSQ_1:34 ; 0 + 1 < k + 1 by A5, XREAL_1:6; then A53: 1 <= k by NAT_1:13; A54: S1[ 0 ] by EXTPRO_1:2; A55: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A54, A39); A56: P /. (IC (Comput (P,s,k))) = P . (IC (Comput (P,s,k))) by PBOOLE:143; A57: CurInstr (P,(Comput (P,s,k))) = P . k by A28, A56 .= halt SCM+FSA by B52, A13 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) then Comput (P,s,k) = Result (P,s) by A57, EXTPRO_1:def_9; hence ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) by A55, A53; ::_thesis: verum end; supposeA58: k <= 0 ; ::_thesis: ( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) then reconsider mk = - k as Element of NAT by INT_1:3; defpred S1[ Nat] means ( $1 <= (mk + 1) + 1 implies ( ( 1 <= $1 implies (Comput (P,s,$1)) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,$1)) . f = s . f ) ) ); consider k1 being Element of NAT such that A59: k1 + k = 1 and A60: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by A58, Def1; A61: 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:33 .= (mk + 1) + 1 by A59, CARD_1:64 ; set f = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>; A62: ((<%(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 ; A63: 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 A61, AFINSQ_1:33 ; A64: now__::_thesis:_for_i_being_Element_of_NAT_st_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: ( i <= (mk + 1) + 1 implies i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) ) assume A65: 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 A65, NAT_1:13; hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by A63, NAT_1:44; ::_thesis: verum end; A66: now__::_thesis:_for_i_being_Element_of_NAT_st_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: ( i <= (mk + 1) + 1 implies P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i ) assume A67: 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 A64, A67; hence P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A3, A60, GRFUNC_1:2; ::_thesis: verum end; then A68: P . 0 = a := (intloc 0) by A62; A69: 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 A70: 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 A2, A68, PBOOLE:143; ::_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 A2, A68, A70, PBOOLE:143 ; ::_thesis: verum end; A71: 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)) A72: 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 A73: 1 <= i and A74: 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 A73, INT_1:5; i - 1 < (k1 + 1) - 1 by A74, A59, XREAL_1:9; then A75: i1 in k1 by NAT_1:44; A76: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 by CARD_1:64; i in dom (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) by A74, A61, 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 A59, A73, A74, A72, A76, AFINSQ_1:18 .= SubFrom (a,(intloc 0)) by A75, FUNCOP_1:7 ; ::_thesis: verum end; A77: 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 A78: 0 < i and A79: i < (mk + 1) + 1 ; ::_thesis: P . i = SubFrom (a,(intloc 0)) A80: 0 + 1 <= i by A78, NAT_1:13; thus P . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A66, A79 .= SubFrom (a,(intloc 0)) by A71, A80, A79 ; ::_thesis: verum end; A81: for i being Element of NAT st i <= (mk + 1) + 1 holds IC (Comput (P,s,i)) = i proof defpred S2[ 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 A82: i <= (mk + 1) + 1 ; ::_thesis: IC (Comput (P,s,i)) = i A83: for n being Element of NAT st S2[n] holds S2[n + 1] proof let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A84: S2[n] ; ::_thesis: S2[n + 1] assume A85: n + 1 <= (mk + 1) + 1 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 then A86: n < (mk + 1) + 1 by NAT_1:13; percases ( n = 0 or n > 0 ) ; supposeA87: 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 A69 .= succ n by A2, A87, SCMFSA_2:63 .= n + 1 by NAT_1:38 ; ::_thesis: verum end; supposeA88: n > 0 ; ::_thesis: IC (Comput (P,s,(n + 1))) = n + 1 n + 0 <= n + 1 by XREAL_1:7; then A90: CurInstr (P,(Comput (P,s,n))) = P . n by A84, A85, PBOOLE:143, XXREAL_0:2 .= SubFrom (a,(intloc 0)) by A77, A86, A88 ; 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 A90 ; hence IC (Comput (P,s,(n + 1))) = succ (IC (Comput (P,s,n))) by SCMFSA_2:65 .= n + 1 by A84, A85, NAT_1:13, NAT_1:38 ; ::_thesis: verum end; end; end; A91: S2[ 0 ] by A2, EXTPRO_1:2; for i being Element of NAT holds S2[i] from NAT_1:sch_1(A91, A83); hence IC (Comput (P,s,i)) = i by A82; ::_thesis: verum end; A92: 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 A93: S1[n] ; ::_thesis: S1[n + 1] assume A94: n + 1 <= (mk + 1) + 1 ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) percases ( n = 0 or n > 0 ) ; supposeA95: n = 0 ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 thus (Comput (P,s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A69, A95 .= ((- (n + 1)) + 1) + 1 by A1, A95, SCMFSA_2:63 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A96: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b thus (Comput (P,s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A69, A95 .= s . b by A96, SCMFSA_2:63 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A69, A95 .= s . f by SCMFSA_2:63 ; ::_thesis: verum end; supposeA97: n > 0 ; ::_thesis: ( ( 1 <= n + 1 implies (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) A98: n < (mk + 1) + 1 by A94, NAT_1:13; A99: P /. (IC (Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by PBOOLE:143; A100: n + 0 <= n + 1 by XREAL_1:7; then A101: CurInstr (P,(Comput (P,s,n))) = P . n by A81, A94, A99, XXREAL_0:2 .= P . n .= SubFrom (a,(intloc 0)) by A77, A97, A98 ; A102: 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 A101 ; A103: 0 + 1 < n + 1 by A97, XREAL_1:6; hereby ::_thesis: ( ( for b being Int-Location st b <> a holds (Comput (P,s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f ) ) assume 1 <= n + 1 ; ::_thesis: (Comput (P,s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 thus (Comput (P,s,(n + 1))) . a = (((- n) + 1) + 1) - ((Comput (P,s,n)) . (intloc 0)) by A93, A94, A103, A102, NAT_1:13, SCMFSA_2:65 .= (((- n) + 1) + 1) - (s . (intloc 0)) by A4, A93, A94, A100, XXREAL_0:2 .= ((- (n + 1)) + 1) + 1 by A1 ; ::_thesis: verum end; hereby ::_thesis: for f being FinSeq-Location holds (Comput (P,s,(n + 1))) . f = s . f let b be Int-Location; ::_thesis: ( b <> a implies (Comput (P,s,(n + 1))) . b = s . b ) assume A104: b <> a ; ::_thesis: (Comput (P,s,(n + 1))) . b = s . b hence (Comput (P,s,(n + 1))) . b = (Comput (P,s,n)) . b by A102, SCMFSA_2:65 .= s . b by A93, A94, A100, A104, XXREAL_0:2 ; ::_thesis: verum end; let f be FinSeq-Location ; ::_thesis: (Comput (P,s,(n + 1))) . f = s . f thus (Comput (P,s,(n + 1))) . f = (Comput (P,s,n)) . f by A102, SCMFSA_2:65 .= s . f by A93, A94, A100, XXREAL_0:2 ; ::_thesis: verum end; end; 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 B105: ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((mk + 1) + 1) = halt SCM+FSA by A61, AFINSQ_1:34, XREAL_1:29; A106: P /. (IC (Comput (P,s,((mk + 1) + 1)))) = P . (IC (Comput (P,s,((mk + 1) + 1)))) by PBOOLE:143; A107: CurInstr (P,(Comput (P,s,((mk + 1) + 1)))) = P . ((mk + 1) + 1) by A81, A106 .= halt SCM+FSA by B105, A66 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) then A108: Comput (P,s,((mk + 1) + 1)) = Result (P,s) by A107, EXTPRO_1:def_9; A109: S1[ 0 ] by EXTPRO_1:2; A110: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A109, A92); ( ((- ((mk + 1) + 1)) + 1) + 1 = k & 0 + 1 <= mk + (1 + 1) ) by XREAL_1:7; hence ( (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds (Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) ) by A110, A108; ::_thesis: verum end; end; end; theorem :: SCMFSA_7:7 for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) proof let P be the InstructionsF of SCM+FSA -valued ManySortedSet of NAT ; ::_thesis: for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) set D = the InstructionsF of SCM+FSA; set V = intloc 2; set I = intloc 1; set O = intloc 0; A1: intloc 1 <> intloc 0 by AMI_3:10; A2: intloc 1 <> intloc 2 by AMI_3:10; let s be 0 -started State of SCM+FSA; ::_thesis: ( s . (intloc 0) = 1 implies for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) ) assume A3: s . (intloc 0) = 1 ; ::_thesis: for f being FinSeq-Location for p being FinSequence of INT st f := p c= P holds ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) let f be FinSeq-Location ; ::_thesis: for p being FinSequence of INT st f := p c= P holds ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) let p be FinSequence of INT ; ::_thesis: ( f := p c= P implies ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) ) assume A4: f := p c= P ; ::_thesis: ( P halts_on s & (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) set q = (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>; A5: 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 A6: 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 = P . i .= ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . i by A4, A6, GRFUNC_1:2 ; ::_thesis: verum end; set q0 = (aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>; consider pp being XFinSequence of such that A7: len pp = len p and A8: 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 A9: aSeq (f,p) = FlattenSeq pp by Def3; len <%(halt SCM+FSA)%> = 1 by AFINSQ_1:34; 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))%>) ^ (FlattenSeq pp))) + 1 by A9, AFINSQ_1:17; then A10: 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 ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) ); A11: intloc 2 <> intloc 0 by AMI_3:10; A12: 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 A13: 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 A14: len r in dom (r ^ <%x%>) by NAT_1:44; assume A15: 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 ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) then A16: dom (r ^ <%x%>) c= dom pp by GRFUNC_1:2; then A17: len r < len pp by A14, NAT_1:44; then consider pr1 being Integer such that A18: pr1 = p . ((len r) + 1) and A19: pp . (len r) = ((aSeq ((intloc 1),((len r) + 1))) ^ (aSeq ((intloc 2),pr1))) ^ <%((f,(intloc 1)) := (intloc 2))%> by A8; ( 1 <= (len r) + 1 & (len r) + 1 <= len pp ) by A17, NAT_1:11, NAT_1:13; then A20: (len r) + 1 in Seg (len pp) ; r c= r ^ <%x%> by AFINSQ_1:74; then consider pp0 being XFinSequence of such that A21: pp0 = r and A22: 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 and A23: ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) and A24: len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p and A25: for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b and A26: for h being FinSeq-Location st h <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . h = s . h by A13, A15, XBOOLE_1:1; A27: x = (r ^ <%x%>) . (len r) by AFINSQ_1:36 .= pp . (len r) by A15, A14, GRFUNC_1:2 ; then x in the InstructionsF of SCM+FSA ^omega by A14, A16, 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 ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) ) thus pp1 = r ^ <%x%> by A21; ::_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 ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) ) reconsider x = x as Element of the InstructionsF of SCM+FSA ^omega by A14, A16, A27, FUNCT_1:102; A28: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <%x%>) by AFINSQ_2:75 .= (FlattenSeq pp0) ^ x by AFINSQ_2:73 ; A29: Seg (len p) = dom p by FINSEQ_1:def_3; len pp1 <= len p by A7, A15, A21, NAT_1:43; then A30: Seg (len pp1) c= Seg (len p) by FINSEQ_1:5; then A31: dom (p | (Seg (len pp1))) = Seg (len pp1) by A29, RELAT_1:62; 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)); set s1 = Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))); set s2 = Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))); A32: x = (aSeq ((intloc 1),((len r) + 1))) ^ ((aSeq ((intloc 2),pr1)) ^ <%((f,(intloc 1)) := (intloc 2))%>) by A19, A27, AFINSQ_1:27; then A33: (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 A28, 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:33 .= ((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 A34: 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; A35: FlattenSeq pp1 c= FlattenSeq pp by A15, A21, AFINSQ_2:82; A36: 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 A35, A28, 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 A37: (((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 A9, 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 A37, XBOOLE_1:1; ::_thesis: verum end; 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 A22; 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; A38: s1 . (intloc 0) = 1 by A1, A11, A3, A25; A39: for c being Element of NAT st c in dom (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 in dom (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 A40: c in dom (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 A41: (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; A42: (((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 A32, A36, AFINSQ_1:74; then A43: 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 A40, 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 A42, A41, GRFUNC_1:2 .= P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) by A4, A43, A41, GRFUNC_1:2 .= P . ((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c) ; ::_thesis: verum end; then A44: (Comput (P,s1,(len (aSeq ((intloc 1),((len r) + 1)))))) . (intloc 1) = (len r) + 1 by Th4, A38, A1; A45: ((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 A28, 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 A36, NAT_1:43; then A46: (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 A34, NAT_1:13; A47: 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 A39, Th4, A38, A1 .= 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; 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))); A48: 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; A49: 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; then A50: Comput (P,s,(len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1)))))) = Comput (P,(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))),(len (aSeq ((intloc 1),((len r) + 1))))) by 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 A49, A50, A39, Th4, A38, A1; 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; A51: s2 . (intloc 0) = 1 by A50, A39, Th4, A38, A1; A52: for c being Element of NAT st c in dom (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 in dom (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 A53: c in dom (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 A54: (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 A19, A27, A36, AFINSQ_1:74; then A55: ((((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 A56: 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 A53, 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 A54, A55, 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 A4, A56, A54, GRFUNC_1:2 .= P . ((len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (aSeq ((intloc 1),((len r) + 1))))) + c) ; ::_thesis: verum end; then A57: (Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . (intloc 2) = pr1 by Th4, A51, A11; A58: (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)))))) . f = (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 2),pr1)))))) . f by AFINSQ_1:17 .= (Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . f by EXTPRO_1:4 .= s2 . f by A52, Th4, A51, A11 .= s1 . f by A50, A39, Th4, A38, A1 ; A59: 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 A52, Th4, A51, A11 .= 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; A60: 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 A61: i < len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) ; ::_thesis: IC (Comput (P,s,i)) = i A62: 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)))_)_) A63: i < (len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) by A61, AFINSQ_1:17; assume A64: 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 A33, A64, A63, 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 A62; 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 A22; ::_thesis: verum end; supposeA65: ( (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 A65, XREAL_1:9; hence i = IC (Comput (P,s,((len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ii))) by A49, A47 .= IC (Comput (P,s,i)) ; ::_thesis: verum end; supposeA66: ( (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 A66, 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 A59 .= IC (Comput (P,s,i)) ; ::_thesis: verum end; end; end; A67: 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 A49, AFINSQ_1:17; A68: 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 PBOOLE:143; (((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 A36; then consider rq being XFinSequence of such that A69: ((((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; A70: 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 A33, AFINSQ_1:17; then A71: 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 A72: 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 A45, A48, AFINSQ_1:66; dom <%((f,(intloc 1)) := (intloc 2))%> = 1 by AFINSQ_1:33; then A73: 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 A74: 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; 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 A48, A60, A68, A71 .= ((((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 A5, A48, A46 .= ((((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 A67, A72, A69, 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 A75: 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 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))))) .= (((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 A74, A19, A27, AFINSQ_1:def_3 .= <%((f,(intloc 1)) := (intloc 2))%> . 0 by A73, AFINSQ_1:def_3 .= (f,(intloc 1)) := (intloc 2) by AFINSQ_1:34 ; A76: 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 A75 ; then A77: IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) = 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 A48, A34, 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 A48, A60, A71 .= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) by A48, A70, NAT_1:38 ; 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: ( ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) ) 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 A78: 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 A78, 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 A60; ::_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 A77; ::_thesis: verum end; end; end; A79: (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)))))) . (intloc 2) = (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 2),pr1)))))) . (intloc 2) by AFINSQ_1:17 .= p . ((len r) + 1) by A18, A57, EXTPRO_1:4 ; consider ki being Element of NAT such that A80: ki = abs ((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)))))) . (intloc 1)) and A81: (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)))))))) . f = ((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)))))) . f) +* (ki,((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)))))) . (intloc 2))) by SCMFSA_2:73; A82: ki = abs ((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 2),pr1)))))) . (intloc 1)) by A80, AFINSQ_1:17 .= abs ((Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . (intloc 1)) by EXTPRO_1:4 .= abs (s2 . (intloc 1)) by A2, A52, Th4, A51, A11 .= (len r) + 1 by A50, A44, ABSVALUE:def_1 ; A83: dom (s1 . f) = Seg (len p) by A24, FINSEQ_1:def_3; for i being Element of NAT st i in Seg (len pp1) holds (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i proof let i be Element of NAT ; ::_thesis: ( i in Seg (len pp1) implies (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ) assume A84: i in Seg (len pp1) ; ::_thesis: (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i then A85: i <= len pp1 by FINSEQ_1:1; len <%x%> = 1 by AFINSQ_1:34; then A86: len pp1 = (len pp0) + 1 by AFINSQ_1:17; percases ( i = len pp1 or i <> len pp1 ) ; supposeA87: i = len pp1 ; ::_thesis: (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i thus (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) . i by A48, A70, A76, A81, A82, A79, A58, A87, A86, FINSEQ_1:4, FUNCT_1:49 .= p . i by A21, A7, A83, A87, A20, A86, FUNCT_7:31 .= (p | (Seg (len pp1))) . i by A87, A86, FINSEQ_1:4, FUNCT_1:49 ; ::_thesis: verum end; supposeA88: i <> len pp1 ; ::_thesis: (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i then i < (len pp0) + 1 by A86, A85, XXREAL_0:1; then A89: i <= len pp0 by NAT_1:13; 1 <= i by A84, FINSEQ_1:1; then A90: i in Seg (len pp0) by A89; (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) . i by A48, A70, A76, A81, A82, A79, A58, A84, FUNCT_1:49 .= (s1 . f) . i by A86, A21, A88, FUNCT_7:32 ; hence (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp0))) . i by A23, A90, FUNCT_1:49 .= p . i by A90, FUNCT_1:49 .= (p | (Seg (len pp1))) . i by A84, FUNCT_1:49 ; ::_thesis: verum end; end; end; then A91: for i being set st i in Seg (len pp1) holds (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . i = (p | (Seg (len pp1))) . i ; A92: dom ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) = dom (s1 . f) by FUNCT_7:30; dom ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = dom ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) by A34, A76, A81, A82, A79, A58, AFINSQ_1:17 .= Seg (len p) by A24, A92, FINSEQ_1:def_3 ; then dom (((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) = Seg (len pp1) by A30, RELAT_1:62; hence ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) = p | (len pp1) by A31, A91, FUNCT_1:2; ::_thesis: ( len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) ) len ((s1 . f) +* (((len r) + 1),(p . ((len r) + 1)))) = len (s1 . f) by A92, FINSEQ_3:29; hence len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) = len p by A24, A34, A76, A81, A82, A79, A58, AFINSQ_1:17; ::_thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g ) ) hereby ::_thesis: for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . g = s . g let b be Int-Location; ::_thesis: ( b <> intloc 1 & b <> intloc 2 implies (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b ) assume that A93: b <> intloc 1 and A94: b <> intloc 2 ; ::_thesis: (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = s . b thus (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . b = (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 2),pr1)))))) . b by A48, A34, A76, SCMFSA_2:73 .= (Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . b by EXTPRO_1:4 .= s2 . b by A52, A94, Th4, A51, A11 .= s1 . b by A50, A39, A93, Th4, A38, A1 .= s . b by A25, A93, A94 ; ::_thesis: verum end; hereby ::_thesis: verum let h be FinSeq-Location ; ::_thesis: ( h <> f implies (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . h ) assume A95: h <> f ; ::_thesis: (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = s . h hence (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h = (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 2),pr1)))))) . h by A48, A34, A76, SCMFSA_2:73 .= (Comput (P,s2,(len (aSeq ((intloc 2),pr1))))) . h by EXTPRO_1:4 .= s2 . h by A52, Th4, A51, A11 .= s1 . h by A50, A39, Th4, A38, A1 .= s . h by A26, A95 ; ::_thesis: verum end; end; set k = len (aSeq ((intloc 1),(len p))); len <%(f :=<0,...,0> (intloc 1))%> = 1 by AFINSQ_1:34; then A96: len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) = (len (aSeq ((intloc 1),(len p)))) + 1 by AFINSQ_1:17; A97: (((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 (((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 aSeq ((intloc 1),(len p)) c= f := p by AFINSQ_1:74; then A98: aSeq ((intloc 1),(len p)) c= P by A4, XBOOLE_1:1; then A99: (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . (intloc 1) = len p by A1, A3, Th5; A100: S1[ {} ] proof A101: 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 A102: i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ; ::_thesis: IC (Comput (P,s,i)) = i ( i < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) implies i <= len (aSeq ((intloc 1),(len p))) ) by A96, NAT_1:13; hence IC (Comput (P,s,i)) = i by A1, A3, A98, A102, Th5; ::_thesis: verum end; 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 ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) reconsider sD = <%> ( the InstructionsF of SCM+FSA ^omega) as XFinSequence of ; take sD ; ::_thesis: ( sD = {} & ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD)) holds IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) ) A103: ((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))%> ; A104: len (aSeq ((intloc 1),(len p))) < len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A96, NAT_1:13; then A105: IC (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) = len (aSeq ((intloc 1),(len p))) by A101; A106: P /. (IC (Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) = P . (IC (Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) by PBOOLE:143; 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 A97, 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 A107: len (aSeq ((intloc 1),(len p))) < len ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) by A96, NAT_1:13; A108: (((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; A109: len (aSeq ((intloc 1),(len p))) in dom ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A104, AFINSQ_1:66; A110: CurInstr (P,(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) = ((((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (aSeq (f,p))) ^ <%(halt SCM+FSA)%>) . (len (aSeq ((intloc 1),(len p)))) by A5, A105, A106, A107 .= ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) . (len (aSeq ((intloc 1),(len p)))) by A108, A109, AFINSQ_1:def_3 .= f :=<0,...,0> (intloc 1) by AFINSQ_1:36 ; thus sD = {} ; ::_thesis: ( ( for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD)) holds IC (Comput (P,s,i)) = i ) & ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) ) A111: 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 A96, EXTPRO_1:3 .= Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len (aSeq ((intloc 1),(len p))))))) by A110 ; then A112: 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 SCMFSA_2:75 .= len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) by A96, A105, NAT_1:38 ; 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 A101, A112; ::_thesis: verum end; hence for i being Element of NAT st i <= len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD)) holds IC (Comput (P,s,i)) = i by A103; ::_thesis: ( ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) & len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) ) consider ki being Element of NAT such that A113: ki = abs ((Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . (intloc 1)) and A114: (Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len (aSeq ((intloc 1),(len p)))))))) . f = ki |-> 0 by SCMFSA_2:75; ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | 0 = p | (len sD) ; hence ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) | (len sD) = p | (len sD) ; ::_thesis: ( len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) ) ki = len p by A99, A113, ABSVALUE:def_1; hence len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . f) = len p by A103, A111, A114, CARD_1:def_7; ::_thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g ) ) now__::_thesis:_for_b_being_Int-Location_st_b_<>_intloc_1_&_b_<>_intloc_2_holds_ (Comput_(P,s,(len_((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>))))_._b_=_s_._b let b be Int-Location; ::_thesis: ( b <> intloc 1 & b <> intloc 2 implies (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . b ) assume that A115: b <> intloc 1 and b <> intloc 2 ; ::_thesis: (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = s . b thus (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . b = (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . b by A111, SCMFSA_2:75 .= s . b by A1, A3, A98, A115, Th5 ; ::_thesis: verum end; hence for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . b = s . b by A103; ::_thesis: for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g now__::_thesis:_for_g_being_FinSeq-Location_st_g_<>_f_holds_ (Comput_(P,s,(len_((aSeq_((intloc_1),(len_p)))_^_<%(f_:=<0,...,0>_(intloc_1))%>))))_._g_=_s_._g let g be FinSeq-Location ; ::_thesis: ( g <> f implies (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g ) assume g <> f ; ::_thesis: (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = s . g hence (Comput (P,s,(len ((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g = (Comput (P,s,(len (aSeq ((intloc 1),(len p)))))) . g by A111, SCMFSA_2:75 .= s . g by A1, A3, A98, Th5 ; ::_thesis: verum end; hence for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq sD))))) . g = s . g by A103; ::_thesis: verum end; for r being XFinSequence holds S1[r] from AFINSQ_1:sch_3(A100, A12); then consider pp0 being XFinSequence of such that A116: pp0 = pp and A117: 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 and A118: ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) = p | (len pp0) and A119: len ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) = len p and A120: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g = s . g ) ) ; A121: P /. (IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) = P . (IC (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) by PBOOLE:143; 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)) by A116, A117; then A122: CurInstr (P,(Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) = ((((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 A5, A10, A121 .= halt SCM+FSA by A9, AFINSQ_1:36 ; hence P halts_on s by EXTPRO_1:29; ::_thesis: ( (Result (P,s)) . f = p & ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) then A123: Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))) = Result (P,s) by A122, EXTPRO_1:def_9; A124: Seg (len pp0) = dom p by A7, A116, FINSEQ_1:def_3; (Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f = ((Comput (P,s,(len (((aSeq ((intloc 1),(len p))) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) by A7, A116, A119, FINSEQ_3:113; hence (Result (P,s)) . f = p by A124, A116, A123, A118, RELAT_1:68; ::_thesis: ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) thus ( ( for b being Int-Location st b <> intloc 1 & b <> intloc 2 holds (Result (P,s)) . b = s . b ) & ( for g being FinSeq-Location st g <> f holds (Result (P,s)) . g = s . g ) ) by A116, A120, A123; ::_thesis: verum end;