32 (let (stk,loc,C,sig,pc) = f; |
32 (let (stk,loc,C,sig,pc) = f; |
33 (ST,LT) = (phi C sig) ! pc |
33 (ST,LT) = (phi C sig) ! pc |
34 in |
34 in |
35 (\\<exists>rT maxl ins. |
35 (\\<exists>rT maxl ins. |
36 method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and> |
36 method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and> |
37 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and> |
37 (\\<exists>C' mn pTs k. pc = k+1 \\<and> ins!k = (Invoke C' mn pTs) \\<and> |
38 (mn,pTs) = sig0 \\<and> |
38 (mn,pTs) = sig0 \\<and> |
39 (\\<exists>apTs D ST'. |
39 (\\<exists>apTs D ST'. |
40 fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and> |
40 fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and> |
41 length apTs = length pTs \\<and> |
41 length apTs = length pTs \\<and> |
42 (\\<exists>D' rT' maxl' ins'. |
42 (\\<exists>D' rT' maxl' ins'. |