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 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))
let I, J be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a > 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))
let a be read-write Int-Location ; :: thesis: ( s . a > 0 & J is_closed_on Initialize s & J is_halting_on Initialize s implies IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) )
assume A1: s . a > 0 ; :: thesis: ( not J is_closed_on Initialize s or not J is_halting_on Initialize s or IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) )
assume A2: ( J is_closed_on Initialize s & J is_halting_on Initialize s ) ; :: thesis: IExec (if<0 a,I,J),s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7)))
(Initialize s) . a > 0 by A1, SCMFSA6C:3;
then ( if>0 a,J,I is_closed_on Initialize s & if>0 a,J,I is_halting_on Initialize s ) by A2, Th22;
hence IExec (if<0 a,I,J),s = (IExec (if>0 a,J,I),s) +* (Start-At (insloc (((card (if>0 a,J,I)) + (card J)) + 3))) by A1, Th19
.= (IExec (if>0 a,J,I),s) +* (Start-At (insloc (((((card I) + (card J)) + 4) + (card J)) + 3))) by Th15
.= ((IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) +* (Start-At (insloc (((((card I) + (card J)) + 4) + (card J)) + 3))) by A1, A2, Th23
.= (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) by AMI_1:141 ;
:: thesis: verum