Step
*
1
1
1
1
of Lemma
int_mod_ring_wf
1. n : ℕ+
⊢ <ℤ_n, λu,v. (u mod n =z v mod n), λu,v. ff, λu,v. (u + v), 0, λu.(-u), λu,v. (u * v), 1, λu,v. (inr ⋅ )> ∈ RngSig
BY
{ (Unfold `rng_sig` 0
THEN RepeatFor 2 ((RepeatFor 3 (MemCD') THEN Try (Complete (Auto))))
THEN Try ((BLemma `add_wf_int_mod` THEN Auto))) }
1
.....subterm..... T:t
1:n
1. n : ℕ+
⊢ λu.(-u) ∈ ℤ_n ⟶ ℤ_n
2
.....subterm..... T:t
2:n
1. n : ℕ+
⊢ <λu,v. (u * v), 1, λu,v. (inr ⋅ )> ∈ times:ℤ_n ⟶ ℤ_n ⟶ ℤ_n × one:ℤ_n × (ℤ_n ⟶ ℤ_n ⟶ (ℤ_n?))
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
\mvdash{} <\mBbbZ{}\_n, \mlambda{}u,v. (u mod n =\msubz{} v mod n), \mlambda{}u,v. ff, \mlambda{}u,v. (u + v), 0, \mlambda{}u.(-u), \mlambda{}u,v. (u * v), 1, \mlambda{}u,v. (in\000Cr \mcdot{} )> \mmember{} RngSig
By
Latex:
(Unfold `rng\_sig` 0
THEN RepeatFor 2 ((RepeatFor 3 (MemCD') THEN Try (Complete (Auto))))
THEN Try ((BLemma `add\_wf\_int\_mod` THEN Auto)))
Home
Index