OAI/Computability/PerfectCompleteness/Foundations/SignedTupleSemantics.lean
23 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PerfectCompleteness.SignedTupleSemantics.sourceIDsline 37 - def
OAI.PerfectCompleteness.SignedTupleSemantics.sourceVariablesline 40 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.sourceIDs_tupleline 45 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.sourceVariables_tupleline 53 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.sourceIDs_eqline 63 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.sourceVariables_eqline 68 - def
OAI.PerfectCompleteness.SignedTupleSemantics.descriptorOfline 72 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.descriptorOf_tapeline 76 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.left_keyline 81 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.right_keyline 90 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.projection_extline 100 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.projection_eqline 111 - def
OAI.PerfectCompleteness.SignedTupleSemantics.occurrenceAtline 128 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.occurrenceAt_sourceline 132 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.descriptorOf_occurrenceAtline 136 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.ofFn_occurrenceAtline 149 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.map_finRange_occurrenceAtline 172 - def
OAI.PerfectCompleteness.SignedTupleSemantics.dataOfPrefixline 178 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.edgeBits_eq_entryline 184 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.next_eq_appendline 199 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.next_atIndex_eqline 214 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.result_eq_appendline 227 - theorem
OAI.PerfectCompleteness.SignedTupleSemantics.full_result_eqline 254