let s be State of ; :: thesis: for I, J being Program of
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 ; :: 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 that
A2: J is_closed_on Initialize s and
A3: 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)))
A4: (Initialize s) . a > 0 by A1, SCMFSA6C:3;
then A5: if>0 a,J,I is_halting_on Initialize s by A2, A3, Th22;
if>0 a,J,I is_closed_on Initialize s by A2, A3, A4, 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, A5, 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, A3, Th23
.= (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) by AMI_1:141 ;
:: thesis: verum