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