Nuprl Definition : correct_proof

correct_proof(Sequent;effect;s;pf) ==
  fix((λcorrect_proof,s,pf. let sr,f = pf 
                            in ((fst(sr)) = s ∈ Sequent)
                               ∧ case effect sr
                                  of inl(subgoals) =>
                                  ∀i:ℕ||subgoals||. (correct_proof subgoals[i] (f i))
                                  | inr(x) =>
                                  False)) 
  s 
  pf


Definitions occuring in Statement :  select: L[n],  length: ||as||,  int_seg: {i..j-},  pi1: fst(t),  all: ∀x:A. B[x],  and: P ∧ Q,  false: False,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  natural_number: $n,  equal: s = t ∈ T
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  and: P ∧ Q,  equal: s = t ∈ T,  pi1: fst(t),  decide: case b of inl(x) => s[x] | inr(y) => t[y],  all: ∀x:A. B[x],  int_seg: {i..j-},  natural_number: $n,  length: ||as||,  select: L[n],  apply: f a,  false: False
FDL editor aliases :  correct_proof
Latex:
correct\_proof(Sequent;effect;s;pf)  ==
    fix((\mlambda{}correct$_{proof}$,s,pf.  let  sr,f  =  pf 
                                                      in  ((fst(sr))  =  s)
                                                            \mwedge{}  case  effect  sr
                                                                  of  inl(subgoals)  =>
                                                                  \mforall{}i:\mBbbN{}||subgoals||.  (correct$_{proof}$  subgoals[i\000C]  (f  i))
                                                                  |  inr(x)  =>
                                                                  False)) 
    s 
    pf


Date html generated: 2016_05_15-PM-03_15_05
Last ObjectModification: 2015_09_23-AM-07_42_49

Theory : general


Home Index