let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 holds
for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
let I be Program of SCM+FSA ; :: thesis: for a being Int-Location st I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 holds
for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
let a be Int-Location ; :: thesis: ( I does_not_refer a & ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & I is_closed_on s1 implies for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
assume A1: I does_not_refer a ; :: thesis: ( ex b being Int-Location st
( a <> b & not s1 . b = s2 . b ) or ex f being FinSeq-Location st not s1 . f = s2 . f or not I is_closed_on s1 or for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
set S2 = s2 +* (I +* (Start-At (insloc 0 )));
set S1 = s1 +* (I +* (Start-At (insloc 0 )));
defpred S1[ State of SCM+FSA , State of SCM+FSA ] means ( ( for b being Int-Location st a <> b holds
$1 . b = $2 . b ) & ( for f being FinSeq-Location holds $1 . f = $2 . f ) );
assume that
A2: for b being Int-Location st a <> b holds
s1 . b = s2 . b and
A3: for f being FinSeq-Location holds s1 . f = s2 . f ; :: thesis: ( not I is_closed_on s1 or for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) )
A4: IC SCM+FSA in dom (I +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A5: now
let f be FinSeq-Location ; :: thesis: (s1 +* (I +* (Start-At (insloc 0 )))) . f = (s2 +* (I +* (Start-At (insloc 0 )))) . f
A6: not f in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:13;
hence (s1 +* (I +* (Start-At (insloc 0 )))) . f = s1 . f by FUNCT_4:12
.= s2 . f by A3
.= (s2 +* (I +* (Start-At (insloc 0 )))) . f by A6, FUNCT_4:12 ;
:: thesis: verum
end;
A7: Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 = s2 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
defpred S2[ Element of NAT ] means ( S1[ Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1, Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1] & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),$1) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),$1) );
A8: I c= I +* (Start-At (insloc 0 )) by SCMFSA8A:9;
A9: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (s1 +* (I +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:13
.= (I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= (s2 +* (I +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by A4, FUNCT_4:14
.= IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by AMI_1:13 ;
I +* (Start-At (insloc 0 )) c= s1 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A10: I c= s1 +* (I +* (Start-At (insloc 0 ))) by A8, XBOOLE_1:1;
A11: now
let b be Int-Location ; :: thesis: ( a <> b implies (s1 +* (I +* (Start-At (insloc 0 )))) . b = (s2 +* (I +* (Start-At (insloc 0 )))) . b )
assume A12: a <> b ; :: thesis: (s1 +* (I +* (Start-At (insloc 0 )))) . b = (s2 +* (I +* (Start-At (insloc 0 )))) . b
A13: not b in dom (I +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
hence (s1 +* (I +* (Start-At (insloc 0 )))) . b = s1 . b by FUNCT_4:12
.= s2 . b by A2, A12
.= (s2 +* (I +* (Start-At (insloc 0 )))) . b by A13, FUNCT_4:12 ;
:: thesis: verum
end;
A14: Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 = s1 +* (I +* (Start-At (insloc 0 ))) by AMI_1:13;
assume A15: I is_closed_on s1 ; :: thesis: for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) )
A16: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) in dom I by A15, SCMFSA7B:def 7;
I +* (Start-At (insloc 0 )) c= s2 +* (I +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A17: I c= s2 +* (I +* (Start-At (insloc 0 ))) by A8, XBOOLE_1:1;
A18: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
A19: Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) ;
A20: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in dom I by A15, SCMFSA7B:def 7;
A21: ProgramPart I = I by AMI_1:105;
then A22: I c= Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) by A17, AMI_1:99;
A23: Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1) = Following (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) by AMI_1:14
.= Exec (CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k)),(Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ;
I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),k by A10, A21, AMI_1:99;
then CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k)) by A20, GRFUNC_1:8;
then CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) in rng I by A20, FUNCT_1:def 5;
then A24: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) does_not_refer a by A1, SCMFSA7B:def 2;
assume A25: S2[k] ; :: thesis: S2[k + 1]
hence S1[ Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1), Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)] by A19, A23, A24, Th37; :: thesis: ( IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) )
thus A26: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A25, A19, A23, A24, Th37; :: thesis: CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1))
A27: IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) in dom I by A15, SCMFSA7B:def 7;
I c= Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1) by A10, A21, AMI_1:99;
hence CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1)) = I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),(k + 1))) by A27, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),(k + 1)) by A22, A26, A27, GRFUNC_1:8 ;
:: thesis: verum
end;
CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 ) = (s1 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 )) by AMI_1:13
.= I . (IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),0 )) by A10, A16, GRFUNC_1:8
.= (s2 +* (I +* (Start-At (insloc 0 )))) . (IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 )) by A17, A9, A16, GRFUNC_1:8
.= CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),0 ) by AMI_1:13 ;
then A28: S2[ 0 ] by A11, A5, A14, A7, A9;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A28, A18);
 hence for k being Element of NAT holds
( ( for b being Int-Location st a <> b holds
(Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . b = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . b ) & ( for f being FinSeq-Location holds (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) . f = (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) . f ) & IC (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) & CurInstr (Computation (s1 +* (I +* (Start-At (insloc 0 )))),k) = CurInstr (Computation (s2 +* (I +* (Start-At (insloc 0 )))),k) ) ; :: thesis: verum