question on synthetic data generation to training data

After a synthetic proof is generated, how is it used as training data? For example, if a synthetic proof has _N_ auxiliary constructions between the premise statement _s_i_ and the conclusion statement _s_N+1_, would you make multiple training data entries from this proof by taking every intermediate statement from doing one auxiliary point construction at a time? i.e. you would generate N-1 data entry from this single N-construction proof:

If each single data entry follows this format
- <_s_i_>< _s_N+1_><_auxiliary construction _i_>
- <_s_i+1_>< _s_N+1_><_auxiliary construction _i+1_>
- <_s_i+2_>< _s_N+1_><_auxiliary construction _i+2_>
- ...
- <_s_N_>< _s_N+1_>N>
where _s_i+1_ is the statements after doing _auxiliary construction _i_ on <_s_i_>

I believe the paper says it made 100M proofs, of which 9M have at least one auxiliary construction. It later also says the fine-tuning used 9M data. How are those proofs with multiple constructions handled? I assume the transformer model only predicts one auxiliary construction at a time. I might have misunderstood this part. Please let me know if I can clarify my questions. Thanks so much for your help.