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