set a2 = intloc 2;
set a1 = intloc 1;
let s be State of SCM+FSA ; :: thesis: ( IC s = 0 implies for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
ProgramPart s halts_on s )
set D = the Instructions of SCM+FSA ;
assume A1: IC s = 0 ; :: thesis: for f being FinSeq-Location
for p being FinSequence of INT st f := p c= s holds
ProgramPart s halts_on s
let f be FinSeq-Location ; :: thesis: for p being FinSequence of INT st f := p c= s holds
ProgramPart s halts_on s
let p be FinSequence of INT ; :: thesis: ( f := p c= s implies ProgramPart s halts_on s )
set q = (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>;
set q0 = (aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>;
A2: f := p = Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:def 5;
assume A3: f := p c= s ; :: thesis: ProgramPart s halts_on s
A4: now
let i be Element of NAT ; :: thesis: ( i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume A5: i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then s . i = (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . i by A3, A2, GRFUNC_1:8;
then A6: s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (i + 1) by A5, SCMFSA_7:def 1;
i + 1 in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A5, SCMFSA_7:26;
hence s . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A6, PARTFUN1:def 8; :: thesis: verum
end;
A7: now
let i, k be Element of NAT ; :: thesis: ( i < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) implies (Comput (ProgramPart s),s,k) . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) )
assume i < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) ; :: thesis: (Comput (ProgramPart s),s,k) . i = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1)
then A8: i in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by SCMFSA_7:29;
thus (Comput (ProgramPart s),s,k) . i = s . i by AMI_1:54
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (i + 1) by A4, A8 ; :: thesis: verum
end;
consider pp being FinSequence of the Instructions of SCM+FSA * such that
A9: ( len pp = len p & ( for k being Element of NAT st 1 <= k & k <= len p holds
ex i being Integer st
( i = p . k & pp . k = ((aSeq (intloc 1),k) ^ (aSeq (intloc 2),i)) ^ <*(f,(intloc 1) := (intloc 2))*> ) ) ) and
A10: aSeq f,p = FlattenSeq pp by SCMFSA_7:def 4;
len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))) + 1 by A10, FINSEQ_2:19;
then A11: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:13;
defpred S1[ FinSequence] means ( $1 c= pp implies ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = $1 & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) ) );
A12: now
let k be Element of NAT ; :: thesis: ( k in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) implies (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) )
assume A13: k in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) ; :: thesis: (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1)
then A14: k + 1 in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:26;
thus (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . k = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) /. (k + 1) by A13, SCMFSA_7:def 1
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (k + 1) by A14, PARTFUN1:def 8 ; :: thesis: verum
end;
A15: for r being FinSequence
for x being set st S1[r] holds
S1[r ^ <*x*>]
proof
let r be FinSequence; :: thesis: for x being set st S1[r] holds
S1[r ^ <*x*>]
let x be set ; :: thesis: ( S1[r] implies S1[r ^ <*x*>] )
assume A16: S1[r] ; :: thesis: S1[r ^ <*x*>]
set r1 = (len r) + 1;
len (r ^ <*x*>) = (len r) + 1 by FINSEQ_2:19;
then (len r) + 1 in Seg (len (r ^ <*x*>)) by FINSEQ_1:6;
then A17: (len r) + 1 in dom (r ^ <*x*>) by FINSEQ_1:def 3;
assume A18: r ^ <*x*> c= pp ; :: thesis: ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = r ^ <*x*> & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) )
then A19: dom (r ^ <*x*>) c= dom pp by GRFUNC_1:8;
then (len r) + 1 in dom pp by A17;
then (len r) + 1 in Seg (len pp) by FINSEQ_1:def 3;
then ( 1 <= (len r) + 1 & (len r) + 1 <= len pp ) by FINSEQ_1:3;
then consider pr1 being Integer such that
pr1 = p . ((len r) + 1) and
A20: pp . ((len r) + 1) = ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*> by A9;
r c= r ^ <*x*> by FINSEQ_6:12;
then consider pp0 being FinSequence of the Instructions of SCM+FSA * such that
A21: pp0 = r and
A22: for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i by A16, A18, XBOOLE_1:1;
A23: x = (r ^ <*x*>) . ((len r) + 1) by FINSEQ_1:59
.= pp . ((len r) + 1) by A18, A17, GRFUNC_1:8 ;
then x in the Instructions of SCM+FSA * by A17, A19, FINSEQ_2:13;
then <*x*> is FinSequence of the Instructions of SCM+FSA * by FINSEQ_1:95;
then reconsider pp1 = pp0 ^ <*x*> as FinSequence of the Instructions of SCM+FSA * by FINSEQ_1:96;
take pp1 ; :: thesis: ( pp1 = r ^ <*x*> & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i ) )
thus pp1 = r ^ <*x*> by A21; :: thesis: for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i
reconsider x = x as Element of the Instructions of SCM+FSA * by A17, A19, A23, FINSEQ_2:13;
A24: FlattenSeq pp1 = (FlattenSeq pp0) ^ (FlattenSeq <*x*>) by PRE_POLY:3
.= (FlattenSeq pp0) ^ x by PRE_POLY:1 ;
set c2 = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)));
set c1 = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0));
A25: 1 <= ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + 1 by NAT_1:11;
A26: x = (aSeq (intloc 1),((len r) + 1)) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>) by A20, A23, FINSEQ_1:45;
then A27: (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (FlattenSeq pp1)) = (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (((FlattenSeq pp0) ^ (aSeq (intloc 1),((len r) + 1))) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>))) by A24, FINSEQ_1:45
.= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (((FlattenSeq pp0) ^ (aSeq (intloc 1),((len r) + 1))) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>))) by FINSEQ_1:35
.= len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>)) by Lm2
.= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len ((aSeq (intloc 2),pr1) ^ <*(f,(intloc 1) := (intloc 2))*>)) by FINSEQ_1:35
.= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + ((len (aSeq (intloc 2),pr1)) + (len <*(f,(intloc 1) := (intloc 2))*>)) by FINSEQ_1:35
.= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + ((len (aSeq (intloc 2),pr1)) + 1) by FINSEQ_1:56
.= ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + 1 ;
then A28: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) = ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + 1 by FINSEQ_1:35;
then A29: len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) > (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) by NAT_1:13;
A30: FlattenSeq pp1 c= FlattenSeq pp by A18, A21, PRE_POLY:6;
A31: now
let p be FinSequence; :: thesis: ( p c= x implies (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> )
assume p c= x ; :: thesis: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>
then (FlattenSeq pp0) ^ p c= (FlattenSeq pp0) ^ x by FINSEQ_6:15;
then (FlattenSeq pp0) ^ p c= FlattenSeq pp by A30, A24, XBOOLE_1:1;
then ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ ((FlattenSeq pp0) ^ p) c= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp) by FINSEQ_6:15;
then A32: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ p c= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp) by FINSEQ_1:45;
((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A10, FINSEQ_6:12;
hence (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ p c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A32, XBOOLE_1:1; :: thesis: verum
end;
A33: ( IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) & ( for c being Element of NAT st c < len (aSeq (intloc 1),((len r) + 1)) holds
(aSeq (intloc 1),((len r) + 1)) . (c + 1) = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) ) )
proof
thus IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) by A22; :: thesis: for c being Element of NAT st c < len (aSeq (intloc 1),((len r) + 1)) holds
(aSeq (intloc 1),((len r) + 1)) . (c + 1) = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c)
let c be Element of NAT ; :: thesis: ( c < len (aSeq (intloc 1),((len r) + 1)) implies (aSeq (intloc 1),((len r) + 1)) . (c + 1) = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) )
assume c < len (aSeq (intloc 1),((len r) + 1)) ; :: thesis: (aSeq (intloc 1),((len r) + 1)) . (c + 1) = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c)
then ( 1 <= c + 1 & c + 1 <= len (aSeq (intloc 1),((len r) + 1)) ) by NAT_1:11, NAT_1:13;
then A34: c + 1 in dom (aSeq (intloc 1),((len r) + 1)) by FINSEQ_3:27;
then A35: (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (c + 1) in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) by FINSEQ_1:41;
A36: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A26, A31, FINSEQ_6:12;
then dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) c= dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
then ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) + 1 in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A35;
then A37: (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by SCMFSA_7:26;
thus (aSeq (intloc 1),((len r) + 1)) . (c + 1) = ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (c + 1)) by A34, FINSEQ_1:def 7
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) + 1) by A36, A35, GRFUNC_1:8
.= (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) by A12, A37
.= s . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) by A3, A2, A37, GRFUNC_1:8
.= (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + c) by AMI_1:54 ; :: thesis: verum
end;
set c3 = len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1));
A38: len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) = (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len (aSeq (intloc 1),((len r) + 1))) by FINSEQ_1:35;
then A39: len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) = ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) by FINSEQ_1:35;
len <*(f,(intloc 1) := (intloc 2))*> <= (len ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1))) + (len <*(f,(intloc 1) := (intloc 2))*>) by NAT_1:12;
then len <*(f,(intloc 1) := (intloc 2))*> <= len (((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*>) by FINSEQ_1:35;
then A40: 1 <= len x by A20, A23, FINSEQ_1:57;
A41: 1 <= len <*(f,(intloc 1) := (intloc 2))*> by FINSEQ_1:57;
A42: ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1) = (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x by A24, FINSEQ_1:45;
then len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A31, FINSEQ_1:84;
then A43: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A28, NAT_1:13;
A44: len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) = (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) by FINSEQ_1:35;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) by AMI_1:123;
A45: Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) = Comput (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),(len (aSeq (intloc 1),((len r) + 1))) by A38, AMI_1:51;
A46: ( IC (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) & ( for c being Element of NAT st c < len (aSeq (intloc 2),pr1) holds
(aSeq (intloc 2),pr1) . (c + 1) = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) ) )
proof
thus IC (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) = len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) by A38, A45, A33, Lm5, T; :: thesis: for c being Element of NAT st c < len (aSeq (intloc 2),pr1) holds
(aSeq (intloc 2),pr1) . (c + 1) = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c)
let c be Element of NAT ; :: thesis: ( c < len (aSeq (intloc 2),pr1) implies (aSeq (intloc 2),pr1) . (c + 1) = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) )
assume c < len (aSeq (intloc 2),pr1) ; :: thesis: (aSeq (intloc 2),pr1) . (c + 1) = (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c)
then ( 1 <= c + 1 & c + 1 <= len (aSeq (intloc 2),pr1) ) by NAT_1:11, NAT_1:13;
then A47: c + 1 in dom (aSeq (intloc 2),pr1) by FINSEQ_3:27;
then A48: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (c + 1) in dom (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) by FINSEQ_1:41;
(((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by A20, A23, A31, FINSEQ_6:12;
then A49: ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1) c= (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> by FINSEQ_1:45;
then dom (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) c= dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by GRFUNC_1:8;
then ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) + 1 in dom ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A48;
then A50: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c in dom (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) by SCMFSA_7:26;
thus (aSeq (intloc 2),pr1) . (c + 1) = (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (c + 1)) by A47, FINSEQ_1:def 7
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) + 1) by A48, A49, GRFUNC_1:8
.= (Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>)) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) by A12, A50
.= s . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) by A3, A2, A50, GRFUNC_1:8
.= (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) . ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + c) by AMI_1:54 ; :: thesis: verum
end;
A51: now
let i be Element of NAT ; :: thesis: ( i <= len (aSeq (intloc 2),pr1) implies (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i = IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i)) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))) by AMI_1:123;
assume i <= len (aSeq (intloc 2),pr1) ; :: thesis: (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i = IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i))
hence (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i = IC (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))))),i) by A46, Lm5, T
.= IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + i)) by AMI_1:51 ;
:: thesis: verum
end;
A52: now
let i be Element of NAT ; :: thesis: ( i <= len (aSeq (intloc 1),((len r) + 1)) implies (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i)) )
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))) by AMI_1:123;
assume i <= len (aSeq (intloc 1),((len r) + 1)) ; :: thesis: (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i))
hence (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i = IC (Comput (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)))),i) by A33, Lm5, T
.= IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + i)) by AMI_1:51 ;
:: thesis: verum
end;
A53: for i being Element of NAT st i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i
proof
let i be Element of NAT ; :: thesis: ( i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) implies IC (Comput (ProgramPart s),s,i) = i )
assume A54: i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
A55: now
A56: i < (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len (FlattenSeq pp1)) by A54, FINSEQ_1:35;
assume A57: not i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ; :: thesis: ( ( not (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) implies ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) )
assume ( not (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i or not i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) ; :: thesis: ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) )
hence ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) by A27, A57, A56, NAT_1:13; :: thesis: verum
end;
per cases ( i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) or ( (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) or ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) ) by A55;
suppose i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
hence IC (Comput (ProgramPart s),s,i) = i by A22; :: thesis: verum
end;
suppose A58: ( (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1 <= i & i <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + 1) - (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) <= i - (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) by XREAL_1:11;
then reconsider ii = i - (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) as Element of NAT by INT_1:16;
i - (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) - (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) by A58, XREAL_1:11;
then i = IC (Comput (ProgramPart s),s,((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + ii)) by A38, A52;
hence IC (Comput (ProgramPart s),s,i) = i ; :: thesis: verum
end;
suppose A59: ( (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1 <= i & i <= (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1)) ) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + 1) - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) <= i - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) by XREAL_1:11;
then reconsider ii = i - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) as Element of NAT by INT_1:16;
i - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) <= ((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) - (len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) by A59, XREAL_1:11;
hence i = IC (Comput (ProgramPart s),s,((len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1)))) + ii)) by A51
.= IC (Comput (ProgramPart s),s,i) ;
:: thesis: verum
end;
end;
end;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) /. (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) = (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) = (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) by Y, COMPOS_1:def 10
.= (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) . (len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) by A44, A53, A29
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) + 1) by A7, A44, A43
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) + 1) by A42, A44, A31, A28, A25, FINSEQ_4:98
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x) . ((((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len (aSeq (intloc 1),((len r) + 1)))) + (len (aSeq (intloc 2),pr1))) + (len <*(f,(intloc 1) := (intloc 2))*>)) by A39, FINSEQ_1:57
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + ((len (aSeq (intloc 1),((len r) + 1))) + ((len (aSeq (intloc 2),pr1)) + (len <*(f,(intloc 1) := (intloc 2))*>))))
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ x) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0))) + (len x)) by A20, A23, Lm3
.= x . (len x) by A40, FINSEQ_1:86 ;
then A60: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) = (((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1)) ^ <*(f,(intloc 1) := (intloc 2))*>) . ((len ((aSeq (intloc 1),((len r) + 1)) ^ (aSeq (intloc 2),pr1))) + (len <*(f,(intloc 1) := (intloc 2))*>)) by A20, A23, FINSEQ_1:35
.= <*(f,(intloc 1) := (intloc 2))*> . (len <*(f,(intloc 1) := (intloc 2))*>) by A41, FINSEQ_1:86
.= <*(f,(intloc 1) := (intloc 2))*> . 1 by FINSEQ_1:57
.= f,(intloc 1) := (intloc 2) by FINSEQ_1:57 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by AMI_1:123;
Comput (ProgramPart s),s,((len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by AMI_1:14
.= Exec (f,(intloc 1) := (intloc 2)),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1)))) by A60, T, AMI_1:def 18 ;
then A61: IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)))) = (Exec (f,(intloc 1) := (intloc 2)),(Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) . (IC SCM+FSA ) by A44, A28, COMPOS_1:def 9
.= succ (IC (Comput (ProgramPart s),s,(len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))))) by SCMFSA_2:99
.= succ (len (((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) ^ (aSeq (intloc 1),((len r) + 1))) ^ (aSeq (intloc 2),pr1))) by A44, A53, A29 ;
thus for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) holds
IC (Comput (ProgramPart s),s,i) = i :: thesis: verum
proof
let i be Element of NAT ; :: thesis: ( i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) implies IC (Comput (ProgramPart s),s,i) = i )
assume A62: i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
per cases ( i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) or i = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ) by A62, XXREAL_0:1;
suppose i < len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
hence IC (Comput (ProgramPart s),s,i) = i by A53; :: thesis: verum
end;
suppose i = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp1)) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
hence IC (Comput (ProgramPart s),s,i) = i by A44, A28, A61, NAT_1:39; :: thesis: verum
end;
end;
end;
end;
set k = len (aSeq (intloc 1),(len p));
A63: len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) = (len (aSeq (intloc 1),(len p))) + 1 by FINSEQ_2:19;
(((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>) by FINSEQ_1:45
.= (aSeq (intloc 1),(len p)) ^ (<*(f :=<0,...,0> (intloc 1))*> ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by FINSEQ_1:45 ;
then A64: Load (aSeq (intloc 1),(len p)) c= f := p by A2, SCMFSA_7:31;
A65: S1[ {} ]
proof
assume {} c= pp ; :: thesis: ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = {} & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) )
take <*> (the Instructions of SCM+FSA * ) ; :: thesis: ( <*> (the Instructions of SCM+FSA * ) = {} & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Comput (ProgramPart s),s,i) = i ) )
thus <*> (the Instructions of SCM+FSA * ) = {} ; :: thesis: for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Comput (ProgramPart s),s,i) = i
A66: 1 <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A63, NAT_1:11;
A67: (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*> = ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ ((aSeq f,p) ^ <*(halt SCM+FSA )*>) by FINSEQ_1:45;
then len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) = (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) + (len ((aSeq f,p) ^ <*(halt SCM+FSA )*>)) by FINSEQ_1:35;
then len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) <= len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by NAT_1:11;
then A68: len (aSeq (intloc 1),(len p)) < len ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by A63, NAT_1:13;
A69: now
let i be Element of NAT ; :: thesis: ( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies IC (Comput (ProgramPart s),s,i) = i )
assume A70: i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies i <= len (aSeq (intloc 1),(len p)) ) by A63, NAT_1:13;
hence IC (Comput (ProgramPart s),s,i) = i by A1, A3, A64, A70, Lm6, XBOOLE_1:1; :: thesis: verum
end;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) /. (IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) = (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . (IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) by COMPOS_1:38;
len (aSeq (intloc 1),(len p)) < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A63, NAT_1:13;
then A71: IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) = len (aSeq (intloc 1),(len p)) by A69;
then A72: CurInstr (ProgramPart (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) = (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) . (len (aSeq (intloc 1),(len p))) by Y, COMPOS_1:def 10
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) by A63, A7, A68
.= ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) . (len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) by A67, A66, FINSEQ_1:85
.= f :=<0,...,0> (intloc 1) by A63, FINSEQ_1:59 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) by AMI_1:123;
A73: Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>)) = Following (ProgramPart s),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) by A63, AMI_1:14
.= Exec (f :=<0,...,0> (intloc 1)),(Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p)))) by A72, T, AMI_1:def 18 ;
A74: IC (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) = (Comput (ProgramPart s),s,(len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>))) . (IC SCM+FSA ) by COMPOS_1:def 9
.= succ (IC (Comput (ProgramPart s),s,(len (aSeq (intloc 1),(len p))))) by A73, SCMFSA_2:101
.= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) by A63, A71, NAT_1:39 ;
A75: now
let i be Element of NAT ; :: thesis: ( i <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) implies IC (Comput (ProgramPart s),s,i) = i )
assume i <= len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ; :: thesis: IC (Comput (ProgramPart s),s,i) = i
then ( i < len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) or i = len ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ) by XXREAL_0:1;
hence IC (Comput (ProgramPart s),s,i) = i by A69, A74; :: thesis: verum
end;
((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * ))) = ((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (<*> the Instructions of SCM+FSA ) by PRE_POLY:2
.= (aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*> by FINSEQ_1:47 ;
hence for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq (<*> (the Instructions of SCM+FSA * )))) holds
IC (Comput (ProgramPart s),s,i) = i by A75; :: thesis: verum
end;
Y: (ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))))) /. (IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))))) = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)))) . (IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))))) by COMPOS_1:38;
TX: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)))) by AMI_1:123;
for r being FinSequence holds S1[r] from FINSEQ_1:sch 3(A65, A15);
 then ex pp0 being FinSequence of the Instructions of SCM+FSA * st
( pp0 = pp & ( for i being Element of NAT st i <= len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp0)) holds
IC (Comput (ProgramPart s),s,i) = i ) ) ;
then IC (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)))) = len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)) ;
then CurInstr (ProgramPart s),(Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)))) = (Comput (ProgramPart s),s,(len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp)))) . (len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))) by Y, TX, COMPOS_1:def 10
.= ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) . ((len (((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (FlattenSeq pp))) + 1) by A7, A11
.= halt SCM+FSA by A10, FINSEQ_1:59 ;
hence ProgramPart s halts_on s by AMI_1:146; :: thesis: verum