The reason the formula only talks about the initial state is that it does not contain any temporal operator. If you want to prove that it holds for all states, you should writeTHEOREM Spec => [](diag = tdiag)This is an invariant, and from a quick glance at the algorithm it appears that it is inductive. You can prove it as follows:<1>1. Init => (diag = tdiag)<1>2. (diag = tdiag) /\ [Next]_vars => (diag = tdiag)'<1>. QED  BY <1>1, <1>2, PTL DEF Spec(You'll have to write proofs for the steps <1>1 and <1>2 in order to complete the proof.) If this doesn't make sense to you, please have a look at the TLAPS tutorial [1].Stephan[1] http://proofs.tlapl.us/doc/web/content/Documentation/Tutorial/The_example.htmlOn 15 Apr 2020, at 18:10, christina.a.burge@xxxxxxxxx wrote:Another quick question:I can see that my assertion only talks about the initial state (I'm guessing that's what the 'Init', in  "BY DEF Spec, Init" does.)Is there a reason why that would not be sufficient proof for my spec? Do you mean that it's just comparing two empty lists?On Wednesday, April 15, 2020 at 4:11:06 PM UTC+1, Stephan Merz wrote:1. Your algorithm is written in PlusCal, which appears as a comment to TLA+. You first need to generate the TLA+ specification (File -> Translate PlusCal Algorithm in the Toolbox).2. Your theorem should then be stated as a consequence of the specification in the formTHEOREM diagseq == Spec => (diag = tdiag)Its proof will look like "BY DEF Spec, Init". Note that your assertion only talks about the initial state.Regards,StephanOn 15 Apr 2020, at 17:04, christi...@xxxxxxxxx wrote:Hi!I've written a specification to transpose a matrix, but I don't know how I use TLAPS to prove correctness. I've tried:`---- MODULE transp ----EXTENDS Naturals, TLCCONSTANT n, m(* --algorithm transposevariables i=1, j=1, array = <<<<>>,<<>>>>,transp = <<<<>>,<<>>>>, diag = <<>>, tdiag = <<>>,beginwhile j <= m do  i := 1;  while i <= n do     transp[i][j]:= array[j][i];     if i = j then        diag[j]:=array[j][i];        tdiag[j]:=transp[i][j];     end if;   i := i+1;  end while;  j := j+1;end while;print array;print transp;     end algorithm *)THEOREM diagseq == diag=tdiagPROOFOBVIOUS`But I get the error that tdiag is unknown. I'm not sure what I'm not understanding so any help would be appreciated! -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a70545cd-37a0-430a-aad5-bc303a0f33e0%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df-4723-96c7-14153a75b529%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/730D2F51-FD92-4F40-BB2E-57E5CE211791%40gmail.com.