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