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= s & a <> intloc 0 holds
( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) ) )
assume A2: s . (intloc 0) = 1 ; :: thesis: for a being Int-Location
for k being Integer st a := k c= s & a <> intloc 0 holds
( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) )
A1: IC s = 0 by COMPOS_1:def 16;
let a be Int-Location ; :: thesis: for k being Integer st a := k c= s & a <> intloc 0 holds
( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) )
let k be Integer; :: thesis: ( a := k c= s & a <> intloc 0 implies ( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) ) )
assume that
A3: a := k c= s and
A4: a <> intloc 0 ; :: thesis: ( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) )
per cases ( k > 0 or k <= 0 ) ;
suppose A5: k > 0 ; :: thesis: ( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),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 Def2;
A8: len (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) = (len <%(a := (intloc 0))%>) + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:20
.= 1 + (len (k1 --> (AddTo (a,(intloc 0))))) by AFINSQ_1:36
.= k by A6, CARD_1:106 ;
reconsider k = k as Element of NAT by A5, INT_1:16;
defpred S1[ Nat] means ( $1 <= k implies ( ( 1 <= $1 implies (Comput ((ProgramPart s),s,$1)) . a = $1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),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:30
.= a := (intloc 0) by AFINSQ_1:39 ;
B11: 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:20
.= k + 1 by A8, AFINSQ_1:36 ;
A14: now
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 A15: i <= k ; :: thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>)
i < k + 1 by A15, NAT_1:13;
hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by B11, NAT_1:45; :: thesis: verum
end;
A17: now
let i be Element of NAT ; :: thesis: ( i <= k implies s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i )
assume A18: i <= k ; :: thesis: s . 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 A14, A18;
hence s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A3, A7, GRFUNC_1:8; :: thesis: verum
end;
then A20: s . 0 = a := (intloc 0) by A9;
A21: now
let n be Element of NAT ; :: thesis: ( n = 0 implies ( Comput ((ProgramPart s),s,n) = s & CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) & Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s) ) )
assume n = 0 ; :: thesis: ( Comput ((ProgramPart s),s,n) = s & CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) & Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence A22: Comput ((ProgramPart s),s,n) = s by EXTPRO_1:3; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) & Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) by A1, A20, COMPOS_1:38; :: thesis: Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s)
thus Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((a := (intloc 0)),s) by A1, A20, A22, COMPOS_1:38 ; :: thesis: verum
end;
A23: now
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
A24: 1 <= i and
A25: 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 A24, INT_1:18;
i - 1 < k - 1 by A25, XREAL_1:11;
then A27: i1 in k1 by A6, NAT_1:45;
A28: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:36;
TT: len (k1 --> (AddTo (a,(intloc 0)))) = k1 by CARD_1:106;
i in dom (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) by A25, A8, NAT_1:45;
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 4
.= (k1 --> (AddTo (a,(intloc 0)))) . (i - 1) by A24, A25, A28, TT, A6, AFINSQ_1:21
.= AddTo (a,(intloc 0)) by A27, FUNCOP_1:13 ;
:: thesis: verum
end;
A29: now
let i be Element of NAT ; :: thesis: ( 0 < i & i < k implies s . i = AddTo (a,(intloc 0)) )
assume that
A30: 0 < i and
A31: i < k ; :: thesis: s . i = AddTo (a,(intloc 0))
A32: 0 + 1 <= i by A30, NAT_1:13;
thus s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A17, A31
.= AddTo (a,(intloc 0)) by A23, A32, A31 ; :: thesis: verum
end;
A33: for i being Element of NAT st i <= k holds
IC (Comput ((ProgramPart s),s,i)) = i
proof
defpred S2[ Nat] means ( $1 <= k implies IC (Comput ((ProgramPart s),s,$1)) = $1 );
let i be Element of NAT ; :: thesis: ( i <= k implies IC (Comput ((ProgramPart s),s,i)) = i )
assume A34: i <= k ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i
A35: 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 A36: S2[n] ; :: thesis: S2[n + 1]
assume A37: n + 1 <= k ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
then A38: n < k by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A39: n = 0 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
hence IC (Comput ((ProgramPart s),s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC SCM+FSA) by A21
.= succ n by A1, A39, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis: verum
end;
suppose A40: n > 0 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
Y: (ProgramPart (Comput ((ProgramPart s),s,n))) /. (IC (Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . (IC (Comput ((ProgramPart s),s,n))) by COMPOS_1:38;
n + 0 <= n + 1 by XREAL_1:9;
then A41: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = s . n by A36, A37, Y, AMI_1:54, XXREAL_0:2
.= AddTo (a,(intloc 0)) by A29, A38, A40 ;
Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((AddTo (a,(intloc 0))),(Comput ((ProgramPart s),s,n))) by A41, AMI_1:123 ;
hence IC (Comput ((ProgramPart s),s,(n + 1))) = succ (IC (Comput ((ProgramPart s),s,n))) by SCMFSA_2:90
.= n + 1 by A36, A37, NAT_1:13, NAT_1:39 ;
:: thesis: verum
end;
end;
end;
A42: S2[ 0 ] by A1, EXTPRO_1:3;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A42, A35);
 hence IC (Comput ((ProgramPart s),s,i)) = i by A34; :: thesis: verum
end;
A43: 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 A44: S1[n] ; :: thesis: S1[n + 1]
assume A45: n + 1 <= k ; :: thesis: ( ( 1 <= n + 1 implies (Comput ((ProgramPart s),s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
per cases ( n = 0 or n > 0 ) ;
suppose A46: n = 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput ((ProgramPart s),s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . a = n + 1
thus (Comput ((ProgramPart s),s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A21, A46
.= n + 1 by A2, A46, SCMFSA_2:89 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
let b be Int-Location ; :: thesis: ( b <> a implies (Comput ((ProgramPart s),s,(n + 1))) . b = s . b )
assume A47: b <> a ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . b = s . b
thus (Comput ((ProgramPart s),s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A21, A46
.= s . b by A47, SCMFSA_2:89 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
thus (Comput ((ProgramPart s),s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A21, A46
.= s . f by SCMFSA_2:89 ; :: thesis: verum
end;
suppose A48: n > 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput ((ProgramPart s),s,(n + 1))) . a = n + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
A49: n < k by A45, NAT_1:13;
Y: (ProgramPart (Comput ((ProgramPart s),s,n))) /. (IC (Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . (IC (Comput ((ProgramPart s),s,n))) by COMPOS_1:38;
A50: n + 0 <= n + 1 by XREAL_1:9;
then A51: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . n by A33, A45, Y, XXREAL_0:2
.= s . n by AMI_1:54
.= AddTo (a,(intloc 0)) by A29, A48, A49 ;
A52: Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((AddTo (a,(intloc 0))),(Comput ((ProgramPart s),s,n))) by A51, AMI_1:123 ;
A53: 0 + 1 <= n by A48, INT_1:20;
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . a = n + 1
thus (Comput ((ProgramPart s),s,(n + 1))) . a = n + ((Comput ((ProgramPart s),s,n)) . (intloc 0)) by A44, A45, A53, A50, A52, SCMFSA_2:90, XXREAL_0:2
.= n + 1 by A2, A4, A44, A45, A50, XXREAL_0:2 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
let b be Int-Location ; :: thesis: ( b <> a implies (Comput ((ProgramPart s),s,(n + 1))) . b = s . b )
assume A54: b <> a ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . b = s . b
hence (Comput ((ProgramPart s),s,(n + 1))) . b = (Comput ((ProgramPart s),s,n)) . b by A52, SCMFSA_2:90
.= s . b by A44, A45, A50, A54, XXREAL_0:2 ;
:: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
thus (Comput ((ProgramPart s),s,(n + 1))) . f = (Comput ((ProgramPart s),s,n)) . f by A52, SCMFSA_2:90
.= s . f by A44, A45, A50, XXREAL_0:2 ; :: thesis: verum
end;
end;
end;
k < k + (len <%(halt SCM+FSA)%>) by XREAL_1:31;
then ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . k = <%(halt SCM+FSA)%> . (k - k) by A8, AFINSQ_1:21
.= halt SCM+FSA by AFINSQ_1:38 ;
then A55: s . k = halt SCM+FSA by A17;
0 + 1 < k + 1 by A5, XREAL_1:8;
then A56: 1 <= k by NAT_1:13;
A57: S1[ 0 ] by EXTPRO_1:3;
A58: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A57, A43);
Y: (ProgramPart (Comput ((ProgramPart s),s,k))) /. (IC (Comput ((ProgramPart s),s,k))) = (Comput ((ProgramPart s),s,k)) . (IC (Comput ((ProgramPart s),s,k))) by COMPOS_1:38;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,k)) by AMI_1:123;
A59: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = (Comput ((ProgramPart s),s,k)) . k by A33, Y, TX
.= halt SCM+FSA by A55, AMI_1:54 ;
hence ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: ( (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) )
then Comput ((ProgramPart s),s,k) = Result ((ProgramPart s),s) by A59, EXTPRO_1:def 8;
hence ( (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) ) by A58, A56; :: thesis: verum
end;
suppose A60: k <= 0 ; :: thesis: ( ProgramPart s halts_on s & (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) )
then reconsider mk = - k as Element of NAT by INT_1:16;
defpred S1[ Nat] means ( $1 <= (mk + 1) + 1 implies ( ( 1 <= $1 implies (Comput ((ProgramPart s),s,$1)) . a = ((- $1) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,$1)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,$1)) . f = s . f ) ) );
consider k1 being Element of NAT such that
A61: k1 + k = 1 and
A62: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by A60, Def2;
A63: len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) = (len <%(a := (intloc 0))%>) + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:20
.= 1 + (len (k1 --> (SubFrom (a,(intloc 0))))) by AFINSQ_1:36
.= (mk + 1) + 1 by A61, CARD_1:106 ;
set f = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>;
A64: ((<%(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:30
.= a := (intloc 0) by AFINSQ_1:39 ;
B66: 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:20
.= ((mk + 1) + 1) + 1 by A63, AFINSQ_1:36 ;
A69: now
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 A70: 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 A70, NAT_1:13;
hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by B66, NAT_1:45; :: thesis: verum
end;
A72: now
let i be Element of NAT ; :: thesis: ( i <= (mk + 1) + 1 implies s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i )
assume A73: i <= (mk + 1) + 1 ; :: thesis: s . 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 A69, A73;
hence s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A3, A62, GRFUNC_1:8; :: thesis: verum
end;
then A75: s . 0 = a := (intloc 0) by A64;
A76: now
let n be Element of NAT ; :: thesis: ( n = 0 implies ( Comput ((ProgramPart s),s,n) = s & CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) & Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s) ) )
assume n = 0 ; :: thesis: ( Comput ((ProgramPart s),s,n) = s & CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) & Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence A77: Comput ((ProgramPart s),s,n) = s by EXTPRO_1:3; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) & Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s) )
hence CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = a := (intloc 0) by A1, A75, COMPOS_1:38; :: thesis: Comput ((ProgramPart s),s,(n + 1)) = Exec ((a := (intloc 0)),s)
thus Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((a := (intloc 0)),s) by A1, A75, A77, COMPOS_1:38 ; :: thesis: verum
end;
A78: now
A79: len <%(a := (intloc 0))%> = 1 by AFINSQ_1:36;
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
A80: 1 <= i and
A81: 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 A80, INT_1:18;
i - 1 < (k1 + 1) - 1 by A81, A61, XREAL_1:11;
then A84: i1 in k1 by NAT_1:45;
TT: len (k1 --> (SubFrom (a,(intloc 0)))) = k1 by CARD_1:106;
i in dom (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) by A81, A63, NAT_1:45;
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 4
.= (k1 --> (SubFrom (a,(intloc 0)))) . (i - 1) by A61, A80, A81, A79, TT, AFINSQ_1:21
.= SubFrom (a,(intloc 0)) by A84, FUNCOP_1:13 ;
:: thesis: verum
end;
A85: now
let i be Element of NAT ; :: thesis: ( 0 < i & i < (mk + 1) + 1 implies s . i = SubFrom (a,(intloc 0)) )
assume that
A86: 0 < i and
A87: i < (mk + 1) + 1 ; :: thesis: s . i = SubFrom (a,(intloc 0))
A88: 0 + 1 <= i by A86, NAT_1:13;
thus s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A72, A87
.= SubFrom (a,(intloc 0)) by A78, A88, A87 ; :: thesis: verum
end;
A89: for i being Element of NAT st i <= (mk + 1) + 1 holds
IC (Comput ((ProgramPart s),s,i)) = i
proof
defpred S2[ Nat] means ( $1 <= (mk + 1) + 1 implies IC (Comput ((ProgramPart s),s,$1)) = $1 );
let i be Element of NAT ; :: thesis: ( i <= (mk + 1) + 1 implies IC (Comput ((ProgramPart s),s,i)) = i )
assume A90: i <= (mk + 1) + 1 ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i
A91: 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 A92: S2[n] ; :: thesis: S2[n + 1]
assume A93: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
then A94: n < (mk + 1) + 1 by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A95: n = 0 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
hence IC (Comput ((ProgramPart s),s,(n + 1))) = (Exec ((a := (intloc 0)),s)) . (IC SCM+FSA) by A76
.= succ n by A1, A95, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis: verum
end;
suppose A96: n > 0 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
Y: (ProgramPart (Comput ((ProgramPart s),s,n))) /. (IC (Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . (IC (Comput ((ProgramPart s),s,n))) by COMPOS_1:38;
n + 0 <= n + 1 by XREAL_1:9;
then A97: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = s . n by A92, A93, Y, AMI_1:54, XXREAL_0:2
.= SubFrom (a,(intloc 0)) by A85, A94, A96 ;
Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((SubFrom (a,(intloc 0))),(Comput ((ProgramPart s),s,n))) by A97, AMI_1:123 ;
hence IC (Comput ((ProgramPart s),s,(n + 1))) = succ (IC (Comput ((ProgramPart s),s,n))) by SCMFSA_2:91
.= n + 1 by A92, A93, NAT_1:13, NAT_1:39 ;
:: thesis: verum
end;
end;
end;
A98: S2[ 0 ] by A1, EXTPRO_1:3;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A98, A91);
 hence IC (Comput ((ProgramPart s),s,i)) = i by A90; :: thesis: verum
end;
A99: 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 A100: S1[n] ; :: thesis: S1[n + 1]
assume A101: n + 1 <= (mk + 1) + 1 ; :: thesis: ( ( 1 <= n + 1 implies (Comput ((ProgramPart s),s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
per cases ( n = 0 or n > 0 ) ;
suppose A102: n = 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput ((ProgramPart s),s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . a = ((- (n + 1)) + 1) + 1
thus (Comput ((ProgramPart s),s,(n + 1))) . a = (Exec ((a := (intloc 0)),s)) . a by A76, A102
.= ((- (n + 1)) + 1) + 1 by A2, A102, SCMFSA_2:89 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
let b be Int-Location ; :: thesis: ( b <> a implies (Comput ((ProgramPart s),s,(n + 1))) . b = s . b )
assume A103: b <> a ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . b = s . b
thus (Comput ((ProgramPart s),s,(n + 1))) . b = (Exec ((a := (intloc 0)),s)) . b by A76, A102
.= s . b by A103, SCMFSA_2:89 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
thus (Comput ((ProgramPart s),s,(n + 1))) . f = (Exec ((a := (intloc 0)),s)) . f by A76, A102
.= s . f by SCMFSA_2:89 ; :: thesis: verum
end;
suppose A104: n > 0 ; :: thesis: ( ( 1 <= n + 1 implies (Comput ((ProgramPart s),s,(n + 1))) . a = ((- (n + 1)) + 1) + 1 ) & ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
A105: n < (mk + 1) + 1 by A101, NAT_1:13;
Y: (ProgramPart (Comput ((ProgramPart s),s,n))) /. (IC (Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . (IC (Comput ((ProgramPart s),s,n))) by COMPOS_1:38;
A106: n + 0 <= n + 1 by XREAL_1:9;
then A107: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . n by A89, A101, Y, XXREAL_0:2
.= s . n by AMI_1:54
.= SubFrom (a,(intloc 0)) by A85, A104, A105 ;
A108: Comput ((ProgramPart s),s,(n + 1)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,n))) by EXTPRO_1:4
.= Exec ((SubFrom (a,(intloc 0))),(Comput ((ProgramPart s),s,n))) by A107, AMI_1:123 ;
A109: 0 + 1 < n + 1 by A104, XREAL_1:8;
hereby :: thesis: ( ( for b being Int-Location st b <> a holds
(Comput ((ProgramPart s),s,(n + 1))) . b = s . b ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f ) )
assume 1 <= n + 1 ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . a = ((- (n + 1)) + 1) + 1
thus (Comput ((ProgramPart s),s,(n + 1))) . a = (((- n) + 1) + 1) - ((Comput ((ProgramPart s),s,n)) . (intloc 0)) by A100, A101, A109, A108, NAT_1:13, SCMFSA_2:91
.= (((- n) + 1) + 1) - (s . (intloc 0)) by A4, A100, A101, A106, XXREAL_0:2
.= ((- (n + 1)) + 1) + 1 by A2 ; :: thesis: verum
end;
hereby :: thesis: for f being FinSeq-Location holds (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
let b be Int-Location ; :: thesis: ( b <> a implies (Comput ((ProgramPart s),s,(n + 1))) . b = s . b )
assume A110: b <> a ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . b = s . b
hence (Comput ((ProgramPart s),s,(n + 1))) . b = (Comput ((ProgramPart s),s,n)) . b by A108, SCMFSA_2:91
.= s . b by A100, A101, A106, A110, XXREAL_0:2 ;
:: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (Comput ((ProgramPart s),s,(n + 1))) . f = s . f
thus (Comput ((ProgramPart s),s,(n + 1))) . f = (Comput ((ProgramPart s),s,n)) . f by A108, SCMFSA_2:91
.= s . f by A100, A101, A106, 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:21;
then ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((mk + 1) + 1) = halt SCM+FSA by A63, AFINSQ_1:38, XREAL_1:31;
then A111: s . ((mk + 1) + 1) = halt SCM+FSA by A72;
Y: (ProgramPart (Comput ((ProgramPart s),s,((mk + 1) + 1)))) /. (IC (Comput ((ProgramPart s),s,((mk + 1) + 1)))) = (Comput ((ProgramPart s),s,((mk + 1) + 1))) . (IC (Comput ((ProgramPart s),s,((mk + 1) + 1)))) by COMPOS_1:38;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((mk + 1) + 1))) by AMI_1:123;
A112: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,((mk + 1) + 1)))) = (Comput ((ProgramPart s),s,((mk + 1) + 1))) . ((mk + 1) + 1) by A89, Y, TX
.= halt SCM+FSA by A111, AMI_1:54 ;
hence ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: ( (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) )
then A113: Comput ((ProgramPart s),s,((mk + 1) + 1)) = Result ((ProgramPart s),s) by A112, EXTPRO_1:def 8;
A114: S1[ 0 ] by EXTPRO_1:3;
A115: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A114, A99);
 ( ((- ((mk + 1) + 1)) + 1) + 1 = k & 0 + 1 <= mk + (1 + 1) ) by XREAL_1:9;
hence ( (Result ((ProgramPart s),s)) . a = k & ( for b being Int-Location st b <> a holds
(Result ((ProgramPart s),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result ((ProgramPart s),s)) . f = s . f ) ) by A115, A113; :: thesis: verum
end;
end;