Nuprl Lemma : mFOLRule-ext

mFOLRule() ≡ lbl:Atom × if lbl =a "andI" then Unit
                        if lbl =a "impI" then Unit
                        if lbl =a "allI" then ℤ
                        if lbl =a "existsI" then ℤ
                        if lbl =a "orI" then 𝔹
                        if lbl =a "hyp" then Unit
                        if lbl =a "andE" then ℕ
                        if lbl =a "orE" then ℕ
                        if lbl =a "impE" then ℕ
                        if lbl =a "allE" then hypnum:ℕ × ℤ
                        if lbl =a "existsE" then hypnum:ℕ × ℤ
                        else Void
                        fi

Proof

Definitions occuring in Statement : mFOLRule: mFOLRule(), nat: ℕ, ifthenelse: if b then t else f fi , eq_atom: x =a y, bool: 𝔹, ext-eq: A ≡ B, unit: Unit, product: x:A × B[x], int: ℤ, token: "$token", atom: Atom, void: Void
Lemmas : ext-eq_weakening, mFOLRule_wf
mFOLRule() \mequiv{} lbl:Atom \mtimes{} if lbl =a "andI" then Unit if lbl =a "impI" then Unit if lbl =a "allI" then \mBbbZ{} if lbl =a "existsI" then \mBbbZ{} if lbl =a "orI" then \mBbbB{} if lbl =a "hyp" then Unit if lbl =a "andE" then \mBbbN{} if lbl =a "orE" then \mBbbN{} if lbl =a "impE" then \mBbbN{} if lbl =a "allE" then hypnum:\mBbbN{} \mtimes{} \mBbbZ{} if lbl =a "existsE" then hypnum:\mBbbN{} \mtimes{} \mBbbZ{} else Void fi Date html generated: 2015_07_17-AM-07_54_56 Last ObjectModification: 2015_01_27-AM-10_06_01 Home Index