Writing a proof in TLA
35 views
Skip to first unread message
marta zhango
Apr 25, 2024, 4:07:40 PM4/25/24
to tlaplus
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
Or something like Thearem 22 on page 31 in
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!
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!
Reply all
Reply to author
Forward
0 new messages