let c0 be Element of NAT ; :: thesis: for s being c0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
let s be c0 -started State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
let P be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
A1: dom P = NAT by PARTFUN1:def 2;
A2: IC s = c0 by MEMSTR_0:def 12;
let a be Int-Location; :: thesis: for k being Integer st ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
let k be Integer; :: thesis: ( ( for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) implies for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i )
assume A3: for c being Element of NAT st c < len (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
A4: for c being Element of NAT st c in dom (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) by A3, AFINSQ_1:66;
per cases ( k > 0 or k <= 0 ) ;
suppose A5: k > 0 ; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
then reconsider k9 = k as Element of NAT by INT_1:3;
consider k1 being Nat such that
A6: k1 + 1 = k9 and
A7: aSeq (a,k9) = <%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0)))) by A5, SCMFSA_7:def 2;
defpred S1[ Nat] means ( $1 <= k9 implies IC (Comput (P,s,$1)) = c0 + $1 );
A8: len (aSeq (a,k9)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (AddTo (a,(intloc 0))))) by A7, AFINSQ_1:17
.= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:34
.= k9 by A6 ;
for i being Element of NAT st i <= len (aSeq (a,k9)) holds
IC (Comput (P,s,i)) = c0 + i
proof
A9: now :: thesis: for i being Element of NAT st 1 <= i & i < k9 holds
(aSeq (a,k9)) . i = AddTo (a,(intloc 0))
let i be Element of NAT ; :: thesis: ( 1 <= i & i < k9 implies (aSeq (a,k9)) . i = AddTo (a,(intloc 0)) )
assume that
A10: 1 <= i and
A11: i < k9 ; :: thesis: (aSeq (a,k9)) . i = AddTo (a,(intloc 0))
reconsider i1 = i - 1 as Element of NAT by A10, INT_1:5;
i = i1 + 1 ;
then i1 < k1 by A11, A6, XREAL_1:6;
then A12: i1 in Segm k1 by NAT_1:44;
A13: len (k1 --> (AddTo (a,(intloc 0)))) = k1 ;
len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33;
hence (aSeq (a,k9)) . i = (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A10, A7, A13, A6, A11, AFINSQ_1:18
.= AddTo (a,(intloc 0)) by A12, FUNCOP_1:7 ;
:: thesis: verum
end;
A14: for i being Element of NAT st i < k9 holds
i in dom (aSeq (a,k9)) by A8, AFINSQ_1:86;
A15: now :: thesis: for i being Nat st 0 < i & i < k9 holds
P . (c0 + i) = AddTo (a,(intloc 0))
let i be Nat; :: thesis: ( 0 < i & i < k9 implies P . (c0 + i) = AddTo (a,(intloc 0)) )
assume that
A16: 0 < i and
A17: i < k9 ; :: thesis: P . (c0 + i) = AddTo (a,(intloc 0))
A18: 0 + 1 <= i by A16, NAT_1:13;
A19: i in NAT by ORDINAL1:def 12;
hence P . (c0 + i) = (aSeq (a,k9)) . i by A4, A14, A17
.= AddTo (a,(intloc 0)) by A9, A18, A17, A19 ;
:: thesis: verum
end;
A20: P . (c0 + 0) = (aSeq (a,k9)) . 0 by A3, A5, A8
.= a := (intloc 0) by A7, AFINSQ_1:35 ;
A21: 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 A22: Comput (P,s,n) = s ; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def 6
.= a := (intloc 0) by A20, A22, MEMSTR_0:def 12 ; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)
thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((a := (intloc 0)),s) by A22, A2, A20, A1, PARTFUN1:def 6 ; :: thesis: verum
end;
A23: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be 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)
per cases ( n = 0 or n > 0 ) ;
suppose A26: n = 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)
hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A21
.= (c0 + 1) + n by A2, A26, SCMFSA_2:63
.= c0 + (n + 1) ;
:: thesis: verum
end;
suppose A27: n > 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)
A28: n < k9 by A25, NAT_1:13;
A29: n + 0 <= n + 1 by XREAL_1:7;
A30: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A24, A25, A29, A1, PARTFUN1:def 6, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A15, A27, A28 ;
A31: 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 A30 ;
thus IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by A31, SCMFSA_2:64
.= (c0 + n) + 1 by A24, A25, A29, XXREAL_0:2
.= c0 + (n + 1) ; :: thesis: verum
end;
end;
end;
let i be Element of NAT ; :: thesis: ( i <= len (aSeq (a,k9)) implies IC (Comput (P,s,i)) = c0 + i )
assume A32: i <= len (aSeq (a,k9)) ; :: thesis: IC (Comput (P,s,i)) = c0 + i
A33: S1[ 0 ] by A2;
for i being Nat holds S1[i] from NAT_1:sch 2(A33, A23);
 hence IC (Comput (P,s,i)) = c0 + i by A8, A32; :: thesis: verum
