let s be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a < 0 & I is_closed_on Initialized s & I is_halting_on Initialized s holds
IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA )
let I, J be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a < 0 & I is_closed_on Initialized s & I is_halting_on Initialized s holds
IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA )
let a be read-write Int-Location ; :: thesis: ( s . a < 0 & I is_closed_on Initialized s & I is_halting_on Initialized s implies IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) )
assume A1: s . a < 0 ; :: thesis: ( not I is_closed_on Initialized s or not I is_halting_on Initialized s or IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) )
assume that
A2: I is_closed_on Initialized s and
A3: I is_halting_on Initialized s ; :: thesis: IExec (if<0 a,I,J),s = (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA )
A4: (Initialized s) . a <= 0 by A1, SCMFSA6C:3;
then A5: if>0 a,J,I is_halting_on Initialized s by A2, A3, Th24;
if>0 a,J,I is_closed_on Initialized s by A2, A3, A4, Th24;
hence IExec (if<0 a,I,J),s = (IExec (if>0 a,J,I),s) +* (Start-At (((card (if>0 a,J,I)) + (card J)) + 3),SCM+FSA ) by A1, A5, Th19
.= (IExec (if>0 a,J,I),s) +* (Start-At (((((card I) + (card J)) + 4) + (card J)) + 3),SCM+FSA ) by Th15
.= ((IExec I,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) +* (Start-At (((((card I) + (card J)) + 4) + (card J)) + 3),SCM+FSA ) by A1, A2, A3, Th25
.= (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) by FUNCT_4:122 ;
:: thesis: verum