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, christina.a.burge@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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. 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/3F9142EF-641E-4A04-8650-DFE1CAC46592%40gmail.com.