let s be State of SCM+FSA; :: thesis: ( IC s = 0 implies for a being Int-Location
for k being Integer st a := k c= s holds
ProgramPart s halts_on s )
assume A1: IC s = 0 ; :: thesis: for a being Int-Location
for k being Integer st a := k c= s holds
ProgramPart s halts_on s
let a be Int-Location ; :: thesis: for k being Integer st a := k c= s holds
ProgramPart s halts_on s
let k be Integer; :: thesis: ( a := k c= s implies ProgramPart s halts_on s )
assume A2: a := k c= s ; :: thesis: ProgramPart s halts_on s
per cases ( k > 0 or k <= 0 ) ;
suppose A3: k > 0 ; :: thesis: ProgramPart s halts_on s
then consider k1 being Element of NAT such that
A4: k1 + 1 = k and
A5: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by SCMFSA_7:def 2;
A6: 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:38
.= k by A4, CARD_1:106 ;
set f = (<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>;
A7: ((<%(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 ;
reconsider k = k as Element of NAT by A3, INT_1:16;
B9: 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 A6, AFINSQ_1:38 ;
A10: 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 A11: i <= k ; :: thesis: i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>)
i < k + 1 by A11, NAT_1:13;
hence i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) by B9, NAT_1:45; :: thesis: verum
end;
A13: 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 A14: 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 A10, A14;
hence s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A2, A5, GRFUNC_1:8; :: thesis: verum
end;
then A16: s . 0 = a := (intloc 0) by A7;
A17: 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 A18: 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, A16, 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 A18, A1, A16, COMPOS_1:38 ; :: thesis: verum
end;
A20: 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 A4, 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, A6, 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, A4, AFINSQ_1:21
.= AddTo (a,(intloc 0)) by A27, FUNCOP_1:13 ;
:: thesis: verum
end;
A26: 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 A13, A31
.= AddTo (a,(intloc 0)) by A20, A32, A31 ; :: thesis: verum
end;
A30: for i being Element of NAT st i <= k holds
IC (Comput ((ProgramPart s),s,i)) = i
proof
defpred S1[ 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 A31: i <= k ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i
A32: 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 A33: S1[n] ; :: thesis: S1[n + 1]
assume A34: n + 1 <= k ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
then A35: n < k by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A36: 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 A17
.= succ n by A1, A36, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis: verum
end;
suppose A37: n > 0 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
n + 0 <= n + 1 by XREAL_1:9;
then A38: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . n by A33, A34, COMPOS_1:38, XXREAL_0:2
.= s . n by AMI_1:54
.= AddTo (a,(intloc 0)) by A26, A35, A37 ;
A39: 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 A38, AMI_1:123 ;
thus IC (Comput ((ProgramPart s),s,(n + 1))) = succ (IC (Comput ((ProgramPart s),s,n))) by A39, SCMFSA_2:90
.= n + 1 by A33, A34, NAT_1:13, NAT_1:39 ; :: thesis: verum
end;
end;
end;
A40: S1[ 0 ] by A1, EXTPRO_1:3;
for i being Element of NAT holds S1[i] from NAT_1:sch 1(A40, A32);
 hence IC (Comput ((ProgramPart s),s,i)) = i by A31; :: thesis: verum
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 A6, AFINSQ_1:21
.= halt SCM+FSA by AFINSQ_1:38 ;
then A41: s . k = halt SCM+FSA by A13;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,k)) by AMI_1:123;
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = (Comput ((ProgramPart s),s,k)) . (IC (Comput ((ProgramPart s),s,k))) by TX, COMPOS_1:38
.= (Comput ((ProgramPart s),s,k)) . k by A30
.= halt SCM+FSA by A41, AMI_1:54 ;
hence ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: verum
end;
suppose A42: k <= 0 ; :: thesis: ProgramPart s halts_on s
then reconsider mk = - k as Element of NAT by INT_1:16;
consider k1 being Element of NAT such that
A43: k1 + k = 1 and
A44: a := k = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> by A42, SCMFSA_7:def 2;
A45: 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:38
.= (mk + 1) + 1 by A43, CARD_1:106 ;
set f = (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>;
A46: ((<%(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 ;
A47: 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 A45, AFINSQ_1:38 ;
A49: now
let i be Element of NAT ; :: thesis: ( 0 <= i & i <= (mk + 1) + 1 implies i in dom ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) )
assume that
0 <= i and
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 A47, NAT_1:45; :: thesis: verum
end;
A52: now
let i be Element of NAT ; :: thesis: ( 0 <= i & i <= (mk + 1) + 1 implies s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i )
assume that
0 <= i and
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 A49, A73;
hence s . i = ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . i by A2, A44, GRFUNC_1:8; :: thesis: verum
end;
then A55: s . 0 = a := (intloc 0) by A46;
A56: 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 A57: 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, A55, 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 A57, A1, A55, COMPOS_1:38 ; :: thesis: verum
end;
A59: 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, A43, 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, A45, 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 A43, A80, A81, A79, TT, AFINSQ_1:21
.= SubFrom (a,(intloc 0)) by A84, FUNCOP_1:13 ;
:: thesis: verum
end;
A66: 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 A52, A87
.= SubFrom (a,(intloc 0)) by A59, A88, A87 ; :: thesis: verum
end;
A70: for i being Element of NAT st i <= (mk + 1) + 1 holds
IC (Comput ((ProgramPart s),s,i)) = i
proof
defpred S1[ 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 A71: i <= (mk + 1) + 1 ; :: thesis: IC (Comput ((ProgramPart s),s,i)) = i
A72: 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 A73: S1[n] ; :: thesis: S1[n + 1]
assume A74: n + 1 <= (mk + 1) + 1 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
then A75: n < (mk + 1) + 1 by NAT_1:13;
per cases ( n = 0 or n > 0 ) ;
suppose A76: 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 A56
.= succ n by A1, A76, SCMFSA_2:89
.= n + 1 by NAT_1:39 ;
:: thesis: verum
end;
suppose A77: n > 0 ; :: thesis: IC (Comput ((ProgramPart s),s,(n + 1))) = n + 1
n + 0 <= n + 1 by XREAL_1:9;
then A78: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = (Comput ((ProgramPart s),s,n)) . n by A73, A74, COMPOS_1:38, XXREAL_0:2
.= s . n by AMI_1:54
.= SubFrom (a,(intloc 0)) by A66, A75, A77 ;
A79: 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 A78, AMI_1:123 ;
thus IC (Comput ((ProgramPart s),s,(n + 1))) = succ (IC (Comput ((ProgramPart s),s,n))) by A79, SCMFSA_2:91
.= n + 1 by A73, A74, NAT_1:13, NAT_1:39 ; :: thesis: verum
end;
end;
end;
A80: S1[ 0 ] by A1, EXTPRO_1:3;
for i being Element of NAT holds S1[i] from NAT_1:sch 1(A80, A72);
 hence IC (Comput ((ProgramPart s),s,i)) = i by A71; :: thesis: verum
end;
( len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) <= (mk + 1) + 1 & (mk + 1) + 1 < (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) implies ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((mk + 1) + 1) = <%(halt SCM+FSA)%> . (((mk + 1) + 1) - (len (<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))))) ) by AFINSQ_1:21;
then ((<%(a := (intloc 0))%> ^ (k1 --> (SubFrom (a,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((mk + 1) + 1) = halt SCM+FSA by A45, AFINSQ_1:38, XREAL_1:31;
then A81: s . ((mk + 1) + 1) = halt SCM+FSA by A52;
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,((mk + 1) + 1))) by AMI_1:123;
CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,((mk + 1) + 1)))) = (Comput ((ProgramPart s),s,((mk + 1) + 1))) . (IC (Comput ((ProgramPart s),s,((mk + 1) + 1)))) by TX, COMPOS_1:38
.= (Comput ((ProgramPart s),s,((mk + 1) + 1))) . ((mk + 1) + 1) by A70
.= halt SCM+FSA by A81, AMI_1:54 ;
hence ProgramPart s halts_on s by EXTPRO_1:30; :: thesis: verum
end;
end;