VerifCond is a verification condition that refers to a SCC of the EFSM. The SCC is named with its index sccIndex, and isInductStep is true if the verification condition is an induction step, and otherwise false. path is then the path considered for this verification condition, and paths are pairs (s{0},[(phi{0},s{1}),...,(phi{N},s{N+1})]) which are just pair (s{0},[(phi{0},s{1})]) in case of induction steps. Also, the invariant used is mentioned, and most important of all, the finally generated verification condition as the proof Goal.