Nuprl Lemma : append_is_nil

[T:Type]. ∀[l1,l2:T List].  uiff((l1 l2) [] ∈ (T List);(l1 [] ∈ (T List)) ∧ (l2 [] ∈ (T List)))


Proof




Definitions occuring in Statement :  append: as bs nil: [] list: List uiff: uiff(P;Q) uall: [x:A]. B[x] and: P ∧ Q universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] implies:  Q append: as bs all: x:A. B[x] so_lambda: so_lambda(x,y,z.t[x; y; z]) top: Top so_apply: x[s1;s2;s3] uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a prop: not: ¬A false: False
Lemmas referenced :  list_induction uall_wf list_wf uiff_wf equal_wf append_wf nil_wf and_wf list_ind_nil_lemma list_ind_cons_lemma null_nil_lemma btrue_wf null_wf null_cons_lemma bfalse_wf btrue_neq_bfalse cons_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin lemma_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality hypothesis independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality independent_pairFormation equalityTransitivity equalitySymmetry productElimination independent_pairEquality axiomEquality because_Cache lambdaFormation rename dependent_set_memberEquality applyEquality setElimination setEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[l1,l2:T  List].    uiff((l1  @  l2)  =  [];(l1  =  [])  \mwedge{}  (l2  =  []))



Date html generated: 2016_05_14-AM-06_42_12
Last ObjectModification: 2015_12_26-PM-00_29_32

Theory : list_0


Home Index