[tlaplus] Writing a proof in TLA

[marta zhango <martazhango@xxxxxxxxx>]

How can I write the proof for the number of permutations of n distinct objects

using TLA ?  In the form of a structured proof for teaching mathematics rather

than the code intended for the complete description for running in a proof system

like Coq or Lean.

I want to have something like page 24 and 25 in

https://lamport.azurewebsites.net/pubs/proof.pdf

Or something like Thearem 22 on page 31 in

https://lamport.azurewebsites.net/pubs/keappa08-web.pdf

This is my usual proof

 Let S = {a1,a2,...an}

First Choice c1 \in S
Cardinality(c1) = n

Second Choice (Remove previous c1)

c2 \in S\{c1} (remove first choice c1)
Cardinality(c2) = n-1

Continued Choice ci \in S\{c1,c2,...,c{i-1}}
Cardinality(ci) = n-(i-1)

Final Choice cn \in S\{c1,c2,...,c{n-1}}
Cardinality(cn) = 1

Thus Cardinality(S) = n!

-- 
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/dcb6eef4-7fe4-4299-8652-44cb2c1af977n%40googlegroups.com.