end;
hence for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i ; :: thesis: verum
end;
suppose A34: k <= 0 ; :: thesis: for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
then reconsider mk = - k as Element of NAT by INT_1:3;
defpred S1[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput (P,s,$1)) = c0 + $1 );
consider k1 being Nat such that
A35: k1 + k = 1 and
A36: aSeq (a,k) = <%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))) by A34, SCMFSA_7:def 2;
A37: len (aSeq (a,k)) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by A36, AFINSQ_1:17
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:34
.= (mk + 1) + 1 by A35 ;
for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i
proof
A38: 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
A39: 1 <= i and
A40: i < (mk + 1) + 1 ; :: thesis: (aSeq (a,k)) . i = SubFrom (a,(intloc 0))
A41: i - 1 < ((mk + 1) + 1) - 1 by A40, XREAL_1:9;
reconsider i1 = i - 1 as Element of NAT by A39, INT_1:5;
A42: i1 in Segm k1 by A35, A41, NAT_1:44;
A43: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 ;
len <%(a := (intloc 0))%> = 1 by AFINSQ_1:33;
hence (aSeq (a,k)) . i = (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A36, A39, A43, A35, A40, AFINSQ_1:18
.= SubFrom (a,(intloc 0)) by A42, FUNCOP_1:7 ;
:: thesis: verum
end;
A44: for i being Element of NAT st i < (mk + 1) + 1 holds
i in dom (aSeq (a,k)) by A37, AFINSQ_1:86;
A45: now :: thesis: for i being Nat st 0 < i & i < (mk + 1) + 1 holds
P . (c0 + i) = SubFrom (a,(intloc 0))
let i be Nat; :: thesis: ( 0 < i & i < (mk + 1) + 1 implies P . (c0 + i) = SubFrom (a,(intloc 0)) )
assume that
A46: 0 < i and
A47: i < (mk + 1) + 1 ; :: thesis: P . (c0 + i) = SubFrom (a,(intloc 0))
A48: 0 + 1 <= i by A46, NAT_1:13;
A49: i in NAT by ORDINAL1:def 12;
hence P . (c0 + i) = (aSeq (a,k)) . i by A4, A44, A47
.= SubFrom (a,(intloc 0)) by A38, A48, A47, A49 ;
:: thesis: verum
end;
A50: P . (c0 + 0) = (aSeq (a,k)) . 0 by A3, A37
.= a := (intloc 0) by A36, AFINSQ_1:35 ;
A51: 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 A52: Comput (P,s,n) = s ; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = a := (intloc 0) & Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s) )
thus CurInstr (P,(Comput (P,s,n))) = P . (IC (Comput (P,s,n))) by A1, PARTFUN1:def 6
.= a := (intloc 0) by A50, A52, MEMSTR_0:def 12 ; :: thesis: Comput (P,s,(n + 1)) = Exec ((a := (intloc 0)),s)
thus Comput (P,s,(n + 1)) = Following (P,(Comput (P,s,n))) by EXTPRO_1:3
.= Exec ((a := (intloc 0)),s) by A52, A2, A50, A1, PARTFUN1:def 6 ; :: thesis: verum
end;
A53: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A54: S1[n] ; :: thesis: S1[n + 1]
assume A55: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)
per cases ( n = 0 or n > 0 ) ;
suppose A56: n = 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)
hence IC (Comput (P,s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC ) by A51
.= (c0 + n) + 1 by A2, A56, SCMFSA_2:63
.= c0 + (n + 1) ;
:: thesis: verum
end;
suppose A57: n > 0 ; :: thesis: IC (Comput (P,s,(n + 1))) = c0 + (n + 1)
A58: n < (mk + 1) + 1 by A55, NAT_1:13;
A59: n + 0 <= n + 1 by XREAL_1:7;
A60: CurInstr (P,(Comput (P,s,n))) = P . (c0 + n) by A54, A55, A59, A1, PARTFUN1:def 6, XXREAL_0:2
.= SubFrom (a,(intloc 0)) by A45, A57, A58 ;
A61: 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 A60 ;
thus IC (Comput (P,s,(n + 1))) = (IC (Comput (P,s,n))) + 1 by A61, SCMFSA_2:65
.= (c0 + n) + 1 by A54, A55, A59, XXREAL_0:2
.= c0 + (n + 1) ; :: thesis: verum
end;
end;
end;
let i be Element of NAT ; :: thesis: ( i <= len (aSeq (a,k)) implies IC (Comput (P,s,i)) = c0 + i )
assume A62: i <= len (aSeq (a,k)) ; :: thesis: IC (Comput (P,s,i)) = c0 + i
A63: S1[ 0 ] by A2;
for i being Nat holds S1[i] from NAT_1:sch 2(A63, A53);
 hence IC (Comput (P,s,i)) = c0 + i by A37, A62; :: thesis: verum
end;
hence for i being Element of NAT st i <= len (aSeq (a,k)) holds
IC (Comput (P,s,i)) = c0 + i ; :: thesis: verum
end;
end;