Nuprl Lemma : fpf-conversion-test
4 : 2 ⊕ 6 : 2 ⊕ 7 : 5 = <[4; 6; 7], λx.if x ∈b [4; 6]) then 2 else 5 fi > ∈ i:ℤ fp-> ℤ
Proof
Definitions occuring in Statement :
fpf-single: x : v,
fpf-join: f ⊕ g,
fpf: a:A fp-> B[a],
deq-member: x ∈b L),
int-deq: IntDeq,
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
pair: <a, b>,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Lemmas :
lifting-strict-int_eq,
top_wf,
has-value_wf_base,
base_wf,
lifting-strict-spread,
lifting-strict-callbyvalue,
lifting-strict-ispair,
lifting-strict-decide,
lifting-strict-isaxiom,
fpf-join_wf,
fpf-single_wf,
int-deq_wf
4 : 2 \moplus{} 6 : 2 \moplus{} 7 : 5 = <[4; 6; 7], \mlambda{}x.if x \mmember{}\msubb{} [4; 6]) then 2 else 5 fi >
Date html generated:
2015_07_17-AM-11_09_01
Last ObjectModification:
2015_01_28-AM-07_47_19
Home
Index