Lines Matching refs:f2
577 SAFE_DEV f2 (start_f,q,done_f,out) /\
607 DEV f2 (start_f,q,done_f,out) /\
735 DEV f2 (start_f,q,done_f,out) /\
831 DEV f2 (start_f,q,done_f,out) /\
855 DEV f2 (start_f,q,done_f,out) /\ DEV f3 (start_g,q,done_g,data_g)
1162 TOTAL (f1,f2,f3) /\
1167 DEV f2 (start_f,q,done_f,out) /\
1418 `TOTAL (f1,f2,f3) /\
1419 REC (DEV f1) (DEV f2) (DEV f3) (load,inp,done,out) ==>
1420 DEV (TAILREC f1 f2 f3) (load,inp,done,out)`,
1424 THEN `REC (SAFE_DEV f1) (SAFE_DEV f2) (SAFE_DEV f3) (load,inp,done,out)`
1434 THEN `DEV f2 (start_f,q,done_f,out)` by PROVE_TAC [LIV_def,DEV_def]
1441 THEN `DEV f2 (start_f,q,done_f,out)` by PROVE_TAC [LIV_def,DEV_def]
1464 THEN `DEV f2 (start_f,q,done_f,out)` by PROVE_TAC [LIV_def,DEV_def]
1478 THEN `DEV f2 (start_f,q,done_f,out)` by PROVE_TAC [LIV_def,DEV_def]
1491 THEN `DEV f2 (start_f,q,done_f,out)` by PROVE_TAC [LIV_def,DEV_def]