OAI/Analysis/MatrixSigning/Machines/TerminalVectorReplace.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.KS.W19.TerminalVectorReplace.portsline 13 - def
OAI.KS.W19.TerminalVectorReplace.programline 14 - def
OAI.KS.W19.TerminalVectorReplace.preparedline 16 - theorem
OAI.KS.W19.TerminalVectorReplace.replace_specline 19 - def
OAI.KS.W19.TerminalVectorReplace.zeroPayloadsline 46 - def
OAI.KS.W19.TerminalVectorReplace.unitPayloadsline 47 - theorem
OAI.KS.W19.TerminalVectorReplace.zeroTape_eqline 49 - def
OAI.KS.W19.TerminalVectorReplace.oneFrameline 58 - def
OAI.KS.W19.TerminalVectorReplace.unitProgramline 59 - theorem
OAI.KS.W19.TerminalVectorReplace.unit_specline 62 - theorem
OAI.KS.W19.TerminalVectorReplace.unit_tapeline 86 - theorem
OAI.KS.W19.TerminalVectorReplace.unit_witness_specline 92