Nuprl Lemma : treeco-ext

[E:Type]. treeco(E) ≡ lbl:Atom × if lbl =a "leaf" then if lbl =a "node" then left:treeco(E) × treeco(E) else Void fi 


Proof




Definitions occuring in Statement :  treeco: treeco(E) ifthenelse: if then else fi  eq_atom: =a y ext-eq: A ≡ B uall: [x:A]. B[x] product: x:A × B[x] token: "$token" atom: Atom void: Void universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T treeco: treeco(E) so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a continuous-monotone: ContinuousMonotone(T.F[T]) and: P ∧ Q type-monotone: Monotone(T.F[T]) subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] strong-type-continuous: Continuous+(T.F[T]) type-continuous: Continuous(T.F[T]) ext-eq: A ≡ B
Lemmas referenced :  corec-ext ifthenelse_wf eq_atom_wf subtype_rel_product bool_wf eqtt_to_assert assert_of_eq_atom eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_atom subtype_rel_wf strong-continuous-depproduct continuous-constant strong-continuous-product continuous-id subtype_rel_weakening nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality productEquality atomEquality instantiate hypothesisEquality tokenEquality hypothesis universeEquality cumulativity voidEquality independent_isectElimination independent_pairFormation because_Cache lambdaFormation unionElimination equalityElimination productElimination dependent_pairFormation equalityTransitivity equalitySymmetry promote_hyp dependent_functionElimination independent_functionElimination voidElimination axiomEquality isect_memberEquality isectEquality applyEquality functionExtensionality functionEquality independent_pairEquality

Latex:
\mforall{}[E:Type]
    treeco(E)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "leaf"  then  E
                                                  if  lbl  =a  "node"  then  left:treeco(E)  \mtimes{}  treeco(E)
                                                  else  Void
                                                  fi 



Date html generated: 2017_10_01-AM-08_30_23
Last ObjectModification: 2017_07_26-PM-04_24_32

Theory : tree_1


Home Index