THEOREM L_3 (H_LogMatching)

Lines 261–275 · AbstractRaft_IndProofs_test.tla

Obligations Proved

21/21

SMT / Zenon / TLAPM

7 / 0 / 14

Prover Time

1.3s

Claude Code Time

~4 min

Proof Tree